:: On Weakly Associative Lattices and Near Lattices
:: by Damian Sawicki and Adam Grabowski
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


:: WAL + v0"/\"(v1"\/"(v0"\/"v2)) = v0 => LT
:: WAL-1
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)
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)
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
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
proof end;

definition
let L be non empty LattStr ;
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;
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;
end;

:: 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 );

:: 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 );

definition
let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;
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
( L is satisfying_W3 iff for v2, v1, v0 being Element of L holds v1 [= (v0 "\/" v1) "/\" (v2 "\/" v1) )
proof end;
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) );

definition
let L be non empty LattStr ;
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
( L is satisfying_W3' iff for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" v1) [= v1 )
proof end;
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 );

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
cluster non empty join-commutative meet-commutative join-idempotent satisfying_W3' -> non empty meet-Absorbing for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-commutative & b1 is join-idempotent & b1 is join-commutative & b1 is satisfying_W3' holds
b1 is meet-Absorbing
by Lemma44;
end;

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
cluster non empty join-commutative meet-commutative meet-idempotent satisfying_W3 -> non empty join-absorbing for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-commutative & b1 is meet-idempotent & b1 is join-commutative & b1 is satisfying_W3 holds
b1 is join-absorbing
by Lemma441;
end;

registration
cluster non empty trivial -> non empty satisfying_W3' for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
b1 is satisfying_W3'
by STRUCT_0:def 10;
end;

registration
cluster non empty join-commutative meet-commutative join-idempotent meet-idempotent satisfying_W3 satisfying_W3' for LattStr ;
existence
ex b1 being non empty LattStr st
( b1 is satisfying_W3 & b1 is satisfying_W3' & b1 is join-idempotent & b1 is meet-idempotent & b1 is join-commutative & b1 is meet-commutative )
proof end;
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
definition
mode WA_Lattice is WeaklyAssociativeLattice;
end;

:: Every lattice is weakly associative lattice
registration
cluster non empty join-associative meet-absorbing Lattice-like -> join-associative meet-absorbing satisfying_W3' for LattStr ;
coherence
for b1 being join-associative meet-absorbing Lattice holds b1 is satisfying_W3'
proof end;
end;

definition
let L be non empty LattStr ;
attr L is satisfying_WA means :: LATWAL_1:def 5
for x, y, z being Element of L holds x "/\" (y "\/" (x "\/" z)) = x;
end;

:: 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 );

registration
cluster non empty join-commutative meet-commutative meet-Absorbing -> non empty meet-absorbing for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-Absorbing & b1 is meet-commutative & b1 is join-commutative holds
b1 is meet-absorbing
proof end;
end;

registration
cluster non empty join-commutative meet-commutative join-idempotent meet-idempotent satisfying_W3 satisfying_W3' -> meet-absorbing for LattStr ;
coherence
for b1 being WA_Lattice holds b1 is meet-absorbing
;
end;

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;

