:: 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 b₁ being non empty LattStr st b₁ is meet-commutative & b₁ is join-idempotent & b₁ is join-commutative & b₁ is satisfying_W3' holds
b₁ 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 b₁ being non empty LattStr st b₁ is meet-commutative & b₁ is meet-idempotent & b₁ is join-commutative & b₁ is satisfying_W3 holds
b₁ is join-absorbing by Lemma441;

end;

registration

cluster non empty trivial -> non empty satisfying_W3' for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is trivial holds
b₁ 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 b₁ being non empty LattStr st
( b₁ is satisfying_W3 & b₁ is satisfying_W3' & b₁ is join-idempotent & b₁ is meet-idempotent & b₁ is join-commutative & b₁ 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 b₁ being join-associative meet-absorbing Lattice holds b₁ 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 b₁ being non empty LattStr st b₁ is meet-Absorbing & b₁ is meet-commutative & b₁ is join-commutative holds
b₁ 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 b₁ being WA_Lattice holds b₁ 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 b₁ being WA_Lattice st b₁ is distributive' holds
b₁ 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 b₁ 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₁ = 2 iff b₁ = 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 b₁ 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₁ = 0 iff b₁ = 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 b₁ being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds b₁ . (x,y) = x ex123"\/" y

proof end;

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

proof end;

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

proof end;

end;

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

:: deftheorem EXNDef defines ex123/\ LATWAL_1:def 9 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = ex123/\ iff for x, y being Element of {0,1,2} holds b₁ . (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 b₁ being non empty LattStr st b₁ is trivial holds
( b₁ is meet-idempotent & b₁ is join-commutative & b₁ is meet-Absorbing & b₁ 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 b₁ being non empty join-commutative meet-commutative LattStr st b₁ is meet-absorbing holds
b₁ 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 b₁ being non empty join-commutative meet-commutative LattStr st b₁ is meet-Absorbing holds
b₁ 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 b₁ being non empty LattStr st b₁ is trivial holds
( b₁ is satisfying_WAL31 & b₁ is satisfying_WAL32 & b₁ is satisfying_WAL33 & b₁ is satisfying_WAL34 & b₁ 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 b₁ being non empty LattStr st b₁ is satisfying_WAL31 & b₁ is satisfying_WAL32 & b₁ is satisfying_WAL33 & b₁ is satisfying_WAL34 & b₁ is satisfying_WAL35 holds
( b₁ is join-idempotent & b₁ is meet-idempotent & b₁ is join-commutative & b₁ 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 b₁ being non empty LattStr st b₁ is trivial holds
b₁ 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 b₁ being non empty LattStr st b₁ is satisfying_WAL4 holds
( b₁ is join-idempotent & b₁ is meet-idempotent ) by Lemma2, LemmaW1;

end;