:: WELLFND1 semantic presentation

registration

let A, B be set ;
cluster PFuncs A,B -> functional ;
coherence

proof end;

end;

definition

let R be 1-sorted ;
let X be set ;
let p be PartFunc of the carrier of R,X;
:: original: dom
redefine func dom p -> Subset of R;
coherence

proof end;

end;

theorem Th1: :: WELLFND1:1

for X being set
for f, g being Function st f c= g & X c= dom f holds
f | X = g | X

proof end;

theorem Th2: :: WELLFND1:2

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{ F₁() -> set , F₂() -> set , P₁[ set ] } :

ex PFS being Subset of (PFuncs F₁(),F₂()) st
for pfs being PartFunc of F₁(),F₂() holds
( pfs in PFS iff P₁[pfs] )

proof end;

registration

let X be set ;
cluster nextcard X -> non empty ;
coherence by CARD_1:def 6;

end;

registration

cluster regular set ;
existence by CARD_5:42;

end;

theorem Th3: :: WELLFND1:3

for M being regular Aleph
for X being set st X c= M & Card X in M holds
sup X in M

proof end;

theorem Th4: :: WELLFND1:4

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

proof end;

end;

:: deftheorem Def1 defines lower WELLFND1:def 1 :

theorem Th5: :: WELLFND1:5

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 Th6: :: WELLFND1:6

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

registration

cluster non empty well_founded RelStr ;
existence

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 :

registration

let R be RelStr ;
cluster well_founded Element of bool the carrier of R;
existence

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

proof end;

uniqueness ;

end;

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

registration

let R be RelStr ;
cluster well_founded-Part R -> lower well_founded ;
coherence

proof end;

end;

theorem Th7: :: WELLFND1:7

for R being non empty RelStr
for x being Element of R holds {x} is well_founded Subset of R

proof end;

theorem Th8: :: WELLFND1:8

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 Th9: :: WELLFND1:9

for R being RelStr holds
( R is well_founded iff well_founded-Part R = the carrier of R )

proof end;

theorem Th10: :: WELLFND1:10

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;

scheme :: WELLFND1:sch 2
WFMin{ F₁() -> non empty RelStr , F₂() -> Element of F₁(), P₁[ set ] } :

ex x being Element of F₁() st
( P₁[x] & ( for y being Element of F₁() holds
( not x <> y or not P₁[y] or not [y,x] in the InternalRel of F₁() ) ) )

provided

A1: P₁[F₂()] and
A2: F₁() is well_founded

proof end;

theorem Th11: :: WELLFND1:11

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{ F₁() -> non empty RelStr , P₁[ set ] } :

for x being Element of F₁() holds P₁[x]

provided

A1: for x being Element of F₁() st ( for y being Element of F₁() st y <> x & [y,x] in the InternalRel of F₁() holds
P₁[y] ) holds
P₁[x] and
A2: F₁() is well_founded

proof end;

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

theorem :: WELLFND1:12

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;

theorem :: WELLFND1:13

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;

theorem :: WELLFND1:14

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;

definition

let R be RelStr ;
let f be sequence of R;
canceled;
attr f is descending means :Def7: :: WELLFND1:def 7
for n being Nat holds
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R );

end;

:: deftheorem WELLFND1:def 6 :

:: deftheorem Def7 defines descending WELLFND1:def 7 :

theorem :: WELLFND1:15

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;