PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
add
action
mem
1
1
1.
St:
Type
2.
l:
St*
3.
f:
St
St
4.
s:
St
mem_f(St;s;(+f)(nil))
mem_f(St;s;nil)
(
s':St. mem_f(St;s';nil) & f(s') = s)
By:
RecUnfold `mem_f` 0
THEN
RecUnfold `add_action` 0
THEN
Reduce 0
Generated subgoals:
None
About:
St
mem_f(St;s;(+f)(nil)) 
mem_f(St;s;nil) 
(
s':St. mem_f(St;s';nil) & f(s') = s)
