:: LATTICE8 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let A be non empty set ;
let P, R be Relation of A;
:: original: c=
redefine pred P c= R means :: LATTICE8:def 1
for a, b being Element of A st [a,b] in P holds
[a,b] in R;
compatibility
( P c= R iff for a, b being Element of A st [a,b] in P holds
[a,b] in R )
proof end;
end;

:: deftheorem defines c= LATTICE8:def 1 :
for A being non empty set
for P, R being Relation of A holds
( P c= R iff for a, b being Element of A st [a,b] in P holds
[a,b] in R );

definition
let L be RelStr ;
attr L is finitely_typed means :Def2: :: LATTICE8:def 2
ex A being non empty set st
( ( for e being set st e in the carrier of L holds
e is Equivalence_Relation of A ) & ex o being Nat st
for e1, e2 being Equivalence_Relation of A
for x, y being set st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of A st
( len F = o & x,y are_joint_by F,e1,e2 ) );
end;

:: deftheorem Def2 defines finitely_typed LATTICE8:def 2 :
for L being RelStr holds
( L is finitely_typed iff ex A being non empty set st
( ( for e being set st e in the carrier of L holds
e is Equivalence_Relation of A ) & ex o being Nat st
for e1, e2 being Equivalence_Relation of A
for x, y being set st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of A st
( len F = o & x,y are_joint_by F,e1,e2 ) ) );

definition
let L be lower-bounded LATTICE;
let n be Nat;
pred L has_a_representation_of_type<= n means :Def3: :: LATTICE8:def 3
ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st
( f is one-to-one & Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n );
end;

:: deftheorem Def3 defines has_a_representation_of_type<= LATTICE8:def 3 :
for L being lower-bounded LATTICE
for n being Nat holds
( L has_a_representation_of_type<= n iff ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st
( f is one-to-one & Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n ) );

registration
cluster lower-bounded distributive finite RelStr ;
existence
ex b1 being LATTICE st
( b1 is lower-bounded & b1 is distributive & b1 is finite )
proof end;
end;

Lm1: not 1 is even
proof end;

Lm2: 2 is even
proof end;

registration
let A be non trivial set ;
cluster non empty full non trivial finitely_typed SubRelStr of EqRelLATT A;
existence
ex b1 being non empty Sublattice of EqRelLATT A st
( not b1 is trivial & b1 is finitely_typed & b1 is full )
proof end;
end;

theorem Th1: :: LATTICE8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d
proof end;

theorem :: LATTICE8:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being trivial Semilattice holds L is modular
proof end;

theorem :: LATTICE8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being non empty Sublattice of EqRelLATT A holds
( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) )
proof end;

theorem Th4: :: LATTICE8:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being lower-bounded LATTICE
for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds
( f is meet-preserving & f is join-preserving )
proof end;

theorem Th5: :: LATTICE8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds
L2 is modular
proof end;

theorem Th6: :: LATTICE8:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty lower-bounded Poset
for T being non empty Poset
for f being monotone Function of S,T holds Image f is lower-bounded
proof end;

theorem Th7: :: LATTICE8:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded LATTICE
for x, y being Element of L
for A being non empty set
for f being Homomorphism of L,(EqRelLATT A) st f is one-to-one & (corestr f) . x <= (corestr f) . y holds
x <= y
proof end;

theorem Th8: :: LATTICE8:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non trivial set
for L being non empty full finitely_typed Sublattice of EqRelLATT A
for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular
proof end;

theorem Th9: :: LATTICE8:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded LATTICE st L has_a_representation_of_type<= 2 holds
L is modular
proof end;

definition
let A be set ;
func new_set2 A -> set equals :: LATTICE8:def 4
A \/ {{A},{{A}}};
correctness
coherence
A \/ {{A},{{A}}} is set
;
;
end;

:: deftheorem defines new_set2 LATTICE8:def 4 :
for A being set holds new_set2 A = A \/ {{A},{{A}}};

