(7steps total)
Remark
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iter
via
intseg
shift
rw
1
1.
A
: Type
2.
f
:
A
A
A
3.
u
:
A
a
,
b
:
,
e
:({
a
..
b
}
A
),
k
:
.
(Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)) = (Iter(
f
;
u
)
j
:{
a
+
k
..
b
+
k
}.
e
(
j
-
k
))
By:
BackThru:
Thm*
P
:(
Prop).
Thm*
(
a
:
,
b
:{...
a
}.
P
(
a
,
b
))
Thm*
Thm*
(
a
:
,
b
:{
a
+1...}. (
c
:{
a
..
b
}.
P
(
a
,
c
))
P
(
a
,
b
))
(
a
,
b
:
.
P
(
a
,
b
))
Generated subgoals:
1
4.
a
:
5.
b
: {...
a
}
6.
e
: {
a
..
b
}
A
7.
k
:
(Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)) = (Iter(
f
;
u
)
j
:{
a
+
k
..
b
+
k
}.
e
(
j
-
k
))
1
step
2
4.
a
:
5.
b
: {
a
+1...}
6.
c
:{
a
..
b
},
e
:({
a
..
c
}
A
),
k
:
.
6.
(Iter(
f
;
u
)
i
:{
a
..
c
}.
e
(
i
)) = (Iter(
f
;
u
)
j
:{
a
+
k
..
c
+
k
}.
e
(
j
-
k
))
7.
e
: {
a
..
b
}
A
8.
k
:
(Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)) = (Iter(
f
;
u
)
j
:{
a
+
k
..
b
+
k
}.
e
(
j
-
k
))
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
Remark
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc