(7steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
increasing
implies
k
:
,
f
:(
k
). increasing(
f
;
k
)
(
x
,
y
:
k
.
x
<
y
f
(
x
)<
f
(
y
))
By:
Unfold `guard` 0 THEN All (Unfold `increasing`)
Generated subgoal:
1
1.
k
:
2.
f
:
k
3.
i
:
(
k
-1).
f
(
i
)<
f
(
i
+1)
4.
x
:
k
5.
y
:
k
6.
x
<
y
f
(
x
)<
f
(
y
)
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
k:
, f:(k
). increasing(f;k) 
(x,y:k. x<y f(x)<f(y)) k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y))
k
i:(k-1). f(i)<f(i+1)
k
k
f(x)<f(y)
