:: LATTICE5 semantic presentation

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

ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = F₁() & ( for b₂ being Element of NAT holds P₁[b₂,b₁ . b₂,b₁ . (b₂ + 1)] ) )

provided

E1: for b₁ being Nat
for b₂ being set ex b₃ being set st P₁[b₁,b₂,b₃]

proof end;

theorem Th1: :: LATTICE5:1

for b₁ being Function
for b₂ being Function-yielding Function st b₁ = union (rng b₂) holds
dom b₁ = union (rng (doms b₂))

proof end;

theorem Th2: :: LATTICE5:2

for b₁, b₂ being non empty set holds [:(union b₁),(union b₂):] = union { [:b₃,b₄:] where B is Element of b₁, B is Element of b₂ : ( b₃ in b₁ & b₄ in b₂ ) }

proof end;

theorem Th3: :: LATTICE5:3

for b₁ being non empty set st b₁ is c=-linear holds
[:(union b₁),(union b₁):] = union { [:b₂,b₂:] where B is Element of b₁ : b₂ in b₁ }

proof end;

definition

let c₁ be set ;
func EqRelLATT c₁ -> Poset equals :: LATTICE5:def 1
LattPOSet (EqRelLatt a₁);
correctness ;

end;

:: deftheorem Def1 defines EqRelLATT LATTICE5:def 1 :

registration

let c₁ be set ;
cluster EqRelLATT a₁ -> with_suprema with_infima ;
coherence ;

end;

theorem Th4: :: LATTICE5:4

for b₁, b₂ being set holds
( b₂ in the carrier of (EqRelLATT b₁) iff b₂ is Equivalence_Relation of b₁ )

proof end;

theorem Th5: :: LATTICE5:5

