PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
add
action
mem
2
2
1
2
1.
St:
Type
2.
l:
St*
3.
f:
St
St
4.
s:
St
5.
u:
St
6.
v:
St*
7.
mem_f(St;s;v)
mem_f(St;s;(+f)(v))
8.
mem_f(St;s;v)
u = s
f(u) = s
mem_f(St;s;(+f)(v))
By:
FwdThru 7 [8]
THEN
ProveProp
Generated subgoals:
None
About:
St
mem_f(St;s;(+f)(v))
u = s 
f(u) = s mem_f(St;s;(+f)(v))
