:: by Dominik Kulesza and Adam Grabowski

::

:: Received May 31, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

definition

let L be non empty LattStr ;

end;
attr L is satisfying_QLT1 means :: LATQUASI:def 1

for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2);

for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2);

attr L is satisfying_QLT2 means :: LATQUASI:def 2

for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2);

for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2);

attr L is QLT-distributive means :: LATQUASI:def 3

for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2);

for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2);

:: deftheorem defines satisfying_QLT1 LATQUASI:def 1 :

for L being non empty LattStr holds

( L is satisfying_QLT1 iff for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) );

for L being non empty LattStr holds

( L is satisfying_QLT1 iff for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) );

:: deftheorem defines satisfying_QLT2 LATQUASI:def 2 :

for L being non empty LattStr holds

( L is satisfying_QLT2 iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) );

for L being non empty LattStr holds

( L is satisfying_QLT2 iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) );

:: deftheorem defines QLT-distributive LATQUASI:def 3 :

for L being non empty LattStr holds

( L is QLT-distributive iff for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) );

for L being non empty LattStr holds

( L is QLT-distributive iff for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) );

registration

for b_{1} being non empty LattStr st b_{1} is trivial holds

( b_{1} is satisfying_QLT1 & b_{1} is satisfying_QLT2 & b_{1} is QLT-distributive )
by STRUCT_0:def 10;

end;

cluster non empty trivial -> non empty satisfying_QLT1 satisfying_QLT2 QLT-distributive for LattStr ;

coherence for b

( b

registration

coherence

for b_{1} being non empty LattStr st b_{1} is trivial holds

( b_{1} is join-idempotent & b_{1} is meet-idempotent )

end;
for b

( b

proof end;

registration

ex b_{1} being non empty LattStr st

( b_{1} is join-commutative & b_{1} is join-associative & b_{1} is join-idempotent & b_{1} is meet-commutative & b_{1} is meet-associative & b_{1} is meet-idempotent & b_{1} is satisfying_QLT1 & b_{1} is satisfying_QLT2 )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 for LattStr ;

existence ex b

( b

proof end;

definition

let L be non empty join-commutative LattStr ;

( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) )

end;
redefine attr L is satisfying_QLT1 means :: LATQUASI:def 4

for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2);

compatibility for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2);

( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) )

proof end;

:: deftheorem defines satisfying_QLT1 LATQUASI:def 4 :

for L being non empty join-commutative LattStr holds

( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) );

for L being non empty join-commutative LattStr holds

( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) );

T2: for x, y being Element of {0,1,2} holds min (x,y) in {0,1,2}

proof end;

definition

let x, y be Element of {0,1,2};

( ( ( x = 1 or y = 1 ) implies 1 is Element of {0,1,2} ) & ( x <> 1 & y <> 1 implies min (x,y) is Element of {0,1,2} ) ) by T2;

consistency

for b_{1} being Element of {0,1,2} st ( x = 1 or y = 1 ) & x <> 1 & y <> 1 holds

( b_{1} = 1 iff b_{1} = min (x,y) )
;

end;
func OpEx2 (x,y) -> Element of {0,1,2} equals :OpEx2Def: :: LATQUASI:def 5

1 if ( x = 1 or y = 1 )

min (x,y) if ( x <> 1 & y <> 1 )

;

coherence 1 if ( x = 1 or y = 1 )

min (x,y) if ( x <> 1 & y <> 1 )

;

( ( ( x = 1 or y = 1 ) implies 1 is Element of {0,1,2} ) & ( x <> 1 & y <> 1 implies min (x,y) is Element of {0,1,2} ) ) by T2;

consistency

for b

( b

:: deftheorem OpEx2Def defines OpEx2 LATQUASI:def 5 :

for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies OpEx2 (x,y) = 1 ) & ( x <> 1 & y <> 1 implies OpEx2 (x,y) = min (x,y) ) );

for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies OpEx2 (x,y) = 1 ) & ( x <> 1 & y <> 1 implies OpEx2 (x,y) = min (x,y) ) );

definition

ex b_{1} being BinOp of {0,1,2} st

for x, y being Element of {0,1,2} holds

