:: by Damian Sawicki and Adam Grabowski

::

:: Received June 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

theorem :: LATWAL_1:1

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 being Element of L holds v0 "\/" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) holds

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

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

proof end;

:: Associativity

theorem :: LATWAL_1:2

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 being Element of L holds v0 "\/" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) holds

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

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

proof end;

:: Third

theorem :: LATWAL_1:3

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

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

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

proof end;

:: Fourth

theorem Lemma4: :: LATWAL_1:4

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

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

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

proof end;

definition

let L be non empty LattStr ;

end;
attr L is satisfying_W3 means :DefW3: :: LATWAL_1:def 1

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

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

attr L is satisfying_W3' means :DefW33: :: LATWAL_1:def 2

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

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

:: deftheorem DefW3 defines satisfying_W3 LATWAL_1:def 1 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

:: deftheorem DefW33 defines satisfying_W3' LATWAL_1:def 2 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

definition

let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;

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

end;
redefine attr L is satisfying_W3 means :defW3: :: LATWAL_1:def 3

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

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

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

proof end;

:: deftheorem defW3 defines satisfying_W3 LATWAL_1:def 3 :

for L being non empty meet-commutative meet-absorbing join-absorbing LattStr holds

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

for L being non empty meet-commutative meet-absorbing join-absorbing LattStr holds

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

definition

let L be non empty LattStr ;

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

end;
redefine attr L is satisfying_W3' means :defW33: :: LATWAL_1:def 4

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

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

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

proof end;

:: deftheorem defW33 defines satisfying_W3' LATWAL_1:def 4 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

Lemma44: for L being non empty LattStr st L is meet-commutative & L is join-idempotent & L is join-commutative & L is satisfying_W3' holds

L is meet-Absorbing

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is meet-commutative & b_{1} is join-idempotent & b_{1} is join-commutative & b_{1} is satisfying_W3' holds

b_{1} is meet-Absorbing
by Lemma44;

end;

cluster non empty join-commutative meet-commutative join-idempotent satisfying_W3' -> non empty meet-Absorbing for LattStr ;

coherence for b

b

Lemma441: for L being non empty LattStr st L is meet-commutative & L is meet-idempotent & L is join-commutative & L is satisfying_W3 holds

L is join-absorbing

proof end;

registration

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

b_{1} is join-absorbing
by Lemma441;

end;

cluster non empty join-commutative meet-commutative meet-idempotent satisfying_W3 -> non empty join-absorbing for LattStr ;

coherence for b

b

registration

coherence

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

b_{1} is satisfying_W3'
by STRUCT_0:def 10;

end;
for b

b

registration

ex b_{1} being non empty LattStr st

