PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: add action mem 1 2 1 2 1 1 1
1. St: Type
2. l: St*
3. f: StSt
4. s: St
5. u: St
6. v: St*
7. mem_f(St;s;(+f)(v)) mem_f(St;s;v) (s':St. mem_f(St;s';v) & f(s') = s)
8. f(u) = s

u = u mem_f(St;u;v)
By: Sel 1 (Analyze 0)
Generated subgoals:

None

About:
orequaluniverselistfunction
impliesexistsandapply