(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
1
1.
i
:
2.
x
:
3.
y
:
4.
x
y
i
x
(
j
:{
x
..
x
+
y
}.
i
) =
i
(
x
+
y
)
By:
BackThru:
Thm*
a
,
c
,
b
:
,
e
:({
a
..
b
}
).
Thm*
a
c
Thm*
Thm*
c
b
(
i
:{
a
..
b
}.
e
(
i
)) = (
i
:{
a
..
c
}.
e
(
i
))
(
i
:{
c
..
b
}.
e
(
i
))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
y
i
x
(
j:{x..x+y
}. i) = i(x+y)
y
ix( j:{x..x+y}. i) = i(x+y)
a,c,b:, e:({a..b}
).
c
b ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))
