PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: add action mem 1 2
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)

mem_f(St;s;(+f)(u.v)) mem_f(St;s;u.v) (s':St. mem_f(St;s';u.v) & f(s') = s)
By:
RecUnfold `mem_f` 0
THEN
RecUnfold `add_action` 0
THEN
Reduce 0
Generated subgoal:

1 u = s f(u) = s mem_f(St;s;(+f)(v)) u = s mem_f(St;s;v) (s':St. u = s' mem_f(St;s';v) & f(s') = s)

About:
impliesconsorexistsand
equalapplyuniverselistfunction