(5steps total)
Remark
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sum
via
intseg
split
mid
2
is_assoc_sep(
; (
x
,
y
.
x
+
y
))
By:
Analyze THEN Reduce Concl
Generated subgoal:
1
1.
x
:
y@0
,
y
:
.
x
+
y@0
+
y
=
x
+
y@0
+
y
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
Remark
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
is_assoc_sep(
; (
x,y. x+y)) is_assoc_sep(; (x,y. x+y))
y@0,y:. x+y@0+y = x+y@0+y
