PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: back listify 1
1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. Fin(Alph)
5. Fin(S.car)

BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s)
By: Assert (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]))))
Generated subgoals:

1 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])))
26. 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)

About:
existslistallequalapply
productnatural_numberanduniverse