theorem :: LATWAL_1:6
for L being WA_Lattice
for x, y being Element of L holds
( x "/\" y = x iff x [= y ) by LATTICES:4;

theorem :: LATWAL_1:7
for L being WA_Lattice
for x being Element of L holds x [= x ;

theorem :: LATWAL_1:8
for L being WA_Lattice
for x, y being Element of L st x [= y & y [= x holds
x = y by LATTICES:8;

theorem LemmaSum: :: LATWAL_1:9
for L being WA_Lattice
for x, y being Element of L holds x [= x "\/" y
proof end;

theorem Lemacik3: :: LATWAL_1:10
for L being WA_Lattice
for x, y being Element of L holds x "/\" y [= x
proof end;

theorem Lemacik1: :: LATWAL_1:11
for L being WA_Lattice
for x, y, z being Element of L st x [= z & y [= z holds
x "\/" y [= z
proof end;

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 ) )
proof end;

theorem Lemacik2: :: LATWAL_1:13
for L being WA_Lattice
for x, y, z being Element of L st z [= x & z [= y holds
z [= x "/\" y
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 ) )
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)
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)
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
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)
proof end;

:: If we assume distributivity (actually one of them), we get full
:: lattice (via the associativity).
registration
cluster non empty join-commutative meet-commutative join-idempotent distributive' meet-idempotent satisfying_W3 satisfying_W3' -> join-associative for LattStr ;
coherence
for b1 being WA_Lattice st b1 is distributive' holds
b1 is join-associative
proof end;
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};
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
( ( ( ( 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 b1 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 ( b1 = 2 iff b1 = min (x,y) ) )
;
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
( ( ( ( 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 b1 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 ( b1 = 0 iff b1 = max (x,y) ) )
;
end;

:: 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) ) );

:: 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) ) );

definition
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
ex b1 being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds b1 . (x,y) = x ex123"\/" y
proof end;
uniqueness
for b1, b2 being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds b1 . (x,y) = x ex123"\/" y ) & ( for x, y being Element of {0,1,2} holds b2 . (x,y) = x ex123"\/" y ) holds
b1 = b2
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
ex b1 being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds b1 . (x,y) = x ex123"/\" y
proof end;
uniqueness
for b1, b2 being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds b1 . (x,y) = x ex123"/\" y ) & ( for x, y being Element of {0,1,2} holds b2 . (x,y) = x ex123"/\" y ) holds
b1 = b2
proof end;
end;

:: deftheorem EXUDef defines ex123\/ LATWAL_1:def 8 :
for b1 being BinOp of {0,1,2} holds
( b1 = ex123\/ iff for x, y being Element of {0,1,2} holds b1 . (x,y) = x ex123"\/" y );

:: deftheorem EXNDef defines ex123/\ LATWAL_1:def 9 :
for b1 being BinOp of {0,1,2} holds
( b1 = ex123/\ iff for x, y being Element of {0,1,2} holds b1 . (x,y) = x ex123"/\" y );

:: Here the example of the near lattice. We should show
:: that it breaks one of the lattice axioms
definition
func ExNearLattice -> non empty LattStr equals :: LATWAL_1:def 10
LattStr(# {0,1,2},ex123\/,ex123/\ #);
coherence
LattStr(# {0,1,2},ex123\/,ex123/\ #) is non empty LattStr
;
end;

:: deftheorem defines ExNearLattice LATWAL_1:def 10 :
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
cluster ExNearLattice -> non empty non join-associative non meet-associative ;
coherence
( not ExNearLattice is join-associative & not ExNearLattice is meet-associative )
by Cosik1, Cosik2;
end;

registration
cluster non empty trivial -> non empty join-commutative join-absorbing meet-idempotent meet-Absorbing for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is meet-idempotent & b1 is join-commutative & b1 is meet-Absorbing & b1 is join-absorbing )
;
end;

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
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;
end;

registration
cluster non empty join-commutative meet-commutative meet-absorbing -> non empty join-commutative meet-commutative meet-Absorbing for LattStr ;
coherence
for b1 being non empty join-commutative meet-commutative LattStr st b1 is meet-absorbing holds
b1 is meet-Absorbing
proof end;
cluster non empty join-commutative meet-commutative meet-Absorbing -> non empty join-commutative meet-commutative meet-absorbing for LattStr ;
coherence
for b1 being non empty join-commutative meet-commutative LattStr st b1 is meet-Absorbing holds
b1 is meet-absorbing
;
end;

theorem :: LATWAL_1:19
( ExNearLattice is NearLattice & ExNearLattice is not Lattice ) ;

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
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
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
proof end;

definition
let L be non empty LattStr ;
attr L is satisfying_WAL31 means :: LATWAL_1:def 11
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;
attr L is satisfying_WAL33 means :: LATWAL_1:def 13
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;
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;
end;

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

registration
cluster non empty trivial -> non empty satisfying_WAL31 satisfying_WAL32 satisfying_WAL33 satisfying_WAL34 satisfying_WAL35 for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is satisfying_WAL31 & b1 is satisfying_WAL32 & b1 is satisfying_WAL33 & b1 is satisfying_WAL34 & b1 is satisfying_WAL35 )
by STRUCT_0:def 10;
end;

registration
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 b1 being non empty LattStr st b1 is satisfying_WAL31 & b1 is satisfying_WAL32 & b1 is satisfying_WAL33 & b1 is satisfying_WAL34 & b1 is satisfying_WAL35 holds
( b1 is join-idempotent & b1 is meet-idempotent & b1 is join-commutative & b1 is meet-commutative )
proof end;
end;

definition
let L be non empty LattStr ;
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;
end;

:: 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 );

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
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
proof end;

registration
cluster non empty trivial -> non empty satisfying_WAL4 for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
b1 is satisfying_WAL4
by STRUCT_0:def 10;
end;

registration
cluster non empty satisfying_WAL4 -> non empty join-idempotent meet-idempotent for LattStr ;
coherence
for b1 being non empty LattStr st b1 is satisfying_WAL4 holds
( b1 is join-idempotent & b1 is meet-idempotent )
by Lemma2, LemmaW1;
end;