registration
let A be set ;
cluster new_set2 A -> non empty ;
coherence
not new_set2 A is empty
proof end;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun2 d,q -> BiFunction of (new_set2 A),L means :Def5: :: LATTICE8:def 5
( ( for u, v being Element of A holds it . u,v = d . u,v ) & it . {A},{A} = Bottom L & it . {{A}},{{A}} = Bottom L & it . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & it . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( it . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & it . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & it . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & it . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) );
existence
ex b1 being BiFunction of (new_set2 A),L st
( ( for u, v being Element of A holds b1 . u,v = d . u,v ) & b1 . {A},{A} = Bottom L & b1 . {{A}},{{A}} = Bottom L & b1 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & b1 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( b1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b1 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & b1 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) )
proof end;
uniqueness
for b1, b2 being BiFunction of (new_set2 A),L st ( for u, v being Element of A holds b1 . u,v = d . u,v ) & b1 . {A},{A} = Bottom L & b1 . {{A}},{{A}} = Bottom L & b1 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & b1 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( b1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b1 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & b1 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) & ( for u, v being Element of A holds b2 . u,v = d . u,v ) & b2 . {A},{A} = Bottom L & b2 . {{A}},{{A}} = Bottom L & b2 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & b2 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( b2 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b2 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b2 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & b2 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines new_bi_fun2 LATTICE8:def 5 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A,the carrier of L,the carrier of L:]
for b5 being BiFunction of (new_set2 A),L holds
( b5 = new_bi_fun2 d,q iff ( ( for u, v being Element of A holds b5 . u,v = d . u,v ) & b5 . {A},{A} = Bottom L & b5 . {{A}},{{A}} = Bottom L & b5 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & b5 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( b5 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b5 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b5 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & b5 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) ) );

theorem Th10: :: LATTICE8:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is zeroed
proof end;

theorem Th11: :: LATTICE8:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is symmetric
proof end;

theorem Th12: :: LATTICE8:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun2 d,q is u.t.i.
proof end;

theorem Th13: :: LATTICE8:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds A c= new_set2 A by XBOOLE_1:7;

theorem Th14: :: LATTICE8:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds d c= new_bi_fun2 d,q
proof end;

