PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int
mag
well
founded
WellFnd{i}(
;
x
,
y
.|
x
|<|
y
|)
By:
FwdThru:
Thm*
r
:(
T
T
Prop),
S
:Type,
f
:(
S
T
).
Thm*
WellFnd{i}(
T
;
x
,
y
.
r
(
x
,
y
))
WellFnd{i}(
S
;
x
,
y
.
r
(
f
(
x
),
f
(
y
)))
on [
Thm*
WellFnd{i}(
;
x
,
y
.
x
<
y
) ]
Using:[
S
:=
|
f
(
x
):= |
x
|]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
WellFnd{i}(
;x,y.|x|<|y|) WellFnd{i}(;x,y.|x|<|y|)
r:(T
TProp), S:Type, f:(ST).
WellFnd{i}(S;x,y.r(f(x),f(y)))
;x,y.x<y) ]
| f(x):= |x|]
