:: LATTICE8 semantic presentation

definition

let c₁ be non empty set ;
let c₂, c₃ be Relation of c₁;
redefine pred c= as c₂ c= c₃ means :: LATTICE8:def 1
for b₁, b₂ being Element of a₁ st [b₁,b₂] in a₂ holds
[b₁,b₂] in a₃;
compatibility

proof end;

end;

:: deftheorem Def1 defines c= LATTICE8:def 1 :

definition

let c₁ be RelStr ;
attr a₁ is finitely_typed means :Def2: :: LATTICE8:def 2
ex b₁ being non empty set st
( ( for b₂ being set st b₂ in the carrier of a₁ holds
b₂ is Equivalence_Relation of b₁ ) & ex b₂ being Nat st
for b₃, b₄ being Equivalence_Relation of b₁
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 b₁ st
( len b₇ = b₂ & b₅,b₆ are_joint_by b₇,b₃,b₄ ) );

end;

:: deftheorem Def2 defines finitely_typed LATTICE8:def 2 :

definition

let c₁ be lower-bounded LATTICE;
let c₂ be Nat;
pred c₁ has_a_representation_of_type<= c₂ means :Def3: :: LATTICE8:def 3
ex b₁ being non trivial set ex b₂ being Homomorphism of a₁,(EqRelLATT b₁) st
( b₂ is one-to-one & Image b₂ is finitely_typed & ex b₃ being Equivalence_Relation of b₁ st
( b₃ in the carrier of (Image b₂) & b₃ <> id b₁ ) & type_of (Image b₂) <= a₂ );

end;

:: deftheorem Def3 defines has_a_representation_of_type<= LATTICE8:def 3 :

registration

cluster lower-bounded distributive finite RelStr ;
existence

proof end;

end;

Lemma3: not 1 is even

proof end;

Lemma4: 2 is even

proof end;

registration

let c₁ be non trivial set ;
cluster non empty full non trivial finitely_typed SubRelStr of EqRelLATT a₁;
existence

proof end;

end;

theorem Th1: :: LATTICE8:1

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

proof end;

theorem Th2: :: LATTICE8:2

for b₁ being trivial Semilattice holds b₁ is modular

proof end;

theorem Th3: :: LATTICE8:3

for b₁ being non empty set
for b₂ being non empty Sublattice of EqRelLATT b₁ holds
( b₂ is trivial or ex b₃ being Equivalence_Relation of b₁ st
( b₃ in the carrier of b₂ & b₃ <> id b₁ ) )

proof end;

theorem Th4: :: LATTICE8:4

for b₁, b₂ being lower-bounded LATTICE
for b₃ being Function of b₁,b₂ st b₃ is infs-preserving & b₃ is sups-preserving holds
( b₃ is meet-preserving & b₃ is join-preserving )

proof end;

theorem Th5: :: LATTICE8:5

for b₁, b₂ being lower-bounded LATTICE st b₁,b₂ are_isomorphic & b₁ is modular holds
b₂ is modular

proof end;

theorem Th6: :: LATTICE8:6

for b₁ being non empty lower-bounded Poset
for b₂ being non empty Poset
for b₃ being monotone Function of b₁,b₂ holds Image b₃ is lower-bounded

proof end;

theorem Th7: :: LATTICE8:7

for b₁ being lower-bounded LATTICE
for b₂, b₃ being Element of b₁
for b₄ being non empty set
for b₅ being Homomorphism of b₁,(EqRelLATT b₄) st b₅ is one-to-one & (corestr b₅) . b₂ <= (corestr b₅) . b₃ holds
b₂ <= b₃

proof end;

theorem Th8: :: LATTICE8:8

for b₁ being non trivial set
for b₂ being non empty full finitely_typed Sublattice of EqRelLATT b₁
for b₃ being Equivalence_Relation of b₁ st b₃ in the carrier of b₂ & b₃ <> id b₁ & type_of b₂ <= 2 holds
b₂ is modular

proof end;

theorem Th9: :: LATTICE8:9

for b₁ being lower-bounded LATTICE st b₁ has_a_representation_of_type<= 2 holds
b₁ is modular

proof end;

definition

let c₁ be set ;
func new_set2 c₁ -> set equals :: LATTICE8:def 4
a₁ \/ {{a₁},{{a₁}}};
correctness ;

end;

:: deftheorem Def4 defines new_set2 LATTICE8:def 4 :