definition
let A be non empty set ;
let O be Ordinal;
func ConsecutiveSet2 A,O -> set means :Def6: :: LATTICE8:def 6
ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) )
;
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def6 defines ConsecutiveSet2 LATTICE8:def 6 :
for A being non empty set
for O being Ordinal
for b3 being set holds
( b3 = ConsecutiveSet2 A,O iff ex L0 being T-Sequence st
( b3 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th15: :: LATTICE8:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds ConsecutiveSet2 A,{} = A
proof end;

theorem Th16: :: LATTICE8:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for O being Ordinal holds ConsecutiveSet2 A,(succ O) = new_set2 (ConsecutiveSet2 A,O)
proof end;

theorem Th17: :: LATTICE8:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for O being Ordinal
for T being T-Sequence st O <> {} & O is_limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 A,O1 ) holds
ConsecutiveSet2 A,O = union (rng T)
proof end;

registration
let A be non empty set ;
let O be Ordinal;
cluster ConsecutiveSet2 A,O -> non empty ;
coherence
not ConsecutiveSet2 A,O is empty
proof end;
end;

theorem Th18: :: LATTICE8:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet2 A,O
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume A1: O in dom q ;
func Quadr2 q,O -> Element of [:(ConsecutiveSet2 A,O),(ConsecutiveSet2 A,O),the carrier of L,the carrier of L:] equals :Def7: :: LATTICE8:def 7
q . O;
correctness
coherence
q . O is Element of [:(ConsecutiveSet2 A,O),(ConsecutiveSet2 A,O),the carrier of L,the carrier of L:]
;
proof end;
end;

:: deftheorem Def7 defines Quadr2 LATTICE8:def 7 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal st O in dom q holds
Quadr2 q,O = q . O;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta2 q,O -> set means :Def8: :: LATTICE8:def 8
ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 (BiFun (L0 . C),(ConsecutiveSet2 A,C),L),(Quadr2 q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 (BiFun (L0 . C),(ConsecutiveSet2 A,C),L),(Quadr2 q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) )
;
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 (BiFun (L0 . C),(ConsecutiveSet2 A,C),L),(Quadr2 q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 (BiFun (L0 . C),(ConsecutiveSet2 A,C),L),(Quadr2 q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines ConsecutiveDelta2 LATTICE8:def 8 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal
for b6 being set holds
( b6 = ConsecutiveDelta2 q,O iff ex L0 being T-Sequence st
( b6 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 (BiFun (L0 . C),(ConsecutiveSet2 A,C),L),(Quadr2 q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th19: :: LATTICE8:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta2 q,{} = d
proof end;

theorem Th20: :: LATTICE8:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,(succ O) = new_bi_fun2 (BiFun (ConsecutiveDelta2 q,O),(ConsecutiveSet2 A,O),L),(Quadr2 q,O)
proof end;

theorem Th21: :: LATTICE8:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for T being T-Sequence
for O being Ordinal st O <> {} & O is_limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta2 q,O1 ) holds
ConsecutiveDelta2 q,O = union (rng T)
proof end;

theorem Th22: :: LATTICE8:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for O, O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet2 A,O1 c= ConsecutiveSet2 A,O2
proof end;

theorem Th23: :: LATTICE8:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
:: original: ConsecutiveDelta2
redefine func ConsecutiveDelta2 q,O -> BiFunction of (ConsecutiveSet2 A,O),L;
coherence
ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
by Th23;
end;

theorem Th24: :: LATTICE8:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds d c= ConsecutiveDelta2 q,O
proof end;

theorem Th25: :: LATTICE8:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for O1, O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 q,O1 c= ConsecutiveDelta2 q,O2
proof end;

theorem Th26: :: LATTICE8:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is zeroed
proof end;

theorem Th27: :: LATTICE8:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric
proof end;

theorem Th28: :: LATTICE8:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 q,O is u.t.i.
proof end;

theorem :: LATTICE8:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 q,O is distance_function of (ConsecutiveSet2 A,O),L by Th26, Th27, Th28;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet2 d -> set equals :: LATTICE8:def 9
ConsecutiveSet2 A,(DistEsti d);
correctness
coherence
ConsecutiveSet2 A,(DistEsti d) is set
;
;
end;

:: deftheorem defines NextSet2 LATTICE8:def 9 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L holds NextSet2 d = ConsecutiveSet2 A,(DistEsti d);

registration
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet2 d -> non empty ;
coherence
not NextSet2 d is empty
;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta2 q -> set equals :: LATTICE8:def 10
ConsecutiveDelta2 q,(DistEsti d);
correctness
coherence
ConsecutiveDelta2 q,(DistEsti d) is set
;
;
end;

:: deftheorem defines NextDelta2 LATTICE8:def 10 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds NextDelta2 q = ConsecutiveDelta2 q,(DistEsti d);

definition
let A be non empty set ;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
:: original: NextDelta2
redefine func NextDelta2 q -> distance_function of (NextSet2 d),L;
coherence
NextDelta2 q is distance_function of (NextSet2 d),L
by Th26, Th27, Th28;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set ;
let dq be distance_function of Aq,L;
pred Aq,dq is_extension2_of A,d means :Def11: :: LATTICE8:def 11
ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q );
end;

:: deftheorem Def11 defines is_extension2_of LATTICE8:def 11 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( Aq,dq is_extension2_of A,d iff ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q ) );

theorem Th30: :: LATTICE8:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . x,y <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . x,z1 = a & dq . z1,z2 = ((d . x,y) "\/" a) "/\" b & dq . z2,y = a )
proof end;

definition
let A be non empty set ;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq2 of A,d -> Function means :Def12: :: LATTICE8:def 12
( dom it = NAT & it . 0 = [A,d] & ( for n being Nat ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A',d' & it . n = [A',d'] & it . (n + 1) = [Aq,dq] ) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Nat ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A',d' & b1 . n = [A',d'] & b1 . (n + 1) = [Aq,dq] ) ) )
proof end;
end;

:: deftheorem Def12 defines ExtensionSeq2 LATTICE8:def 12 :
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for b4 being Function holds
( b4 is ExtensionSeq2 of A,d iff ( dom b4 = NAT & b4 . 0 = [A,d] & ( for n being Nat ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A',d' & b4 . n = [A',d'] & b4 . (n + 1) = [Aq,dq] ) ) ) );

theorem Th31: :: LATTICE8:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1
proof end;

theorem Th32: :: LATTICE8:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2
proof end;

theorem Th33: :: LATTICE8:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) `1 ) where i is Nat : verum } holds
union { ((S . i) `2 ) where i is Nat : verum } is distance_function of FS,L
proof end;

theorem Th34: :: LATTICE8:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1 ) where i is Nat : verum } & FD = union { ((S . i) `2 ) where i is Nat : verum } & FD . x,y <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
proof end;

Lm3: for m being Nat holds
( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )
proof end;

Lm4: for j being Nat st 1 <= j & j < 4 & not j = 1 & not j = 2 holds
j = 3
proof end;

theorem Th35: :: LATTICE8:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for f being Homomorphism of L,(EqRelLATT FS)
for e1, e2 being Equivalence_Relation of FS
for x, y being set st f = alpha FD & FS = union { ((S . i) `1 ) where i is Nat : verum } & FD = union { ((S . i) `2 ) where i is Nat : verum } & e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 2 + 2 & x,y are_joint_by F,e1,e2 )
proof end;

theorem Th36: :: LATTICE8:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2
proof end;

theorem :: LATTICE8:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded LATTICE holds
( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th36;