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