PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

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) False mem_f(S.car;s;AL)) & (s:S.car, a:Alph. False False mem_f(S.car;s;AL))
By: InstConcl [sL]
Generated subgoals:

16. s: S.car
7. mem_f(S.car;s;sL)
w:Alph*. mem_f(S.car;(S:ws);sL)
26. s: S.car
7. mem_f(S.car;s;sL)
False mem_f(S.car;s;sL)

About:
existslistandallimpliesorfalseuniverse