registration

let c₁ be set ;
cluster new_set2 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_fun2 c₃,c₄ -> BiFunction of (new_set2 a₁),a₂ means :Def5: :: LATTICE8:def 5
( ( 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₁}} = ((a₃ . (a₄ `1 ),(a₄ `2 )) "\/" (a₄ `3 )) "/\" (a₄ `4 ) & a₅ . {{a₁}},{a₁} = ((a₃ . (a₄ `1 ),(a₄ `2 )) "\/" (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₄ `2 )) "\/" (a₄ `3 ) & a₅ . {{a₁}},b₁ = (a₃ . b₁,(a₄ `2 )) "\/" (a₄ `3 ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines new_bi_fun2 LATTICE8:def 5 :

theorem Th10: :: LATTICE8:10

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_fun2 b₃,b₄ is zeroed

proof end;

theorem Th11: :: LATTICE8:11

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_fun2 b₃,b₄ is symmetric

proof end;

theorem Th12: :: LATTICE8:12

for b₁ being non empty set
for b₂ being lower-bounded LATTICE st b₂ is modular holds
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_fun2 b₃,b₄ is u.t.i.

proof end;

theorem Th13: :: LATTICE8:13

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

theorem Th14: :: LATTICE8:14

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_fun2 b₃,b₄

proof end;

definition

let c₁ be non empty set ;
let c₂ be Ordinal;
func ConsecutiveSet2 c₁,c₂ -> set means :Def6: :: LATTICE8:def 6
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_set2 (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 Def6 defines ConsecutiveSet2 LATTICE8:def 6 :

theorem Th15: :: LATTICE8:15

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

proof end;

theorem Th16: :: LATTICE8:16

for b₁ being non empty set
for b₂ being Ordinal holds ConsecutiveSet2 b₁,(succ b₂) = new_set2 (ConsecutiveSet2 b₁,b₂)

proof end;

theorem Th17: :: LATTICE8:17

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

proof end;

registration

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

proof end;

end;

theorem Th18: :: LATTICE8:18

for b₁ being non empty set
for b₂ being Ordinal holds b₁ c= ConsecutiveSet2 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;
assume E23: c₅ in dom c₄ ;
func Quadr2 c₄,c₅ -> Element of [:(ConsecutiveSet2 a₁,a₅),(ConsecutiveSet2 a₁,a₅),the carrier of a₂,the carrier of a₂:] equals :Def7: :: LATTICE8:def 7
a₄ . a₅;
correctness

proof end;

end;

:: deftheorem Def7 defines Quadr2 LATTICE8:def 7 :

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 ConsecutiveDelta2 c₄,c₅ -> set means :Def8: :: LATTICE8:def 8
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_fun2 (BiFun (b₁ . b₂),(ConsecutiveSet2 a₁,b₂),a₂),(Quadr2 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 Def8 defines ConsecutiveDelta2 LATTICE8:def 8 :

theorem Th19: :: LATTICE8:19

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 ConsecutiveDelta2 b₄,{} = b₃

proof end;

theorem Th20: :: LATTICE8:20

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₃
for b₅ being Ordinal holds ConsecutiveDelta2 b₄,(succ b₅) = new_bi_fun2 (BiFun (ConsecutiveDelta2 b₄,b₅),(ConsecutiveSet2 b₁,b₅),b₂),(Quadr2 b₄,b₅)

proof end;

theorem Th21: :: LATTICE8:21

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₃
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₇ = ConsecutiveDelta2 b₄,b₇ ) holds
ConsecutiveDelta2 b₄,b₆ = union (rng b₅)

proof end;

theorem Th22: :: LATTICE8:22

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

proof end;

theorem Th23: :: LATTICE8:23

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₃
for b₅ being Ordinal holds ConsecutiveDelta2 b₄,b₅ is BiFunction of (ConsecutiveSet2 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 ConsecutiveDelta2 as ConsecutiveDelta2 c₄,c₅ -> BiFunction of (ConsecutiveSet2 a₁,a₅),a₂;
coherence by Th23;

end;

theorem Th24: :: LATTICE8:24

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₃
for b₅ being Ordinal holds b₃ c= ConsecutiveDelta2 b₄,b₅

proof end;

theorem Th25: :: LATTICE8:25

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

proof end;

theorem Th26: :: LATTICE8:26

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 QuadrSeq of b₃
for b₅ being Ordinal holds ConsecutiveDelta2 b₄,b₅ is zeroed

proof end;

theorem Th27: :: LATTICE8:27

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 QuadrSeq of b₃
for b₅ being Ordinal holds ConsecutiveDelta2 b₄,b₅ is symmetric

proof end;

theorem Th28: :: LATTICE8:28

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

proof end;

theorem Th29: :: LATTICE8:29

for b₁ being non empty set
for b₂ being lower-bounded modular LATTICE
for b₃ being distance_function of b₁,b₂
for b₄ being Ordinal
for b₅ being QuadrSeq of b₃ st b₄ c= DistEsti b₃ holds
ConsecutiveDelta2 b₅,b₄ is distance_function of (ConsecutiveSet2 b₁,b₄),b₂ by Th26, Th27, Th28;

definition

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
func NextSet2 c₃ -> set equals :: LATTICE8:def 9
ConsecutiveSet2 a₁,(DistEsti a₃);
correctness ;

end;

:: deftheorem Def9 defines NextSet2 LATTICE8:def 9 :

registration

let c₁ be non empty set ;
let c₂ be lower-bounded LATTICE;
let c₃ be BiFunction of c₁,c₂;
cluster NextSet2 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 NextDelta2 c₄ -> set equals :: LATTICE8:def 10
ConsecutiveDelta2 a₄,(DistEsti a₃);
correctness ;

end;

:: deftheorem Def10 defines NextDelta2 LATTICE8:def 10 :

definition

let c₁ be non empty set ;
let c₂ be lower-bounded modular LATTICE;
let c₃ be distance_function of c₁,c₂;
let c₄ be QuadrSeq of c₃;
redefine func NextDelta2 as NextDelta2 c₄ -> distance_function of (NextSet2 a₃),a₂;
coherence by Th26, Th27, Th28;

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_extension2_of c₁,c₃ means :Def11: :: LATTICE8:def 11
ex b₁ being QuadrSeq of a₃ st
( a₄ = NextSet2 a₃ & a₅ = NextDelta2 b₁ );

end;

:: deftheorem Def11 defines is_extension2_of LATTICE8:def 11 :

theorem Th30: :: LATTICE8:30

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_extension2_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₁₁ 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 modular LATTICE;
let c₃ be distance_function of c₁,c₂;
mode ExtensionSeq2 of c₁,c₃ -> Function means :Def12: :: LATTICE8:def 12
( 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_extension2_of b₂,b₃ & a₄ . b₁ = [b₂,b₃] & a₄ . (b₁ + 1) = [b₄,b₅] ) ) );
existence

proof end;

end;

:: deftheorem Def12 defines ExtensionSeq2 LATTICE8:def 12 :

theorem Th31: :: LATTICE8:31

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

proof end;

theorem Th32: :: LATTICE8:32

proof end;

theorem Th33: :: LATTICE8:33

for b₁ being lower-bounded modular LATTICE
for b₂ being ExtensionSeq2 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 Th34: :: LATTICE8:34

for b₁ being lower-bounded modular LATTICE
for b₂ being ExtensionSeq2 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₁₀ being Element of b₃ st
( b₄ . b₅,b₉ = b₇ & b₄ . b₉,b₁₀ = ((b₄ . b₅,b₆) "\/" b₇) "/\" b₈ & b₄ . b₁₀,b₆ = b₇ )

proof end;

Lemma42: for b₁ being Nat holds
( not b₁ in Seg 4 or b₁ = 1 or b₁ = 2 or b₁ = 3 or b₁ = 4 )

proof end;

Lemma43: for b₁ being Nat st 1 <= b₁ & b₁ < 4 & not b₁ = 1 & not b₁ = 2 holds
b₁ = 3

proof end;

theorem Th35: :: LATTICE8:35

for b₁ being lower-bounded modular LATTICE
for b₂ being ExtensionSeq2 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 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₁₀ = 2 + 2 & b₈,b₉ are_joint_by b₁₀,b₆,b₇ )

proof end;

theorem Th36: :: LATTICE8:36

for b₁ being lower-bounded modular LATTICE holds b₁ has_a_representation_of_type<= 2

proof end;

theorem Th37: :: LATTICE8:37

for b₁ being lower-bounded LATTICE holds
( b₁ has_a_representation_of_type<= 2 iff b₁ is modular ) by Th9, Th36;