(7steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
and
via
all
intseg
notnull
1
3
1.
a
:
2.
b
:
3.
P
: {
a
..
b
}
Prop
4.
a
<
b
5.
c
:
6.
b
=
c
+1
7.
i
:{
a
..
c
}.
P
(
i
)
8.
P
(
c
)
9.
i
: {
a
..
b
}
P
(
i
)
By:
Decide:
i
=
c
Generated subgoals:
1
10.
i
=
c
P
(
i
)
1
step
2
10.
i
=
c
P
(
i
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
}
Prop
i:{a..c
P(i)
i = c
