PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
lremove
mem
1
2
1
2
2
1.
St:
Type
2.
l:
St*
3.
s:
St
4.
eq:
St
St
5.
sx:
St
6.
u:
St
7.
v:
St*
8.
eq(s,sx)
9.
mem_f(St;sx;v \ s)
mem_f(St;sx;v)
10.
eq(s,u)
mem_f(St;sx;u.(v \ s))
u = sx
mem_f(St;sx;v)
By:
Analyze 0
THEN
RecUnfold `mem_f` -1
THEN
Reduce -1
Generated subgoal:
1
11.
u = sx
mem_f(St;sx;v \ s)
u = sx
mem_f(St;sx;v)
About:
mem_f(St;sx;v \ s)
u = sx mem_f(St;sx;v)
St
eq(s,sx)
mem_f(St;sx;v)eq(s,u) mem_f(St;sx;u.(v \ s)) u = sx mem_f(St;sx;v) mem_f(St;sx;v \ s) u = sx mem_f(St;sx;v)
