(4steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The zero-zero pair does not succeed any other.
At:
next
nat
pair
not
zeroes
xy
:(
).
<0,0> = next_nat_pair(
xy
)
By:
Def of
<prop> THEN New:[
x
|
y
] Analyze1
Generated subgoal:
1
1.
x
:
2.
y
:
3. <0,0> = next_nat_pair(<
x
,
y
>)
False
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
xy:(
). 
<0,0> = next_nat_pair(xy) 
xy:(). <0,0> = next_nat_pair(xy) <prop> THEN New:[x | y] Analyze1
False
