(5steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
st
vs
boolsize
1
1
1.
a
:
2.
p
:
a
i
:
a
.
p
(
i
)
if
p
(
i
)
1 else 0 fi = 1
2
By:
Analyze THEN SplitOnConclITE
Generated subgoals:
1
3.
i
:
a
4.
p
(
i
)
true
1 = 1
2
1
step
2
3.
i
:
a
4.
p
(
i
)
false
0 = 1
2
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
a
i:a. p(i) 
if p(i)
1 else 0 fi = 1 
2
a
i:a. p(i) if p(i) 1 else 0 fi = 1 2a
true
1 = 1 2
a
p(i)
false 0 = 1 2
