WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites wellfounded?
wellfounded
Def WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
Def
==
P
:(
A
Prop). (
j
:
A
. (
k
:
A
.
R
(
k
;
j
)
P
(
k
))
P
(
j
))
{
n
:
A
.
P
(
n
)}
Thm*
A
:Type{i},
r
:(
A
A
Prop{i}). WellFnd{i}(
A
;
x
,
y
.
r
(
x
,
y
))
Prop{i'}
Syntax:
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
has structure:
wellfounded{i:l}(
A
;
x
,
y
.
R
(
x
;
y
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc