PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
add
action
mem
3
2
1.
St:
Type
2.
l:
St*
3.
f:
St
St
4.
s:
St
5.
s':
St
6.
f(s') = s
7.
u:
St
8.
v:
St*
9.
mem_f(St;s';v)
mem_f(St;s;(+f)(v))
mem_f(St;s';u.v)
mem_f(St;s;(+f)(u.v))
By:
RecUnfold `mem_f` 0
THEN
RecUnfold `add_action` 0
THEN
Reduce 0
Generated subgoal:
1
u = s'
mem_f(St;s';v)
u = s
f(u) = s
mem_f(St;s;(+f)(v))
About:
u = s' 
mem_f(St;s';v) 
u = s f(u) = s mem_f(St;s;(+f)(v))
St mem_f(St;s;(+f)(v)) mem_f(St;s';u.v) mem_f(St;s;(+f)(u.v)) u = s' mem_f(St;s';v) u = s f(u) = s mem_f(St;s;(+f)(v))
