(10steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sq
stable
is
member
1
2
1
1.
T:
Type
2.
eq:
T
T
3.
x:
T
4.
L:
T List
5.
u:
T
6.
v:
T List
7.
SqStable(x(
eq) v)
SqStable(if eq(x,u)
true
else x(
eq) v fi)
By:
GenConcl (eq(x,u) = b)
Generated subgoal:
1
8.
b:
9.
eq(x,u) = b
SqStable(if b
true
else x(
eq) v fi)
About:
(10steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
SqStable(if b
true
else x(
eq) v fi)
T
eq) v)
SqStable(if eq(x,u) true else x(eq) v fi)
SqStable(if b true else x(eq) v fi)
