(13steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iter
prod
zero
iff
factor
zero
1
1
1
1.
a
:
k
:
,
b
:
,
e
:({
a
..
b
}
).
b
-
a
=
k
((
i
:{
a
..
b
}.
e
(
i
)) = 0
(Or
i
:{
a
..
b
}.
e
(
i
) = 0))
By:
Guarding (<prop>
<prop>) (NatInd Concl)
Generated subgoals:
1
2.
b
:
3.
e
: {
a
..
b
}
4.
b
-
a
= 0
(
i
:{
a
..
b
}.
e
(
i
)) = 0
(Or
i
:{
a
..
b
}.
e
(
i
) = 0)
2
steps
2
2.
k
:
3. 0<
k
4.
b
:
,
e
:({
a
..
b
}
).
4.
b
-
a
=
k
-1
((
i
:{
a
..
b
}.
e
(
i
)) = 0
(Or
i
:{
a
..
b
}.
e
(
i
) = 0))
5.
b
:
6.
e
: {
a
..
b
}
7.
b
-
a
=
k
(
i
:{
a
..
b
}.
e
(
i
)) = 0
(Or
i
:{
a
..
b
}.
e
(
i
) = 0)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc