:: 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

f tolerates g ) holds

union X is Function

proof end;

:: Cardinals

registration
end;

registration

ex b_{1} being Aleph st b_{1} is regular
by CARD_5:30;

end;

cluster non empty epsilon-transitive epsilon-connected ordinal non finite cardinal regular for set ;

existence ex b

:: Relational structures

definition

let R be RelStr ;

let X be Subset of R;

( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds

y in X )

end;
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 for x, y being set st x in X & [y,x] in the InternalRel of R holds

y in X;

( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds

y in X )

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

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

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

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;

begin

definition

let R be RelStr ;

end;
attr R is well_founded means :Def2: :: WELLFND1:def 2

the InternalRel of R is_well_founded_in the carrier of R;

the InternalRel of R is_well_founded_in the carrier of R;

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

for R being RelStr holds

( R is well_founded iff the InternalRel of R is_well_founded_in the carrier of R );

registration
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 );

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

definition

let R be RelStr ;

ex b_{1} being Subset of R st b_{1} = union { S where S is Subset of R : ( S is well_founded & S is lower ) }

for b_{1}, b_{2} being Subset of R st b_{1} = union { S where S is Subset of R : ( S is well_founded & S is lower ) } & b_{2} = union { S where S is Subset of R : ( S is well_founded & S is lower ) } holds

b_{1} = b_{2}
;

end;
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 it = union { S where S is Subset of R : ( S is well_founded & S is lower ) } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines well_founded-Part WELLFND1:def 4 :

for R being RelStr

for b_{2} being Subset of R holds

( b_{2} = well_founded-Part R iff b_{2} = union { S where S is Subset of R : ( S is well_founded & S is lower ) } );

for R being RelStr

for b

( b

registration

let R be RelStr ;

coherence

( well_founded-Part R is lower & well_founded-Part R is well_founded )

end;
coherence

( well_founded-Part R is lower & well_founded-Part R is well_founded )

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

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 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

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

:: 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 )

( 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{ F_{1}() -> non empty RelStr , P_{1}[ set ] } :

provided

WFInduction{ F

provided

A1:
for x being Element of F_{1}() st ( for y being Element of F_{1}() st y <> x & [y,x] in the InternalRel of F_{1}() holds

P_{1}[y] ) holds

P_{1}[x]
and

A2: F_{1}() is well_founded

P

P

A2: F

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;

end;
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 :Def5: :: WELLFND1:def 5

for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x)));

for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x)));

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

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 )

( 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

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

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;

end;
let f be sequence of R;

attr f is descending means :Def6: :: WELLFND1:def 6

for n being Nat holds

( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R );

for n being Nat holds

( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R );

:: 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 & [(f . (n + 1)),(f . n)] in the InternalRel of R ) );

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 )

( R is well_founded iff for f being sequence of R holds not f is descending )

proof end;