:: On same equivalents of well-foundedness
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Copyright (c) 1997-2019 Association of Mizar Users

:: 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
proof end;

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] )
proof end;

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

registration
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
proof end;

:: 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
proof end;

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 object st x in X & [y,x] in the InternalRel of R holds
y in X;
compatibility
( X is lower iff for x, y being object st x in X & [y,x] in the InternalRel of R holds
y in X )
proof end;
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 object 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
proof end;

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
proof end;

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

:: deftheorem 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
existence
ex b1 being RelStr st
( not b1 is empty & b1 is well_founded )
proof end;
end;

definition
let R be RelStr ;
let X be Subset of R;
attr X 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
proof end;
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 ) }
proof end;
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 ;
coherence
proof end;
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
proof end;

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
proof end;

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

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
proof end;

:: Well-founded induction
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
proof end;

:: 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 )
proof end;

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 & [y,x] in the InternalRel of F1() holds
P1[y] ) holds
P1[x] and
A2: F1() is well_founded
proof end;

:: 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;
pred F is_recursively_expressed_by H means :: WELLFND1:def 5
for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x)));
end;

:: deftheorem 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 )
proof end;

:: 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 & F2 is_recursively_expressed_by H holds
F1 = F2 ) holds
R is well_founded
proof end;

:: 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 & F2 is_recursively_expressed_by H holds
F1 = F2
proof end;

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

:: deftheorem 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 & [(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 )
proof end;