IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
well_fnd
Nuprl Section: well_fnd
Defines predicate saying that a binary relation over some type is well-founded.
Well-foundedness is phrased in terms of a `course of values' induction principle, since this is more useful constructively than alternative formulations (e.g. saying that there are no infinite descending chains, or saying that every non-empty subset has a minimal element).
NB: constructively, these alternative formulations are not equivalent.
Lemmas and tactics are introduced for induction on the rank of
an expression (`inverse image induction'). One deficiency of Nuprl's
type theory is that in some situations (notably when proving well-formedness
goals) lemmas are unusable, and instead one must resort to using
tactics that reproduce equivalent sequences of primitive rules.
The theorem
r:(T
T
WellFnd{i}(S;x,y.r(f(x),f(y)))
