PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
lremove
mem
1
2
1
1
2
1
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)
False
10.
eq(s,u)
u = sx
mem_f(St;sx;v \ s)
False
By:
Analyze 0
THEN
Analyze -1
Generated subgoals:
1
11.
u = sx
False
2
11.
mem_f(St;sx;v \ s)
False
About:
False False
St
False
eq(s,u) u = sx 
mem_f(St;sx;v \ s) False False False