( ( x = y implies b_{1} . (x,y) = x ) & ( x <> y implies b_{1} . (x,y) = 0 ) )

for b_{1}, b_{2} being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds

( ( x = y implies b_{1} . (x,y) = x ) & ( x <> y implies b_{1} . (x,y) = 0 ) ) ) & ( for x, y being Element of {0,1,2} holds

( ( x = y implies b_{2} . (x,y) = x ) & ( x <> y implies b_{2} . (x,y) = 0 ) ) ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of {0,1,2} st

for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies b_{1} . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b_{1} . (x,y) = min (x,y) ) )

for b_{1}, b_{2} being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies b_{1} . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b_{1} . (x,y) = min (x,y) ) ) ) & ( for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies b_{2} . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b_{2} . (x,y) = min (x,y) ) ) ) holds

b_{1} = b_{2}
end;

func QLT_Ex1 -> BinOp of {0,1,2} means :QLTEx1Def: :: LATQUASI:def 6

for x, y being Element of {0,1,2} holds

( ( x = y implies it . (x,y) = x ) & ( x <> y implies it . (x,y) = 0 ) );

existence for x, y being Element of {0,1,2} holds

( ( x = y implies it . (x,y) = x ) & ( x <> y implies it . (x,y) = 0 ) );

ex b

for x, y being Element of {0,1,2} holds

