PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: back listify 1 2 1
1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. n:
5. f: nAlph
6. Bij(n; Alph; f)
7. n1:
8. f1: n1S.car
9. Bij(n1; S.car; f1)
10. LL:(S.carS.car*)*. BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||LL||. 1of(LL[i]) = t & mem_f(S.car;s;2of(LL[i])))

BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s)
By:
InstHyp [(x. < f1(x),(y.S.act(f(y),f1(x)))[n] > )[n1]] -1
THEN
Thin -2
Generated subgoal:

110. BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||(x. < f1(x),(y.S.act(f(y),f1(x)))[n] > )[n1]||. 1of(((x. < f1(x),(y.S.act(f(y),f1(x)))[n] > )[n1])[i]) = t & mem_f(S.car;s;2of(((x. < f1(x),(y.S.act(f(y),f1(x)))[n] > )[n1])[i])))
BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s)

About:
existslistallequalapplylambda
pairnatural_numberuniversefunctionproductand