(7steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sum
exponent
1
2
1.
i
:
2.
x
,
y
:
.
x
y
i
x
i
y
=
i
(
x
+
y
)
3.
x
:
4.
y
:
i
x
i
y
=
i
(
x
+
y
)
By:
Decide:
x
y
Generated subgoals:
1
5.
x
y
i
x
i
y
=
i
(
x
+
y
)
1
step
2
5.
x
y
i
x
i
y
=
i
(
x
+
y
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
x,y:
. x
y 
i
x
iy = i(x+y)
ixiy = i(x+y)
x,y:. xy ixiy = i(x+y)
ixiy = i(x+y)yy
ixiy = i(x+y)
xy
ixiy = i(x+y)
