PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
lshort
mem
2
1
2
1
1.
St:
Type
2.
l:
St*
3.
eq:
St
St
4.
x,y:St. eq(x,y)
x = y
5.
s:
St
6.
u:
St
7.
v:
St*
8.
mem_f(St;s;v)
mem_f(St;s;LShort(v))
9.
mem_f(St;s;v)
u = s
if eq(u,s)
False else mem_f(St;s;LShort(v)) fi
By:
SplitOnConclITE
Generated subgoals:
1
10.
eq(u,s)
u = s
False
2
10.
eq(u,s)
u = s
mem_f(St;s;LShort(v))
About:
u = s 
False
eq(u,s) u = s mem_f(St;s;LShort(v))
St
x,y:St. eq(x,y) 
x = y mem_f(St;s;LShort(v)) u = s if eq(u,s)
False else mem_f(St;s;LShort(v)) fi u = s Falseeq(u,s) u = s mem_f(St;s;LShort(v))