for b₁ being set
for b₂, b₃ being Element of (EqRelLatt b₁) holds
( b₂ [= b₃ iff b₂ c= b₃ )

proof end;

theorem Th6: :: LATTICE5:6

for b₁ being set
for b₂, b₃ being Element of (EqRelLATT b₁) holds
( b₂ <= b₃ iff b₂ c= b₃ )

proof end;

theorem Th7: :: LATTICE5:7

for b₁ being Lattice
for b₂, b₃ being Element of (LattPOSet b₁) holds b₂ "/\" b₃ = (% b₂) "/\" (% b₃)

proof end;

theorem Th8: :: LATTICE5:8

for b₁ being set
for b₂, b₃ being Element of (EqRelLATT b₁) holds b₂ "/\" b₃ = b₂ /\ b₃

proof end;

theorem Th9: :: LATTICE5:9

for b₁ being Lattice
for b₂, b₃ being Element of (LattPOSet b₁) holds b₂ "\/" b₃ = (% b₂) "\/" (% b₃)

proof end;

theorem Th10: :: LATTICE5:10

for b₁ being set
for b₂, b₃ being Element of (EqRelLATT b₁)
for b₄, b₅ being Equivalence_Relation of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ "\/" b₃ = b₄ "\/" b₅

proof end;

definition

let c₁ be non empty RelStr ;
redefine attr a₁ is complete means :: LATTICE5:def 2
for b₁ being Subset of a₁ ex b₂ being Element of a₁ st
( b₂ is_<=_than b₁ & ( for b₃ being Element of a₁ st b₃ is_<=_than b₁ holds
b₃ <= b₂ ) );
compatibility

proof end;

end;

:: deftheorem Def2 defines complete LATTICE5:def 2 :

registration

let c₁ be set ;
cluster EqRelLATT a₁ -> with_suprema with_infima complete ;
coherence

proof end;

end;

registration

let c₁, c₂ be LATTICE;
cluster meet-preserving join-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

definition

let c₁, c₂ be LATTICE;
mode Homomorphism of a₁,a₂ is meet-preserving join-preserving Function of a₁,a₂;

end;

registration

let c₁ be LATTICE;
cluster strict meet-inheriting join-inheriting SubRelStr of a₁;
existence

proof end;

end;

definition

let c₁ be non empty RelStr ;
mode Sublattice of a₁ is meet-inheriting join-inheriting SubRelStr of a₁;

end;

definition

let c₁, c₂ be LATTICE;
let c₃ be Homomorphism of c₁,c₂;
redefine func Image as Image c₃ -> strict full Sublattice of a₂;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty FinSequence of c₁;
let c₃, c₄ be set ;
let c₅, c₆ be Relation;
pred c₃,c₄ are_joint_by c₂,c₅,c₆ means :Def3: :: LATTICE5:def 3
( a₂ . 1 = a₃ & a₂ . (len a₂) = a₄ & ( for b₁ being Nat st 1 <= b₁ & b₁ < len a₂ holds
( ( not b₁ is even implies [(a₂ . b₁),(a₂ . (b₁ + 1))] in a₅ ) & ( b₁ is even implies [(a₂ . b₁),(a₂ . (b₁ + 1))] in a₆ ) ) ) );

end;

:: deftheorem Def3 defines are_joint_by LATTICE5:def 3 :

theorem Th11: :: LATTICE5:11

canceled;

theorem Th12: :: LATTICE5:12

for b₁ being non empty set
for b₂ being set
for b₃ being Nat
for b₄, b₅ being Relation
for b₆ being non empty FinSequence of b₁ st b₄ is_reflexive_in b₁ & b₅ is_reflexive_in b₁ & b₆ = b₃ |-> b₂ holds
b₂,b₂ are_joint_by b₆,b₄,b₅

proof end;

E13: now

let c₁, c₂, c₃ be Nat;
assume ( 1 <= c₁ & c₁ < c₂ + c₃ ) ;
then ( ( 1 <= c₁ & c₁ < c₂ ) or ( c₂ = c₁ & c₁ < c₂ + c₃ ) or ( c₂ < c₁ & c₁ < c₂ + c₃ ) ) by REAL_1:def 5;
hence ( ( 1 <= c₁ & c₁ < c₂ ) or ( c₂ = c₁ & c₁ < c₂ + c₃ ) or ( c₂ + 1 <= c₁ & c₁ < c₂ + c₃ ) ) by NAT_1:38;

end;

theorem Th13: :: LATTICE5:13

canceled;

theorem Th14: :: LATTICE5:14

for b₁ being non empty set
for b₂, b₃ being set
for b₄, b₅ being Relation
for b₆, b₇ being Nat st b₆ <= b₇ & b₄ is_reflexive_in b₁ & b₅ is_reflexive_in b₁ & ex b₈ being non empty FinSequence of b₁ st
( len b₈ = b₆ & b₂,b₃ are_joint_by b₈,b₄,b₅ ) holds
ex b₈ being non empty FinSequence of b₁ st
( len b₈ = b₇ & b₂,b₃ are_joint_by b₈,b₄,b₅ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Sublattice of EqRelLATT c₁;
given c₃ being Equivalence_Relation of c₁ such that E15: c₃ in the carrier of c₂ and
E16: c₃ <> id c₁ ;
given c₄ being Nat such that E17: for b₁, b₂ being Equivalence_Relation of c₁
for b₃, b₄ being set st b₁ in the carrier of c₂ & b₂ in the carrier of c₂ & [b₃,b₄] in b₁ "\/" b₂ holds
ex b₅ being non empty FinSequence of c₁ st
( len b₅ = c₄ & b₃,b₄ are_joint_by b₅,b₁,b₂ ) ;
func type_of c₂ -> Nat means :Def4: :: LATTICE5:def 4
( ( for b₁, b₂ being Equivalence_Relation of a₁
for b₃, b₄ being set st b₁ in the carrier of a₂ & b₂ in the carrier of a₂ & [b₃,b₄] in b₁ "\/" b₂ holds
ex b₅ being non empty FinSequence of a₁ st
( len b₅ = a₃ + 2 & b₃,b₄ are_joint_by b₅,b₁,b₂ ) ) & ex b₁, b₂ being Equivalence_Relation of a₁ex b₃, b₄ being set st
( b₁ in the carrier of a₂ & b₂ in the carrier of a₂ & [b₃,b₄] in b₁ "\/" b₂ & ( for b₅ being non empty FinSequence of a₁ holds
( not len b₅ = a₃ + 1 or not b₃,b₄ are_joint_by b₅,b₁,b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines type_of LATTICE5:def 4 :

theorem Th15: :: LATTICE5:15

for b₁ being non empty set
for b₂ being Sublattice of EqRelLATT b₁
for b₃ being Nat st ex b₄ being Equivalence_Relation of b₁ st
( b₄ in the carrier of b₂ & b₄ <> id b₁ ) & ( for b₄, b₅ being Equivalence_Relation of b₁
for b₆, b₇ being set st b₄ in the carrier of b₂ & b₅ in the carrier of b₂ & [b₆,b₇] in b₄ "\/" b₅ holds
ex b₈ being non empty FinSequence of b₁ st
( len b₈ = b₃ + 2 & b₆,b₇ are_joint_by b₈,b₄,b₅ ) ) holds
type_of b₂ <= b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
mode BiFunction of a₁,a₂ is Function of [:a₁,a₁:],the carrier of a₂;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
let c₄, c₅ be Element of c₁;
redefine func . as c₃ . c₄,c₅ -> Element of a₂;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
canceled;
attr a₃ is symmetric means :Def6: :: LATTICE5:def 6
for b₁, b₂ being Element of a₁ holds a₃ . b₁,b₂ = a₃ . b₂,b₁;
attr a₃ is zeroed means :Def7: :: LATTICE5:def 7
for b₁ being Element of a₁ holds a₃ . b₁,b₁ = Bottom a₂;
attr a₃ is u.t.i. means :Def8: :: LATTICE5:def 8
for b₁, b₂, b₃ being Element of a₁ holds (a₃ . b₁,b₂) "\/" (a₃ . b₂,b₃) >= a₃ . b₁,b₃;

end;

:: deftheorem Def5 LATTICE5:def 5 :

:: deftheorem Def6 defines symmetric LATTICE5:def 6 :

:: deftheorem Def7 defines zeroed LATTICE5:def 7 :

:: deftheorem Def8 defines u.t.i. LATTICE5:def 8 :

registration

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
cluster symmetric zeroed u.t.i. Relation of [:a₁,a₁:],the carrier of a₂;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
mode distance_function of a₁,a₂ is symmetric zeroed u.t.i. BiFunction of a₁,a₂;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be distance_function of c₁,c₂;
func alpha c₃ -> Function of a₂,(EqRelLATT a₁) means :Def9: :: LATTICE5:def 9
for b₁ being Element of a₂ ex b₂ being Equivalence_Relation of a₁ st
( b₂ = a₄ . b₁ & ( for b₃, b₄ being Element of a₁ holds
( [b₃,b₄] in b₂ iff a₃ . b₃,b₄ <= b₁ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines alpha LATTICE5:def 9 :

theorem Th16: :: LATTICE5:16

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being distance_function of b₁,b₂ holds alpha b₃ is meet-preserving

proof end;

theorem Th17: :: LATTICE5:17

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being distance_function of b₁,b₂ st b₃ is onto holds
alpha b₃ is one-to-one

proof end;

definition

let c₁ be set ;
func new_set c₁ -> set equals :: LATTICE5:def 10
a₁ \/ {{a₁},{{a₁}},{{{a₁}}}};
correctness ;

end;

:: deftheorem Def10 defines new_set LATTICE5:def 10 :

registration

let c₁ be set ;
cluster new_set a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
let c₄ be Element of [:c₁,c₁,the carrier of c₂,the carrier of c₂:];
func new_bi_fun c₃,c₄ -> BiFunction of (new_set a₁),a₂ means :Def11: :: LATTICE5:def 11
( ( for b₁, b₂ being Element of a₁ holds a₅ . b₁,b₂ = a₃ . b₁,b₂ ) & a₅ . {a₁},{a₁} = Bottom a₂ & a₅ . {{a₁}},{{a₁}} = Bottom a₂ & a₅ . {{{a₁}}},{{{a₁}}} = Bottom a₂ & a₅ . {{a₁}},{{{a₁}}} = a₄ `3 & a₅ . {{{a₁}}},{{a₁}} = a₄ `3 & a₅ . {a₁},{{a₁}} = a₄ `4 & a₅ . {{a₁}},{a₁} = a₄ `4 & a₅ . {a₁},{{{a₁}}} = (a₄ `3 ) "\/" (a₄ `4 ) & a₅ . {{{a₁}}},{a₁} = (a₄ `3 ) "\/" (a₄ `4 ) & ( for b₁ being Element of a₁ holds
( a₅ . b₁,{a₁} = (a₃ . b₁,(a₄ `1 )) "\/" (a₄ `3 ) & a₅ . {a₁},b₁ = (a₃ . b₁,(a₄ `1 )) "\/" (a₄ `3 ) & a₅ . b₁,{{a₁}} = ((a₃ . b₁,(a₄ `1 )) "\/" (a₄ `3 )) "\/" (a₄ `4 ) & a₅ . {{a₁}},b₁ = ((a₃ . b₁,(a₄ `1 )) "\/" (a₄ `3 )) "\/" (a₄ `4 ) & a₅ . b₁,{{{a₁}}} = (a₃ . b₁,(a₄ `2 )) "\/" (a₄ `4 ) & a₅ . {{{a₁}}},b₁ = (a₃ . b₁,(a₄ `2 )) "\/" (a₄ `4 ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines new_bi_fun LATTICE5:def 11 :

theorem Th18: :: LATTICE5:18

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being BiFunction of b₁,b₂ st b₃ is zeroed holds
for b₄ being Element of [:b₁,b₁,the carrier of b₂,the carrier of b₂:] holds new_bi_fun b₃,b₄ is zeroed

proof end;

theorem Th19: :: LATTICE5:19

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being BiFunction of b₁,b₂ st b₃ is symmetric holds
for b₄ being Element of [:b₁,b₁,the carrier of b₂,the carrier of b₂:] holds new_bi_fun b₃,b₄ is symmetric

proof end;

theorem Th20: :: LATTICE5:20

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being BiFunction of b₁,b₂ st b₃ is symmetric & b₃ is u.t.i. holds
for b₄ being Element of [:b₁,b₁,the carrier of b₂,the carrier of b₂:] st b₃ . (b₄ `1 ),(b₄ `2 ) <= (b₄ `3 ) "\/" (b₄ `4 ) holds
new_bi_fun b₃,b₄ is u.t.i.

proof end;

theorem Th21: :: LATTICE5:21

for b₁ being set holds b₁ c= new_set b₁ by XBOOLE_1:7;

theorem Th22: :: LATTICE5:22

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being BiFunction of b₁,b₂
for b₄ being Element of [:b₁,b₁,the carrier of b₂,the carrier of b₂:] holds b₃ c= new_bi_fun b₃,b₄

proof end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
func DistEsti c₃ -> Cardinal means :Def12: :: LATTICE5:def 12
a₄,{ [b₁,b₂,b₃,b₄] where B is Element of a₁, B is Element of a₁, B is Element of a₂, B is Element of a₂ : a₃ . b₁,b₂ <= b₃ "\/" b₄ } are_equipotent ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines DistEsti LATTICE5:def 12 :

theorem Th23: :: LATTICE5:23

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being distance_function of b₁,b₂ holds DistEsti b₃ <> {}

proof end;

definition

let c₁ be non empty set ;
let c₂ be Ordinal;
func ConsecutiveSet c₁,c₂ -> set means :Def13: :: LATTICE5:def 13
ex b₁ being T-Sequence st
( a₃ = last b₁ & dom b₁ = succ a₂ & b₁ . {} = a₁ & ( for b₂ being Ordinal st succ b₂ in succ a₂ holds
b₁ . (succ b₂) = new_set (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₂ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = union (rng (b₁ | b₂)) ) );
correctness

proof end;

end;

:: deftheorem Def13 defines ConsecutiveSet LATTICE5:def 13 :

theorem Th24: :: LATTICE5:24

for b₁ being non empty set holds ConsecutiveSet b₁,{} = b₁

proof end;

theorem Th25: :: LATTICE5:25

for b₁ being non empty set
for b₂ being Ordinal holds ConsecutiveSet b₁,(succ b₂) = new_set (ConsecutiveSet b₁,b₂)

proof end;

theorem Th26: :: LATTICE5:26

for b₁ being non empty set
for b₂ being T-Sequence
for b₃ being Ordinal st b₃ <> {} & b₃ is_limit_ordinal & dom b₂ = b₃ & ( for b₄ being Ordinal st b₄ in b₃ holds
b₂ . b₄ = ConsecutiveSet b₁,b₄ ) holds
ConsecutiveSet b₁,b₃ = union (rng b₂)

proof end;

registration

let c₁ be non empty set ;
let c₂ be Ordinal;
cluster ConsecutiveSet a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th27: :: LATTICE5:27

for b₁ being non empty set
for b₂ being Ordinal holds b₁ c= ConsecutiveSet b₁,b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
mode QuadrSeq of c₃ -> T-Sequence of [:a₁,a₁,the carrier of a₂,the carrier of a₂:] means :Def14: :: LATTICE5:def 14
( dom a₄ is Cardinal & a₄ is one-to-one & rng a₄ = { [b₁,b₂,b₃,b₄] where B is Element of a₁, B is Element of a₁, B is Element of a₂, B is Element of a₂ : a₃ . b₁,b₂ <= b₃ "\/" b₄ } );
existence

proof end;

end;

:: deftheorem Def14 defines QuadrSeq LATTICE5:def 14 :

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
let c₄ be QuadrSeq of c₃;
let c₅ be Ordinal;
assume E37: c₅ in dom c₄ ;
func Quadr c₄,c₅ -> Element of [:(ConsecutiveSet a₁,a₅),(ConsecutiveSet a₁,a₅),the carrier of a₂,the carrier of a₂:] equals :Def15: :: LATTICE5:def 15
a₄ . a₅;
correctness

proof end;

end;

:: deftheorem Def15 defines Quadr LATTICE5:def 15 :

theorem Th28: :: LATTICE5:28

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂
for b₅ being QuadrSeq of b₄ holds
( b₃ in DistEsti b₄ iff b₃ in dom b₅ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be set ;
assume E39: c₃ is BiFunction of c₁,c₂ ;
func BiFun c₃,c₁,c₂ -> BiFunction of a₁,a₂ equals :Def16: :: LATTICE5:def 16
a₃;
coherence by E39;

end;

:: deftheorem Def16 defines BiFun LATTICE5:def 16 :

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
let c₄ be QuadrSeq of c₃;
let c₅ be Ordinal;
func ConsecutiveDelta c₄,c₅ -> set means :Def17: :: LATTICE5:def 17
ex b₁ being T-Sequence st
( a₆ = last b₁ & dom b₁ = succ a₅ & b₁ . {} = a₃ & ( for b₂ being Ordinal st succ b₂ in succ a₅ holds
b₁ . (succ b₂) = new_bi_fun (BiFun (b₁ . b₂),(ConsecutiveSet a₁,b₂),a₂),(Quadr a₄,b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₅ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = union (rng (b₁ | b₂)) ) );
correctness

proof end;

end;

:: deftheorem Def17 defines ConsecutiveDelta LATTICE5:def 17 :

theorem Th29: :: LATTICE5:29

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being BiFunction of b₁,b₂
for b₄ being QuadrSeq of b₃ holds ConsecutiveDelta b₄,{} = b₃

proof end;

theorem Th30: :: LATTICE5:30

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂
for b₅ being QuadrSeq of b₄ holds ConsecutiveDelta b₅,(succ b₃) = new_bi_fun (BiFun (ConsecutiveDelta b₅,b₃),(ConsecutiveSet b₁,b₃),b₂),(Quadr b₅,b₃)

proof end;

theorem Th31: :: LATTICE5:31

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being T-Sequence
for b₄ being Ordinal
for b₅ being BiFunction of b₁,b₂
for b₆ being QuadrSeq of b₅ st b₄ <> {} & b₄ is_limit_ordinal & dom b₃ = b₄ & ( for b₇ being Ordinal st b₇ in b₄ holds
b₃ . b₇ = ConsecutiveDelta b₆,b₇ ) holds
ConsecutiveDelta b₆,b₄ = union (rng b₃)

proof end;

theorem Th32: :: LATTICE5:32

for b₁ being non empty set
for b₂, b₃ being Ordinal st b₂ c= b₃ holds
ConsecutiveSet b₁,b₂ c= ConsecutiveSet b₁,b₃

proof end;

theorem Th33: :: LATTICE5:33

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂
for b₅ being QuadrSeq of b₄ holds ConsecutiveDelta b₅,b₃ is BiFunction of (ConsecutiveSet b₁,b₃),b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
let c₄ be QuadrSeq of c₃;
let c₅ be Ordinal;
redefine func ConsecutiveDelta as ConsecutiveDelta c₄,c₅ -> BiFunction of (ConsecutiveSet a₁,a₅),a₂;
coherence by Th33;

end;

theorem Th34: :: LATTICE5:34

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂
for b₅ being QuadrSeq of b₄ holds b₄ c= ConsecutiveDelta b₅,b₃

proof end;

theorem Th35: :: LATTICE5:35

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃, b₄ being Ordinal
for b₅ being BiFunction of b₁,b₂
for b₆ being QuadrSeq of b₅ st b₃ c= b₄ holds
ConsecutiveDelta b₆,b₃ c= ConsecutiveDelta b₆,b₄

proof end;

theorem Th36: :: LATTICE5:36

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂ st b₄ is zeroed holds
for b₅ being QuadrSeq of b₄ holds ConsecutiveDelta b₅,b₃ is zeroed

proof end;

theorem Th37: :: LATTICE5:37

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂ st b₄ is symmetric holds
for b₅ being QuadrSeq of b₄ holds ConsecutiveDelta b₅,b₃ is symmetric

proof end;

theorem Th38: :: LATTICE5:38

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being BiFunction of b₁,b₂ st b₄ is symmetric & b₄ is u.t.i. holds
for b₅ being QuadrSeq of b₄ st b₃ c= DistEsti b₄ holds
ConsecutiveDelta b₅,b₃ is u.t.i.

proof end;

theorem Th39: :: LATTICE5:39

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being Ordinal
for b₄ being distance_function of b₁,b₂
for b₅ being QuadrSeq of b₄ st b₃ c= DistEsti b₄ holds
ConsecutiveDelta b₅,b₃ is distance_function of (ConsecutiveSet b₁,b₃),b₂ by Th36, Th37, Th38;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
func NextSet c₃ -> set equals :: LATTICE5:def 18
ConsecutiveSet a₁,(DistEsti a₃);
correctness ;

end;

:: deftheorem Def18 defines NextSet LATTICE5:def 18 :

registration

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
cluster NextSet a₃ -> non empty ;
coherence ;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
let c₄ be QuadrSeq of c₃;
func NextDelta c₄ -> set equals :: LATTICE5:def 19
ConsecutiveDelta a₄,(DistEsti a₃);
correctness ;

end;

:: deftheorem Def19 defines NextDelta LATTICE5:def 19 :

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be distance_function of c₁,c₂;
let c₄ be QuadrSeq of c₃;
redefine func NextDelta as NextDelta c₄ -> distance_function of (NextSet a₃),a₂;
coherence by Th36, Th37, Th38;

end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be distance_function of c₁,c₂;
let c₄ be non empty set ;
let c₅ be distance_function of c₄,c₂;
pred c₄,c₅ is_extension_of c₁,c₃ means :Def20: :: LATTICE5:def 20
ex b₁ being QuadrSeq of a₃ st
( a₄ = NextSet a₃ & a₅ = NextDelta b₁ );

end;

:: deftheorem Def20 defines is_extension_of LATTICE5:def 20 :

theorem Th40: :: LATTICE5:40

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being distance_function of b₁,b₂
for b₄ being non empty set
for b₅ being distance_function of b₄,b₂ st b₄,b₅ is_extension_of b₁,b₃ holds
for b₆, b₇ being Element of b₁
for b₈, b₉ being Element of b₂ st b₃ . b₆,b₇ <= b₈ "\/" b₉ holds
ex b₁₀, b₁₁, b₁₂ being Element of b₄ st
( b₅ . b₆,b₁₀ = b₈ & b₅ . b₁₁,b₁₂ = b₈ & b₅ . b₁₀,b₁₁ = b₉ & b₅ . b₁₂,b₇ = b₉ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be distance_function of c₁,c₂;
mode ExtensionSeq of c₁,c₃ -> Function means :Def21: :: LATTICE5:def 21
( dom a₄ = NAT & a₄ . 0 = [a₁,a₃] & ( for b₁ being Nat ex b₂ being non empty set ex b₃ being distance_function of b₂,a₂ex b₄ being non empty set ex b₅ being distance_function of b₄,a₂ st
( b₄,b₅ is_extension_of b₂,b₃ & a₄ . b₁ = [b₂,b₃] & a₄ . (b₁ + 1) = [b₄,b₅] ) ) );
existence

proof end;

end;

:: deftheorem Def21 defines ExtensionSeq LATTICE5:def 21 :

theorem Th41: :: LATTICE5:41

for b₁ being non empty set
for b₂ being lower-bounded LATTICE
for b₃ being distance_function of b₁,b₂
for b₄ being ExtensionSeq of b₁,b₃
for b₅, b₆ being Nat st b₅ <= b₆ holds
(b₄ . b₅) `1 c= (b₄ . b₆) `1

proof end;

theorem Th42: :: LATTICE5:42

proof end;

definition

let c₁ be lower-bounded LATTICE;
func BasicDF c₁ -> distance_function of the carrier of a₁,a₁ means :Def22: :: LATTICE5:def 22
for b₁, b₂ being Element of a₁ holds
( ( b₁ <> b₂ implies a₂ . b₁,b₂ = b₁ "\/" b₂ ) & ( b₁ = b₂ implies a₂ . b₁,b₂ = Bottom a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines BasicDF LATTICE5:def 22 :

theorem Th43: :: LATTICE5:43

for b₁ being lower-bounded LATTICE holds BasicDF b₁ is onto

proof end;

E58: now

let c₁ be Nat;
assume E59: ( 1 <= c₁ & c₁ < 5 ) ;
then c₁ < 4 + 1 ;
then c₁ <= 4 by NAT_1:38;
then ( c₁ = 0 or c₁ = 1 or c₁ = 2 or c₁ = 3 or c₁ = 4 ) by CQC_THE1:5;
hence ( c₁ = 1 or c₁ = 2 or c₁ = 3 or c₁ = 4 ) by E59;

end;

E59: now

let c₁ be Nat;
assume E60: c₁ in Seg 5 ;
then ( 1 <= c₁ & c₁ <= 5 ) by FINSEQ_1:3;
then ( c₁ = 0 or c₁ = 1 or c₁ = 2 or c₁ = 3 or c₁ = 4 or c₁ = 5 ) by CQC_THE1:6;
hence ( c₁ = 1 or c₁ = 2 or c₁ = 3 or c₁ = 4 or c₁ = 5 ) by E60, FINSEQ_1:3;

end;

E60: now

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be distance_function of c₁,c₂;
( succ {} c= DistEsti c₃ or DistEsti c₃ in succ {} ) by ORDINAL1:26;
then ( succ {} c= DistEsti c₃ or DistEsti c₃ c= {} ) by ORDINAL1:34;
then ( succ {} c= DistEsti c₃ or DistEsti c₃ = {} ) by XBOOLE_1:3;
hence succ {} c= DistEsti c₃ by Th23;

end;

theorem Th44: :: LATTICE5:44

for b₁ being lower-bounded LATTICE
for b₂ being ExtensionSeq of the carrier of b₁, BasicDF b₁
for b₃ being non empty set st b₃ = union { ((b₂ . b₄) `1 ) where B is Nat : verum } holds
union { ((b₂ . b₄) `2 ) where B is Nat : verum } is distance_function of b₃,b₁

proof end;

theorem Th45: :: LATTICE5:45

for b₁ being lower-bounded LATTICE
for b₂ being ExtensionSeq of the carrier of b₁, BasicDF b₁
for b₃ being non empty set
for b₄ being distance_function of b₃,b₁
for b₅, b₆ being Element of b₃
for b₇, b₈ being Element of b₁ st b₃ = union { ((b₂ . b₉) `1 ) where B is Nat : verum } & b₄ = union { ((b₂ . b₉) `2 ) where B is Nat : verum } & b₄ . b₅,b₆ <= b₇ "\/" b₈ holds
ex b₉, b₁₀, b₁₁ being Element of b₃ st
( b₄ . b₅,b₉ = b₇ & b₄ . b₁₀,b₁₁ = b₇ & b₄ . b₉,b₁₀ = b₈ & b₄ . b₁₁,b₆ = b₈ )

proof end;

theorem Th46: :: LATTICE5:46

for b₁ being lower-bounded LATTICE
for b₂ being ExtensionSeq of the carrier of b₁, BasicDF b₁
for b₃ being non empty set
for b₄ being distance_function of b₃,b₁
for b₅ being Homomorphism of b₁,(EqRelLATT b₃)
for b₆, b₇ being Element of b₃
for b₈, b₉ being Equivalence_Relation of b₃
for b₁₀, b₁₁ being set st b₅ = alpha b₄ & b₃ = union { ((b₂ . b₁₂) `1 ) where B is Nat : verum } & b₄ = union { ((b₂ . b₁₂) `2 ) where B is Nat : verum } & b₈ in the carrier of (Image b₅) & b₉ in the carrier of (Image b₅) & [b₁₀,b₁₁] in b₈ "\/" b₉ holds
ex b₁₂ being non empty FinSequence of b₃ st
( len b₁₂ = 3 + 2 & b₁₀,b₁₁ are_joint_by b₁₂,b₈,b₉ )

proof end;

theorem Th47: :: LATTICE5:47

for b₁ being lower-bounded LATTICE ex b₂ being non empty set ex b₃ being Homomorphism of b₁,(EqRelLATT b₂) st
( b₃ is one-to-one & type_of (Image b₃) <= 3 )

proof end;