:: WELLFND1 semantic presentation

registration

let c₁, c₂ be set ;
cluster PFuncs a₁,a₂ -> functional ;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be set ;
let c₃ be PartFunc of the carrier of c₁,c₂;
redefine func dom as dom c₃ -> Subset of a₁;
coherence

proof end;

end;

theorem Th1: :: WELLFND1:1

for b₁ being set
for b₂, b₃ being Function st b₂ c= b₃ & b₁ c= dom b₂ holds
b₂ | b₁ = b₃ | b₁

proof end;

theorem Th2: :: WELLFND1:2

for b₁ being functional set st ( for b₂, b₃ being Function st b₂ in b₁ & b₃ in b₁ holds
b₂ tolerates b₃ ) holds
union b₁ is Function

proof end;

scheme :: WELLFND1:sch 1
s1{ F₁() -> set , F₂() -> set , P₁[ set ] } :

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

proof end;

registration

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

end;

registration

cluster regular set ;
existence by CARD_5:42;

end;

theorem Th3: :: WELLFND1:3

for b₁ being regular Aleph
for b₂ being set st b₂ c= b₁ & Card b₂ in b₁ holds
sup b₂ in b₁

proof end;

theorem Th4: :: WELLFND1:4

for b₁ being RelStr
for b₂ being set holds the InternalRel of b₁ -Seg b₂ c= the carrier of b₁

proof end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
redefine attr a₂ is lower means :Def1: :: WELLFND1:def 1
for b₁, b₂ being set st b₁ in a₂ & [b₂,b₁] in the InternalRel of a₁ holds
b₂ in a₂;
compatibility

proof end;

end;

:: deftheorem Def1 defines lower WELLFND1:def 1 :

theorem Th5: :: WELLFND1:5

for b₁ being RelStr
for b₂ being Subset of b₁
for b₃ being set st b₂ is lower & b₃ in b₂ holds
the InternalRel of b₁ -Seg b₃ c= b₂

proof end;

theorem Th6: :: WELLFND1:6

for b₁ being RelStr
for b₂ being lower Subset of b₁
for b₃ being Subset of b₁
for b₄ being set st b₃ = b₂ \/ {b₄} & the InternalRel of b₁ -Seg b₄ c= b₂ holds
b₃ is lower

proof end;

definition

let c₁ be RelStr ;
attr a₁ is well_founded means :Def2: :: WELLFND1:def 2
the InternalRel of a₁ is_well_founded_in the carrier of a₁;

end;

:: deftheorem Def2 defines well_founded WELLFND1:def 2 :

registration

cluster non empty well_founded RelStr ;
existence

proof end;

end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
attr a₂ is well_founded means :Def3: :: WELLFND1:def 3
the InternalRel of a₁ is_well_founded_in a₂;

end;

:: deftheorem Def3 defines well_founded WELLFND1:def 3 :

registration

let c₁ be RelStr ;
cluster well_founded Element of bool the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be RelStr ;
func well_founded-Part c₁ -> Subset of a₁ means :Def4: :: WELLFND1:def 4
a₂ = union { b₁ where B is Subset of a₁ : ( b₁ is well_founded & b₁ is lower ) } ;
existence

proof end;

uniqueness ;

end;

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

registration

let c₁ be RelStr ;
cluster well_founded-Part a₁ -> lower well_founded ;
coherence

proof end;

end;

theorem Th7: :: WELLFND1:7

for b₁ being non empty RelStr
for b₂ being Element of b₁ holds {b₂} is well_founded Subset of b₁

proof end;

theorem Th8: :: WELLFND1:8

for b₁ being RelStr
for b₂, b₃ being well_founded Subset of b₁ st b₂ is lower holds
b₂ \/ b₃ is well_founded Subset of b₁

proof end;

theorem Th9: :: WELLFND1:9

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

proof end;

theorem Th10: :: WELLFND1:10

for b₁ being non empty RelStr
for b₂ being Element of b₁ st the InternalRel of b₁ -Seg b₂ c= well_founded-Part b₁ holds
b₂ in well_founded-Part b₁

proof end;

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

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

provided

E15: P₁[F₂()] and
E16: F₁() is well_founded

proof end;

theorem Th11: :: WELLFND1:11

for b₁ being non empty RelStr holds
( b₁ is well_founded iff for b₂ being set st ( for b₃ being Element of b₁ st the InternalRel of b₁ -Seg b₃ c= b₂ holds
b₃ in b₂ ) holds
the carrier of b₁ c= b₂ )

proof end;

scheme :: WELLFND1:sch 3
s3{ F₁() -> non empty RelStr , P₁[ set ] } :

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

provided

E16: for b₁ being Element of F₁() st ( for b₂ being Element of F₁() st b₂ <> b₁ & [b₂,b₁] in the InternalRel of F₁() holds
P₁[b₂] ) holds
P₁[b₁] and
E17: F₁() is well_founded

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be non empty set ;
let c₃ be Function of [:the carrier of c₁,(PFuncs the carrier of c₁,c₂):],c₂;
let c₄ be Function;
pred c₄ is_recursively_expressed_by c₃ means :Def5: :: WELLFND1:def 5
for b₁ being Element of a₁ holds a₄ . b₁ = a₃ . [b₁,(a₄ | (the InternalRel of a₁ -Seg b₁))];

end;

:: deftheorem Def5 defines is_recursively_expressed_by WELLFND1:def 5 :

theorem Th12: :: WELLFND1:12

for b₁ being non empty RelStr holds
( b₁ is well_founded iff for b₂ being non empty set
for b₃ being Function of [:the carrier of b₁,(PFuncs the carrier of b₁,b₂):],b₂ ex b₄ being Function of the carrier of b₁,b₂ st b₄ is_recursively_expressed_by b₃ )

proof end;

theorem Th13: :: WELLFND1:13

for b₁ being non empty RelStr
for b₂ being non trivial set st ( for b₃ being Function of [:the carrier of b₁,(PFuncs the carrier of b₁,b₂):],b₂
for b₄, b₅ being Function of the carrier of b₁,b₂ st b₄ is_recursively_expressed_by b₃ & b₅ is_recursively_expressed_by b₃ holds
b₄ = b₅ ) holds
b₁ is well_founded

proof end;

theorem Th14: :: WELLFND1:14

for b₁ being non empty well_founded RelStr
for b₂ being non empty set
for b₃ being Function of [:the carrier of b₁,(PFuncs the carrier of b₁,b₂):],b₂
for b₄, b₅ being Function of the carrier of b₁,b₂ st b₄ is_recursively_expressed_by b₃ & b₅ is_recursively_expressed_by b₃ holds
b₄ = b₅

proof end;

definition

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

end;

:: deftheorem Def6 WELLFND1:def 6 :

:: deftheorem Def7 defines descending WELLFND1:def 7 :

theorem Th15: :: WELLFND1:15

for b₁ being non empty RelStr holds
( b₁ is well_founded iff for b₂ being sequence of b₁ holds not b₂ is descending )

proof end;