(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
1.
i
:
x
,
y
:
.
i
x
i
y
=
i
(
x
+
y
)
By:
x
,
y
:
.
x
y
i
x
i
y
=
i
(
x
+
y
) Asserted
Generated subgoals:
1
2.
x
:
3.
y
:
4.
x
y
i
x
i
y
=
i
(
x
+
y
)
2
steps
2
2.
x
,
y
:
.
x
y
i
x
i
y
=
i
(
x
+
y
)
3.
x
:
4.
y
:
i
x
i
y
=
i
(
x
+
y
)
3
steps
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:
. i
x
iy = i(x+y)
x,y:. ixiy = i(x+y)x,y:. x
y 
ixiy = i(x+y) Asserted
y
ixiy = i(x+y)
x,y:. xy ixiy = i(x+y)
ixiy = i(x+y)
