:: On same equivalents of well-foundedness
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 25, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

:: General preliminaries
theorem Th1: :: WELLFND1:1
for X being functional set st ( for f, g being Function st f in X & g in X holds
f tolerates g ) holds
union X is Function
proofend;

scheme :: WELLFND1:sch 1
PFSeparation{ F1() ->  set , F2() ->  set , P1[ set ] } :
 ex PFS being Subset of (PFuncs (F1(),F2())) st
for pfs being PartFunc of F1(),F2() holds
( pfs in PFS iff P1[pfs] )
proofend;

:: Cardinals
registration
let X be set ;
cluster nextcard X ->  non empty ;
coherence
 not nextcard X is empty by CARD_1:def_3;
end;

registration
cluster non empty epsilon-transitive epsilon-connected ordinal non finite cardinal regular for set ;
existence
 ex b1 being Aleph st b1 is regular by CARD_5:30;
end;

theorem Th2: :: WELLFND1:2
for M being regular Aleph
for X being set st X c= M & card X in M holds
sup X in M
proofend;

:: Relational structures
theorem Th3: :: WELLFND1:3
for R being RelStr
for x being set holds the InternalRel of R -Seg x c= the carrier of R
proofend;

definition
let R be RelStr ;
let X be Subset of R;
redefine attr X is lower  means :Def1: :: WELLFND1:def 1
 for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X;
compatibility
 ( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X )
proofend;
end;

:: deftheorem Def1 defines lower WELLFND1:def_1_:_
 for R being RelStr
for X being Subset of R holds
( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X );

theorem Th4: :: WELLFND1:4
for R being RelStr
for X being Subset of R
for x being set st X is lower & x in X holds
the InternalRel of R -Seg x c= X
proofend;

theorem Th5: :: WELLFND1:5
for R being RelStr
for X being lower Subset of R
for Y being Subset of R
for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds
Y is lower
proofend;

begin

definition
let R be RelStr ;
attrR is well_founded  means :Def2: :: WELLFND1:def 2
 the InternalRel of R is_well_founded_in the carrier of R;
end;

:: deftheorem Def2 defines well_founded WELLFND1:def_2_:_
 for R being RelStr holds
( R is well_founded iff the InternalRel of R is_well_founded_in the carrier of R );

registration
cluster non empty well_founded for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is empty & b1 is well_founded )
proofend;
end;

definition
let R be RelStr ;
let X be Subset of R;
attrX is well_founded  means :Def3: :: WELLFND1:def 3
 the InternalRel of R is_well_founded_in X;
end;

:: deftheorem Def3 defines well_founded WELLFND1:def_3_:_
 for R being RelStr
for X being Subset of R holds
( X is well_founded iff the InternalRel of R is_well_founded_in X );

registration
let R be RelStr ;
cluster well_founded for Element of bool the carrier of R;
existence
 ex b1 being Subset of R st b1 is well_founded
proofend;
end;

definition
let R be RelStr ;
func well_founded-Part R ->  Subset of R means :Def4: :: WELLFND1:def 4
it = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ;
existence
 ex b1 being Subset of R st b1 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }
proofend;
uniqueness
 for b1, b2 being Subset of R st b1 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  & b2 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  holds
b1 = b2 ;
end;

:: deftheorem Def4 defines well_founded-Part WELLFND1:def_4_:_
 for R being RelStr
for b2 being Subset of R holds
( b2 = well_founded-Part R iff b2 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  );

registration
let R be RelStr ;
cluster well_founded-Part R ->  lower well_founded ;
coherence
 ( well_founded-Part R is lower & well_founded-Part R is well_founded )
proofend;
end;

theorem Th6: :: WELLFND1:6
for R being non empty RelStr
for x being Element of R holds {x} is well_founded Subset of R
proofend;

theorem Th7: :: WELLFND1:7
for R being RelStr
for X, Y being well_founded Subset of R st X is lower holds
X \/ Y is well_founded Subset of R
proofend;

theorem Th8: :: WELLFND1:8
for R being RelStr holds
( R is well_founded iff well_founded-Part R = the carrier of R )
proofend;

theorem Th9: :: WELLFND1:9
for R being non empty RelStr
for x being Element of R st the InternalRel of R -Seg x c= well_founded-Part R holds
x in well_founded-Part R
proofend;

scheme :: WELLFND1:sch 2
WFMin{ F1() ->  non empty RelStr , F2() ->  Element of F1(), P1[ set ] } :
 ex x being Element of F1() st
( P1[x] & ( for y being Element of F1() holds
( not x <> y or not P1[y] or not [y,x] in the InternalRel of F1() ) ) )
provided
A1: P1[F2()] and
A2: F1() is well_founded
proofend;

:: WF iff WFInduction
theorem Th10: :: WELLFND1:10
for R being non empty RelStr holds
( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S )
proofend;

scheme :: WELLFND1:sch 3
WFInduction{ F1() ->  non empty RelStr , P1[ set ] } :
 for x being Element of F1() holds P1[x]
provided
A1: for x being Element of F1() st ( for y being Element of F1() st y <> x &amp; [y,x] in the InternalRel of F1() holds
P1[y] ) holds
P1[x] and
A2: F1() is well_founded
proofend;

:: Well-foundedness and recursive definitions
definition
let R be non empty RelStr ;
let V be non empty set ;
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V;
let F be Function;
predF is_recursively_expressed_by H means :Def5: :: WELLFND1:def 5
 for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x)));
end;

:: deftheorem Def5 defines is_recursively_expressed_by WELLFND1:def_5_:_
 for R being non empty RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F being Function holds
( F is_recursively_expressed_by H iff for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x))) );

:: Well foundedness and existence
theorem :: WELLFND1:11
for R being non empty RelStr holds
( R is well_founded iff for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )
proofend;

:: Uniqueness implies well-foundedness
theorem :: WELLFND1:12
for R being non empty RelStr
for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H &amp; F2 is_recursively_expressed_by H holds
F1 = F2 ) holds
R is well_founded
proofend;

:: Well-foundedness implies uniqueness
theorem :: WELLFND1:13
for R being non empty well_founded RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H &amp; F2 is_recursively_expressed_by H holds
F1 = F2
proofend;

:: Well-foundedness and omega chains
definition
let R be RelStr ;
let f be sequence of R;
attrf is descending  means :Def6: :: WELLFND1:def 6
 for n being Nat holds
( f . (n + 1) <> f . n &amp; [(f . (n + 1)),(f . n)] in the InternalRel of R );
end;

:: deftheorem Def6 defines descending WELLFND1:def_6_:_
 for R being RelStr
for f being sequence of R holds
( f is descending iff for n being Nat holds
( f . (n + 1) <> f . n &amp; [(f . (n + 1)),(f . n)] in the InternalRel of R ) );

:: omega chains
theorem :: WELLFND1:14
for R being non empty RelStr holds
( R is well_founded iff for f being sequence of R holds not f is descending )
proofend;