( b_{1} is satisfying_W3 & b_{1} is satisfying_W3' & b_{1} is join-idempotent & b_{1} is meet-idempotent & b_{1} is join-commutative & b_{1} is meet-commutative )
end;

cluster non empty join-commutative meet-commutative join-idempotent meet-idempotent satisfying_W3 satisfying_W3' for LattStr ;

existence ex b

( b

proof end;

definition

mode WeaklyAssociativeLattice is non empty join-commutative meet-commutative join-idempotent meet-idempotent satisfying_W3 satisfying_W3' LattStr ;

end;
:: The above definition is taken from Padmanabhan and Rudeanu, Chapter 6

:: x ^ x = x x v x = x

:: x ^ y = y ^ x x v y = y v x

:: ((x v z) ^ (y v z)) ^ z = z ((x ^ z) v (y ^ z)) v z = z

::

:: but

::

:: Fried and Gratzer Some Examples of Weakly Associative Lattices states that

:: x ^ x = x x v x = x

:: x ^ y = y ^ x x v y = y v x

:: x ^ (x v y) = x x v (x ^ y) = x

:: ((x v z) ^ (y v z)) ^ z = z ((x ^ z) v (y ^ z)) v z = z

:: weak-associative identities

:: Absorption law can be derived from these

:: x ^ x = x x v x = x

:: x ^ y = y ^ x x v y = y v x

:: ((x v z) ^ (y v z)) ^ z = z ((x ^ z) v (y ^ z)) v z = z

::

:: but

::

:: Fried and Gratzer Some Examples of Weakly Associative Lattices states that

:: x ^ x = x x v x = x

:: x ^ y = y ^ x x v y = y v x

:: x ^ (x v y) = x x v (x ^ y) = x

:: ((x v z) ^ (y v z)) ^ z = z ((x ^ z) v (y ^ z)) v z = z

:: weak-associative identities

:: Absorption law can be derived from these

:: Every lattice is weakly associative lattice

registration

for b_{1} being join-associative meet-absorbing Lattice holds b_{1} is satisfying_W3'
end;

cluster non empty join-associative meet-absorbing Lattice-like -> join-associative meet-absorbing satisfying_W3' for LattStr ;

coherence for b

proof end;

definition

let L be non empty LattStr ;

end;
attr L is satisfying_WA means :: LATWAL_1:def 5

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

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

:: deftheorem defines satisfying_WA LATWAL_1:def 5 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

registration

for b_{1} being non empty LattStr st b_{1} is meet-Absorbing & b_{1} is meet-commutative & b_{1} is join-commutative holds

b_{1} is meet-absorbing
end;

cluster non empty join-commutative meet-commutative meet-Absorbing -> non empty meet-absorbing for LattStr ;

coherence for b

b

proof end;

registration

for b_{1} being WA_Lattice holds b_{1} is meet-absorbing
;

end;

cluster non empty join-commutative meet-commutative join-idempotent meet-idempotent satisfying_W3 satisfying_W3' -> meet-absorbing for LattStr ;

coherence for b

theorem :: LATWAL_1:5

for L being WA_Lattice

for x, y being Element of L holds

( x "\/" y = y iff x [= y ) by LATTICES:def 3;

for x, y being Element of L holds

( x "\/" y = y iff x [= y ) by LATTICES:def 3;

theorem :: LATWAL_1:6

theorem :: LATWAL_1:8

theorem :: LATWAL_1:12

for L being WA_Lattice

for x, y being Element of L ex z being Element of L st

( x [= z & y [= z & ( for u being Element of L st x [= u & y [= u holds

z [= u ) )

for x, y being Element of L ex z being Element of L st

( x [= z & y [= z & ( for u being Element of L st x [= u & y [= u holds

z [= u ) )

proof end;

theorem :: LATWAL_1:14

for L being WA_Lattice

for x, y being Element of L ex z being Element of L st

( z [= x & z [= y & ( for u being Element of L st u [= x & u [= y holds

u [= z ) )

for x, y being Element of L ex z being Element of L st

( z [= x & z [= y & ( for u being Element of L st u [= x & u [= y holds

u [= z ) )

proof end;

:: Under the assumption of (4) the following is true:

theorem :: LATWAL_1:15

for L being WA_Lattice

for x, y, z being Element of L st x [= z & y [= z holds

(x "\/" y) "\/" z = x "\/" (y "\/" z)

for x, y, z being Element of L st x [= z & y [= z holds

(x "\/" y) "\/" z = x "\/" (y "\/" z)

proof end;

theorem :: LATWAL_1:16

for L being WA_Lattice

for x, y, z being Element of L st z [= x & z [= y holds

(x "/\" y) "/\" z = x "/\" (y "/\" z)

for x, y, z being Element of L st z [= x & z [= y holds

(x "/\" y) "/\" z = x "/\" (y "/\" z)

proof end;

:: WA-Lattice is a lattice iff [= is transitive

theorem :: LATWAL_1:17

for L being WA_Lattice

for x, y, z being Element of L st L is distributive & x [= y & y [= z holds

x [= z

for x, y, z being Element of L st L is distributive & x [= y & y [= z holds

x [= z

proof end;

theorem WALDistri: :: LATWAL_1:18

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 being Element of L holds v0 "\/" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ) & ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ) holds

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

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

proof end;

:: If we assume distributivity (actually one of them), we get full

:: lattice (via the associativity).

:: lattice (via the associativity).

registration

for b_{1} being WA_Lattice st b_{1} is distributive' holds

b_{1} is join-associative
end;

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

coherence for b

b

proof end;

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

proof end;

Lmy2: ( 2 in {0,1,2} & ( for x, y being Element of {0,1,2} holds max (x,y) in {0,1,2} ) )

proof end;

definition

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

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

consistency

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

( ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) or ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or ( b_{1} = 2 iff b_{1} = min (x,y) ) )
;

( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies 0 is Element of {0,1,2} ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or max (x,y) is Element of {0,1,2} ) ) by Lmy2;

consistency

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

( ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) or ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or ( b_{1} = 0 iff b_{1} = max (x,y) ) )
;

end;
func x ex123"/\" y -> Element of {0,1,2} equals :ExMeetDef: :: LATWAL_1:def 6

2 if ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) )

min (x,y) if ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) )

;

coherence 2 if ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) )

min (x,y) if ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) )

;

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

consistency

for b

( ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) or ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or ( b

func x ex123"\/" y -> Element of {0,1,2} equals :UPDef: :: LATWAL_1:def 7

0 if ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) )

max (x,y) if ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) )

;

coherence 0 if ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) )

max (x,y) if ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) )

;

( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies 0 is Element of {0,1,2} ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or max (x,y) is Element of {0,1,2} ) ) by Lmy2;

consistency

for b

( ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) or ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or ( b

:: deftheorem ExMeetDef defines ex123"/\" LATWAL_1:def 6 :

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

( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies x ex123"/\" y = 2 ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or x ex123"/\" y = min (x,y) ) );

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

( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies x ex123"/\" y = 2 ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or x ex123"/\" y = min (x,y) ) );

:: deftheorem UPDef defines ex123"\/" LATWAL_1:def 7 :

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

( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies x ex123"\/" y = 0 ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or x ex123"\/" y = max (x,y) ) );

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

( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies x ex123"\/" y = 0 ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or x ex123"\/" y = max (x,y) ) );

definition

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

for x, y being Element of {0,1,2} holds b_{1} . (x,y) = x ex123"\/" y

for b_{1}, b_{2} being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds b_{1} . (x,y) = x ex123"\/" y ) & ( for x, y being Element of {0,1,2} holds b_{2} . (x,y) = x ex123"\/" y ) 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 b_{1} . (x,y) = x ex123"/\" y

for b_{1}, b_{2} being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds b_{1} . (x,y) = x ex123"/\" y ) & ( for x, y being Element of {0,1,2} holds b_{2} . (x,y) = x ex123"/\" y ) holds

b_{1} = b_{2}
end;

func ex123\/ -> BinOp of {0,1,2} means :EXUDef: :: LATWAL_1:def 8

for x, y being Element of {0,1,2} holds it . (x,y) = x ex123"\/" y;

existence for x, y being Element of {0,1,2} holds it . (x,y) = x ex123"\/" y;

ex b

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

proof end;

uniqueness for b

b

proof end;

func ex123/\ -> BinOp of {0,1,2} means :EXNDef: :: LATWAL_1:def 9

for x, y being Element of {0,1,2} holds it . (x,y) = x ex123"/\" y;

existence for x, y being Element of {0,1,2} holds it . (x,y) = x ex123"/\" y;

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem EXUDef defines ex123\/ LATWAL_1:def 8 :

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

( b_{1} = ex123\/ iff for x, y being Element of {0,1,2} holds b_{1} . (x,y) = x ex123"\/" y );

for b

( b

:: deftheorem EXNDef defines ex123/\ LATWAL_1:def 9 :

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

( b_{1} = ex123/\ iff for x, y being Element of {0,1,2} holds b_{1} . (x,y) = x ex123"/\" y );

for b

( b

:: Here the example of the near lattice. We should show

:: that it breaks one of the lattice axioms

:: that it breaks one of the lattice axioms

definition

LattStr(# {0,1,2},ex123\/,ex123/\ #) is non empty LattStr ;

end;

func ExNearLattice -> non empty LattStr equals :: LATWAL_1:def 10

LattStr(# {0,1,2},ex123\/,ex123/\ #);

coherence LattStr(# {0,1,2},ex123\/,ex123/\ #);

LattStr(# {0,1,2},ex123\/,ex123/\ #) is non empty LattStr ;

:: deftheorem defines ExNearLattice LATWAL_1:def 10 :

ExNearLattice = LattStr(# {0,1,2},ex123\/,ex123/\ #);

ExNearLattice = LattStr(# {0,1,2},ex123\/,ex123/\ #);

ExJoinAbs: ExNearLattice is join-absorbing

proof end;

ExMeetAbs: ExNearLattice is meet-absorbing

proof end;

Lemacik1: for x, y being Element of ExNearLattice holds ex123/\ . (x,y) = ex123/\ . (y,x)

proof end;

Lemacik1A: for x, y being Element of ExNearLattice holds ex123\/ . (x,y) = ex123\/ . (y,x)

proof end;

Cosik1: not ExNearLattice is join-associative

proof end;

Cosik2: not ExNearLattice is meet-associative

proof end;

registration

coherence

( not ExNearLattice is join-associative & not ExNearLattice is meet-associative ) by Cosik1, Cosik2;

end;
( not ExNearLattice is join-associative & not ExNearLattice is meet-associative ) by Cosik1, Cosik2;

registration

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

( b_{1} is meet-idempotent & b_{1} is join-commutative & b_{1} is meet-Absorbing & b_{1} is join-absorbing )
;

end;

cluster non empty trivial -> non empty join-commutative join-absorbing meet-idempotent meet-Absorbing for LattStr ;

coherence for b

( b

definition

mode NearLattice is non empty join-commutative meet-commutative join-absorbing join-idempotent meet-idempotent meet-Absorbing LattStr ;

end;
ExJoinComm: ExNearLattice is join-commutative

proof end;

ExMeetComm: ExNearLattice is meet-commutative

proof end;

registration

( ExNearLattice is join-commutative & ExNearLattice is meet-commutative & ExNearLattice is join-idempotent & ExNearLattice is meet-idempotent & ExNearLattice is join-absorbing & ExNearLattice is meet-absorbing ) by ExJoinComm, ExMeetComm, ExMeetAbs, ExJoinAbs;

end;

cluster ExNearLattice -> non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent meet-idempotent ;

coherence ( ExNearLattice is join-commutative & ExNearLattice is meet-commutative & ExNearLattice is join-idempotent & ExNearLattice is meet-idempotent & ExNearLattice is join-absorbing & ExNearLattice is meet-absorbing ) by ExJoinComm, ExMeetComm, ExMeetAbs, ExJoinAbs;

registration

for b_{1} being non empty join-commutative meet-commutative LattStr st b_{1} is meet-absorbing holds

b_{1} is meet-Absorbing

for b_{1} being non empty join-commutative meet-commutative LattStr st b_{1} is meet-Absorbing holds

b_{1} is meet-absorbing
;

end;

cluster non empty join-commutative meet-commutative meet-absorbing -> non empty join-commutative meet-commutative meet-Absorbing for LattStr ;

coherence for b

b

proof end;

cluster non empty join-commutative meet-commutative meet-Absorbing -> non empty join-commutative meet-commutative meet-absorbing for LattStr ;

coherence for b

b

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

for v0 being Element of L holds v0 "/\" v0 = v0

proof end;

theorem Lemma2: :: LATWAL_1:20

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

for v0 being Element of L holds v0 "\/" v0 = v0

for v0 being Element of L holds v0 "\/" v0 = v0

proof end;

theorem Lemma3: :: LATWAL_1:21

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

for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0

for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0

proof end;

theorem Lemma4: :: LATWAL_1:22

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

for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0

for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0

proof end;

definition

let L be non empty LattStr ;

end;
attr L is satisfying_WAL31 means :: LATWAL_1:def 11

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

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

attr L is satisfying_WAL32 means :: LATWAL_1:def 12

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

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

attr L is satisfying_WAL33 means :: LATWAL_1:def 13

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

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

attr L is satisfying_WAL34 means :: LATWAL_1:def 14

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

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

attr L is satisfying_WAL35 means :: LATWAL_1:def 15

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

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

:: deftheorem defines satisfying_WAL31 LATWAL_1:def 11 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

:: deftheorem defines satisfying_WAL32 LATWAL_1:def 12 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

:: deftheorem defines satisfying_WAL33 LATWAL_1:def 13 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

:: deftheorem defines satisfying_WAL34 LATWAL_1:def 14 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

:: deftheorem defines satisfying_WAL35 LATWAL_1:def 15 :

for L being non empty LattStr holds

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

for L being non empty LattStr holds

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

registration

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

( b_{1} is satisfying_WAL31 & b_{1} is satisfying_WAL32 & b_{1} is satisfying_WAL33 & b_{1} is satisfying_WAL34 & b_{1} is satisfying_WAL35 )
by STRUCT_0:def 10;

end;

cluster non empty trivial -> non empty satisfying_WAL31 satisfying_WAL32 satisfying_WAL33 satisfying_WAL34 satisfying_WAL35 for LattStr ;

coherence for b

( b

registration

for b_{1} being non empty LattStr st b_{1} is satisfying_WAL31 & b_{1} is satisfying_WAL32 & b_{1} is satisfying_WAL33 & b_{1} is satisfying_WAL34 & b_{1} is satisfying_WAL35 holds

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

cluster non empty satisfying_WAL31 satisfying_WAL32 satisfying_WAL33 satisfying_WAL34 satisfying_WAL35 -> non empty join-commutative meet-commutative join-idempotent meet-idempotent for LattStr ;

coherence for b

( b

proof end;

definition

let L be non empty LattStr ;

end;
attr L is satisfying_WAL4 means :: LATWAL_1:def 16

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

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

:: deftheorem defines satisfying_WAL4 LATWAL_1:def 16 :

for L being non empty LattStr holds

( L is satisfying_WAL4 iff for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1 );

for L being non empty LattStr holds

( L is satisfying_WAL4 iff for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1 );

theorem LemmaW1: :: LATWAL_1:23

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

for v0 being Element of L holds v0 "/\" v0 = v0

for v0 being Element of L holds v0 "/\" v0 = v0

proof end;

theorem Lemma2: :: LATWAL_1:24

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

for v0 being Element of L holds v0 "\/" v0 = v0

for v0 being Element of L holds v0 "\/" v0 = v0

proof end;

registration

coherence

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

b_{1} is satisfying_WAL4
by STRUCT_0:def 10;

end;
for b

b

registration

coherence

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

( b_{1} is join-idempotent & b_{1} is meet-idempotent )
by Lemma2, LemmaW1;

end;
for b

( b

:: WAL-1