( ( x = y implies b

proof end;

uniqueness for b

( ( x = y implies b

( ( x = y implies b

b

proof end;

func QLT_Ex2 -> BinOp of {0,1,2} means :QLTEx2Def: :: LATQUASI:def 7

for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies it . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies it . (x,y) = min (x,y) ) );

existence for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies it . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies it . (x,y) = min (x,y) ) );

ex b

for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies b

proof end;

uniqueness for b

( ( ( x = 1 or y = 1 ) implies b

( ( ( x = 1 or y = 1 ) implies b

b

proof end;

:: deftheorem QLTEx1Def defines QLT_Ex1 LATQUASI:def 6 :

for b_{1} being BinOp of {0,1,2} holds

( b_{1} = QLT_Ex1 iff for x, y being Element of {0,1,2} holds

( ( x = y implies b_{1} . (x,y) = x ) & ( x <> y implies b_{1} . (x,y) = 0 ) ) );

for b

( b

( ( x = y implies b

:: deftheorem QLTEx2Def defines QLT_Ex2 LATQUASI:def 7 :

for b_{1} being BinOp of {0,1,2} holds

( b_{1} = QLT_Ex2 iff for x, y being Element of {0,1,2} holds

( ( ( x = 1 or y = 1 ) implies b_{1} . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b_{1} . (x,y) = min (x,y) ) ) );

for b

( b

( ( ( x = 1 or y = 1 ) implies b

definition

LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #) is non empty strict LattStr ;

LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #) is non empty strict LattStr ;

end;

func QLTLattice1 -> non empty strict LattStr equals :: LATQUASI:def 8

LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

coherence LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #) is non empty strict LattStr ;

func QLTLattice2 -> non empty strict LattStr equals :: LATQUASI:def 9

LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

coherence LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #) is non empty strict LattStr ;

:: deftheorem defines QLTLattice1 LATQUASI:def 8 :

QLTLattice1 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

QLTLattice1 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

:: deftheorem defines QLTLattice2 LATQUASI:def 9 :

QLTLattice2 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

QLTLattice2 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

registration
end;

registration
end;

registration

coherence

( QLTLattice1 is join-commutative & QLTLattice1 is join-associative & QLTLattice1 is join-idempotent )

end;
( QLTLattice1 is join-commutative & QLTLattice1 is join-associative & QLTLattice1 is join-idempotent )

proof end;

registration

coherence

( QLTLattice1 is meet-commutative & QLTLattice1 is meet-associative & QLTLattice1 is meet-idempotent )

end;
( QLTLattice1 is meet-commutative & QLTLattice1 is meet-associative & QLTLattice1 is meet-idempotent )

proof end;

:: Every QLTLattice is QuasiLattice

registration

coherence

( QLTLattice2 is join-commutative & QLTLattice2 is join-associative & QLTLattice2 is join-idempotent )

end;
( QLTLattice2 is join-commutative & QLTLattice2 is join-associative & QLTLattice2 is join-idempotent )

proof end;

registration

coherence

( QLTLattice2 is meet-commutative & QLTLattice2 is meet-associative & QLTLattice2 is meet-idempotent )

end;
( QLTLattice2 is meet-commutative & QLTLattice2 is meet-associative & QLTLattice2 is meet-idempotent )

proof end;

registration

coherence

not QLTLattice2 is join-absorbing

not QLTLattice2 is meet-absorbing

end;
not QLTLattice2 is join-absorbing

proof end;

coherence not QLTLattice2 is meet-absorbing

proof end;

registration

coherence

not QLTLattice1 is join-absorbing

not QLTLattice1 is meet-absorbing

end;
not QLTLattice1 is join-absorbing

proof end;

coherence not QLTLattice1 is meet-absorbing

proof end;

definition

mode QuasiLattice is non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr ;

end;
:: In QLT-1 we don't need two QLT axioms:

:: for v0 holds v0"/\"v0 = v0 & :: /\-idempotent

:: (for v2,v1,v0 holds

:: (v0"/\"v1)"/\"v2 = v0"/\"(v1"/\"v2)) & :: /\-associative

:: for v0 holds v0"/\"v0 = v0 & :: /\-idempotent

:: (for v2,v1,v0 holds

:: (v0"/\"v1)"/\"v2 = v0"/\"(v1"/\"v2)) & :: /\-associative

theorem Lemma1: :: LATQUASI:4

for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) ) holds

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3)

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3)

proof end;

theorem Cluster1: :: LATQUASI:5

for L being non empty LattStr st L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-distributive holds

L is distributive

L is distributive

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-commutative & b_{1} is satisfying_QLT1 & b_{1} is join-idempotent & b_{1} is join-associative & b_{1} is join-commutative & b_{1} is satisfying_QLT2 & b_{1} is QLT-distributive holds

b_{1} is distributive
by Cluster1;

end;

cluster non empty join-commutative join-associative meet-commutative join-idempotent satisfying_QLT1 satisfying_QLT2 QLT-distributive -> non empty distributive for LattStr ;

coherence for b

b

theorem ThQLT2: :: LATQUASI:6

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) holds

for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

proof end;

theorem Cluster2: :: LATQUASI:7

for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is join-idempotent & L is join-associative & L is satisfying_QLT2 & L is distributive holds

L is distributive'

L is distributive'

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-idempotent & b_{1} is meet-associative & b_{1} is meet-commutative & b_{1} is join-idempotent & b_{1} is join-associative & b_{1} is satisfying_QLT2 & b_{1} is distributive holds

b_{1} is distributive'
by Cluster2;

end;

cluster non empty join-associative meet-commutative meet-associative distributive join-idempotent meet-idempotent satisfying_QLT2 -> non empty distributive' for LattStr ;

coherence for b

b

:: deftheorem defines QLT-selfdistributive LATQUASI:def 10 :

for L being non empty LattStr holds

( L is QLT-selfdistributive iff for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) );

for L being non empty LattStr holds

( L is QLT-selfdistributive iff for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) );

theorem ThQLT3: :: LATQUASI:8

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) ) holds

for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

proof end;

Cluster3: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfdistributive holds

L is distributive'

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-idempotent & b_{1} is meet-associative & b_{1} is meet-commutative & b_{1} is satisfying_QLT1 & b_{1} is join-idempotent & b_{1} is join-associative & b_{1} is join-commutative & b_{1} is satisfying_QLT2 & b_{1} is QLT-selfdistributive holds

b_{1} is distributive'
by Cluster3;

end;

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfdistributive -> non empty distributive' for LattStr ;

coherence for b

b

definition

let L be non empty LattStr ;

end;
attr L is satisfying_Bowden_inequality means :: LATQUASI:def 11

for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z);

for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z);

:: deftheorem defines satisfying_Bowden_inequality LATQUASI:def 11 :

for L being non empty LattStr holds

( L is satisfying_Bowden_inequality iff for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z) );

for L being non empty LattStr holds

( L is satisfying_Bowden_inequality iff for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z) );

definition

let L be non empty join-commutative LattStr ;

( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) )

end;
redefine attr L is satisfying_Bowden_inequality means :BowdenRedef: :: LATQUASI:def 12

for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2);

compatibility for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2);

( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) )

proof end;

:: deftheorem BowdenRedef defines satisfying_Bowden_inequality LATQUASI:def 12 :

for L being non empty join-commutative LattStr holds

( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) );

for L being non empty join-commutative LattStr holds

( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) );

theorem ThQLT4: :: LATQUASI:9

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) ) holds

for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)

proof end;

Cluster4: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is satisfying_Bowden_inequality holds

L is distributive'

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-idempotent & b_{1} is meet-associative & b_{1} is meet-commutative & b_{1} is satisfying_QLT1 & b_{1} is join-idempotent & b_{1} is join-associative & b_{1} is join-commutative & b_{1} is satisfying_QLT2 & b_{1} is satisfying_Bowden_inequality holds

b_{1} is distributive'
by Cluster4;

end;

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 satisfying_Bowden_inequality -> non empty distributive' for LattStr ;

coherence for b

b

:: deftheorem defines QLT-selfmodular LATQUASI:def 13 :

for L being non empty LattStr holds

( L is QLT-selfmodular iff for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) );

for L being non empty LattStr holds

( L is QLT-selfmodular iff for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) );

definition

let L be non empty join-idempotent LattStr ;

let a, b be Element of L;

:: original: [=

redefine pred a [= b;

reflexivity

for a being Element of L holds R29(L,b_{1},b_{1})

end;
let a, b be Element of L;

:: original: [=

redefine pred a [= b;

reflexivity

for a being Element of L holds R29(L,b

proof end;

:: Modularity for Quasilattices

theorem QLTMod: :: LATQUASI:10

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v1, v2 being Element of L st v0 "\/" v1 = v1 holds

v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) holds

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) holds

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

ClusterA: for L being non empty LattStr st L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & L is modular holds

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

theorem QLTMod2: :: LATQUASI:11

for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) holds

for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds

v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2

for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds

v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2

proof end;

ClusterB: for L being non empty LattStr st L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) holds

L is modular

proof end;

definition

let L be non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr ;

( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )

end;
redefine attr L is modular means :ModRedef: :: LATQUASI:def 14

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3));

compatibility for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3));

( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )

proof end;

:: deftheorem ModRedef defines modular LATQUASI:def 14 :

for L being non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr holds

( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) );

for L being non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr holds

( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) );

theorem ThQLT5: :: LATQUASI:12

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) ) holds

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

Cluster5: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfmodular holds

L is modular

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-idempotent & b_{1} is meet-associative & b_{1} is meet-commutative & b_{1} is satisfying_QLT1 & b_{1} is join-idempotent & b_{1} is join-associative & b_{1} is join-commutative & b_{1} is satisfying_QLT2 & b_{1} is QLT-selfmodular holds

b_{1} is modular
by Cluster5;

end;

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfmodular -> non empty modular for LattStr ;

coherence for b

b

theorem ThQLT6: :: LATQUASI:13

for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 ) holds

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

:: deftheorem defines QLT-selfmodular' LATQUASI:def 15 :

for L being non empty LattStr holds

( L is QLT-selfmodular' iff for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 );

for L being non empty LattStr holds

( L is QLT-selfmodular' iff for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 );

Cluster6: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfmodular' holds

L is modular

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-idempotent & b_{1} is meet-associative & b_{1} is meet-commutative & b_{1} is satisfying_QLT1 & b_{1} is join-idempotent & b_{1} is join-associative & b_{1} is join-commutative & b_{1} is satisfying_QLT2 & b_{1} is QLT-selfmodular' holds

b_{1} is modular
by Cluster6;

end;

cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfmodular' -> non empty modular for LattStr ;

coherence for b

b

theorem :: LATQUASI:14

ex L1, L2 being QuasiLattice st

( the carrier of L1 = the carrier of L2 & the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )

( the carrier of L1 = the carrier of L2 & the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )

proof end;

:: x <= y iff x "\/" y = y

::: if absorption is true, then x <= y iff x "/\" y = x