(9steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
remove
wf
1
2
1
1
1.
T:
Type
2.
eq:
T
T
3.
x:
T
4.
L:
T List
5.
u:
T
6.
v:
T List
7.
remove(eq;x;v)
T List
8.
b:
9.
eq(x,u) = b
if b
v else u.remove(eq;x;v) fi
T List
By:
BoolInd 8
THEN
Rewrite (HigherC ifthenelse_evalC) 0
Generated subgoals:
1
8.
eq(x,u) = true
v
T List
2
8.
eq(x,u) = false
u.remove(eq;x;v)
T List
About:
(9steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
v 
T List u.remove(eq;x;v) T List
T
T List
if b
v else u.remove(eq;x;v) fi T List
v T List u.remove(eq;x;v) T List
