PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
lremove
wf
1
1.
St:
Type
2.
l:
St*
3.
s:
St
4.
eq:
St
St
(l \ s)
St*
By:
ListInd 2
THEN
RecUnfold `lremove` 0
THEN
Reduce 0
Generated subgoals:
1
nil
St*
2
5.
u:
St
6.
v:
St*
7.
(v \ s)
St*
if eq(s,u)
v \ s else u.(v \ s) fi
St*
About:
nil 
St* St* if eq(s,u)
v \ s else u.(v \ s) fi St*
St
(l \ s) St* nil St* St* if eq(s,u) v \ s else u.(v \ s) fi St*
