PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))
By: Assert (n:. TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL))))
Generated subgoals:

1 n:. TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)))
26. n:. TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)))
TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))

About:
existslistallorand
equalnatural_numberimpliesapplyuniverse