:: Formalization of Trellises and Tolerance Relations
:: by Adam Grabowski and Franciszek Turowski
::
:: Received December 27, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

:: reflexive antisymmetric = pseudo-order

registration

cluster non empty reflexive antisymmetric with_suprema with_infima for RelStr ;

existence
ex b₁ being non empty RelStr st
( b₁ is reflexive & b₁ is antisymmetric & b₁ is with_suprema & b₁ is with_infima )

proof end;

end;

definition

mode RT-Lattice is non empty antisymmetric with_suprema with_infima RelStr ;

end;

definition

mode WA-Lattice is non empty reflexive antisymmetric with_suprema with_infima RelStr ;

end;

theorem Lemat0: :: LATWAL_2:1

for W being WA-Lattice
for a, b being Element of W holds
( a <= b iff a "\/" b = b ) by YELLOW_0:24;

theorem Lemat01: :: LATWAL_2:2

for W being WA-Lattice
for a, b being Element of W holds
( a <= b iff a "/\" b = a ) by YELLOW_0:25;

theorem LemmaId: :: LATWAL_2:3

for W being WA-Lattice
for a being Element of W holds a "/\" a = a by YELLOW_0:25;

theorem LemmaId2: :: LATWAL_2:4

for W being WA-Lattice
for a being Element of W holds a "\/" a = a

proof end;

theorem :: LATWAL_2:5

for W being WA-Lattice
for a, b being Element of W holds a "/\" b = b "/\" a ;

theorem :: LATWAL_2:6

for W being WA-Lattice
for a, b being Element of W holds a "\/" b = b "\/" a ;

theorem LemmaX1: :: LATWAL_2:7

for W being WA-Lattice
for a, b being Element of W holds (a "/\" b) "\/" a = a by LATTICE3:17;

theorem LemmaX2: :: LATWAL_2:8

for W being WA-Lattice
for a, b being Element of W holds (a "\/" b) "/\" a = a by LATTICE3:18;

theorem :: LATWAL_2:9

for W being WA-Lattice
for a, b, c being Element of W st W is transitive holds
(a "\/" b) "\/" c = a "\/" (b "\/" c) by LATTICE3:14;

theorem :: LATWAL_2:10

for W being WA-Lattice
for a, b, c being Element of W st W is transitive holds
(a "/\" b) "/\" c = a "/\" (b "/\" c) by LATTICE3:16;

theorem LatWal1: :: LATWAL_2:11

for W being WA-Lattice
for a, b, c being Element of W st a <= c & b <= c holds
a "\/" b <= c by YELLOW_0:22;

theorem LatWal2: :: LATWAL_2:12

for W being WA-Lattice
for a, b being Element of W holds a <= a "\/" b by YELLOW_0:22;

theorem LatWal3: :: LATWAL_2:13

for W being WA-Lattice
for a, b, c being Element of W st c <= a & c <= b holds
c <= a "/\" b by YELLOW_0:23;

theorem :: LATWAL_2:14

for W being WA-Lattice
for a, b, c being Element of W holds ((a "/\" c) "\/" (b "/\" c)) "\/" c = c

proof end;

theorem :: LATWAL_2:15

for W being WA-Lattice
for a, b, c being Element of W holds ((a "\/" c) "/\" (b "\/" c)) "/\" c = c

proof end;

:: Definition 3

registration

let D be non empty trivial set ;

cluster pcs-total D -> antisymmetric ;

coherence
pcs-total D is antisymmetric

proof end;

end;

registration

cluster non empty reflexive antisymmetric with_suprema with_infima for pcs-Str ;

existence
ex b₁ being pcs-Str st
( b₁ is reflexive & b₁ is antisymmetric & b₁ is with_suprema & b₁ is with_infima & not b₁ is empty )

proof end;

end;

definition

mode WAP-Lattice is non empty reflexive antisymmetric with_suprema with_infima pcs-Str ;

end;

:: Compatibility in Tolerance Structures

definition

let P be pcs-Str ;

:: a (--) b means that a tolerates b
:: T is compatible with P

attr P is pcs-Compatible means :CompDef: :: LATWAL_2:def 1
for a1, a2, b1, b2 being Element of P st a1 (--) b1 & a2 (--) b2 holds
( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 );

end;

:: deftheorem CompDef defines pcs-Compatible LATWAL_2:def 1 :
for P being pcs-Str holds
( P is pcs-Compatible iff for a1, a2, b1, b2 being Element of P st a1 (--) b1 & a2 (--) b2 holds
( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 ) );

:: Theorem 1

registration

cluster non empty trivial total reflexive antisymmetric with_suprema with_infima pcs-Compatible for pcs-Str ;

existence
ex b₁ being WAP-Lattice st
( b₁ is trivial & b₁ is total & b₁ is pcs-Compatible )

proof end;

end;

:: Definition 4: Segment

definition

let W be WA-Lattice;
let a, b be Element of W;

func Segment (a,b) -> Subset of W equals :: LATWAL_2:def 2
{ x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } ;

coherence
{ x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } is Subset of W

proof end;

end;

:: deftheorem defines Segment LATWAL_2:def 2 :
for W being WA-Lattice
for a, b being Element of W holds Segment (a,b) = { x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } ;

:: Section 2, before Proposition 1
:: The definition of a symmetric hull

definition

let W be non empty RelStr ;

:: Section 2, before Proposition 1
:: The definition of a symmetric hull

func SymmetricHull W -> Relation of the carrier of W means :SymHull: :: LATWAL_2:def 3
for x, y being Element of W holds
( [x,y] in it iff ( x <= y or y <= x ) );

existence
ex b₁ being Relation of the carrier of W st
for x, y being Element of W holds
( [x,y] in b₁ iff ( x <= y or y <= x ) )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier of W st ( for x, y being Element of W holds
( [x,y] in b₁ iff ( x <= y or y <= x ) ) ) & ( for x, y being Element of W holds
( [x,y] in b₂ iff ( x <= y or y <= x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem SymHull defines SymmetricHull LATWAL_2:def 3 :
for W being non empty RelStr
for b₂ being Relation of the carrier of W holds
( b₂ = SymmetricHull W iff for x, y being Element of W holds
( [x,y] in b₂ iff ( x <= y or y <= x ) ) );

registration

let W be WA-Lattice;

cluster SymmetricHull W -> total ;

coherence
SymmetricHull W is total

proof end;

end;

registration

let W be WA-Lattice;

cluster SymmetricHull W -> reflexive symmetric ;

coherence
( SymmetricHull W is reflexive & SymmetricHull W is symmetric )

proof end;

end;

registration

let L be WA-Lattice;

cluster Relation-like the carrier of L -defined the carrier of L -valued total reflexive symmetric for Element of bool [: the carrier of L, the carrier of L:];

existence
ex b₁ being Relation of the carrier of L st
( b₁ is total & b₁ is reflexive & b₁ is symmetric )

proof end;

end;

theorem :: LATWAL_2:16

for W being WA-Lattice holds SymmetricHull W is Tolerance of the carrier of W ;

definition

let S be non empty RelStr ;

attr S is tournament means :: LATWAL_2:def 4
for x, y being Element of S holds
( x <= y or y <= x );

end;

:: deftheorem defines tournament LATWAL_2:def 4 :
for S being non empty RelStr holds
( S is tournament iff for x, y being Element of S holds
( x <= y or y <= x ) );

theorem :: LATWAL_2:17

for S being non empty RelStr holds
( S is tournament iff SymmetricHull S = nabla the carrier of S )

proof end;

theorem NablaCompat: :: LATWAL_2:18

for P being non empty pcs-Str st the ToleranceRel of P = nabla the carrier of P holds
P is pcs-Compatible

proof end;

theorem :: LATWAL_2:19

for P being non empty pcs-Str st the ToleranceRel of P = id the carrier of P holds
P is pcs-Compatible

proof end;

registration

cluster non empty total reflexive antisymmetric with_suprema with_infima pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible for pcs-Str ;

existence
ex b₁ being WAP-Lattice st
( b₁ is pcs-Compatible & b₁ is pcs-tol-reflexive & b₁ is pcs-tol-symmetric )

proof end;

end;

theorem LemmaRefl: :: LATWAL_2:20

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for x being Element of W holds x (--) x

proof end;

theorem :: LATWAL_2:21

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for x, y being Element of W st x (--) y holds
y (--) x ;

theorem :: LATWAL_2:22

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for a, b being Element of W st a (--) b & b (--) b holds
a "/\" b (--) b "/\" b by CompDef;

theorem :: LATWAL_2:23

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for a, b being Element of W st a (--) b & b (--) b holds
a "/\" b (--) b

proof end;

theorem :: LATWAL_2:24

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for a, b being Element of W st a (--) b & a (--) a holds
a "/\" b (--) a

proof end;

theorem :: LATWAL_2:25

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for a, b being Element of W st a (--) b & a (--) a holds
a "\/" b (--) a

proof end;

theorem :: LATWAL_2:26

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for a, b being Element of W st a (--) b holds
for x, y being Element of W st x in Segment ((a "/\" b),(a "\/" b)) & y in Segment ((a "/\" b),(a "\/" b)) holds
x (--) y

proof end;

theorem Idem2: :: LATWAL_2:27

for L being WA_Lattice
for x, y being Element of L holds
( [x,y] in LatOrder L iff x [= y )

proof end;

theorem Th32: :: LATWAL_2:28

for L being WA_Lattice holds
( dom (LatOrder L) = the carrier of L & rng (LatOrder L) = the carrier of L & field (LatOrder L) = the carrier of L )

proof end;

definition

let L be WA_Lattice;
:: original: LatOrder
redefine func LatOrder L -> Relation of the carrier of L;
correctness
coherence
LatOrder L is Relation of the carrier of L;

proof end;

end;

registration

let W be WA_Lattice;

cluster LatOrder W -> the carrier of W -defined ;

coherence
LatOrder W is the carrier of W -defined ;

cluster LatOrder W -> the carrier of W -valued ;

coherence
LatOrder W is the carrier of W -valued ;

end;

registration

let L be WA_Lattice;

cluster LatOrder L -> total for Relation of the carrier of L;

correctness
coherence
for b₁ being Relation of the carrier of L st b₁ = LatOrder L holds
b₁ is total ;

proof end;

end;

registration

let W be WA_Lattice;

cluster LatOrder W -> reflexive ;

coherence
LatOrder W is reflexive

proof end;

end;

registration

let W be WA_Lattice;

cluster LatOrder W -> antisymmetric ;

coherence
LatOrder W is antisymmetric

proof end;

end;

PomocU21: for a, b being Element of ExNearLattice st a = 2 & b = 1 holds
a "\/" b = 2

proof end;

PomocU12: for a, b being Element of ExNearLattice st a = 1 & b = 2 holds
a "\/" b = 2

proof end;

PomocU01: for a, b being Element of ExNearLattice st a = 0 & b = 1 holds
a "\/" b = 1

proof end;

PomocU20: for a, b being Element of ExNearLattice st a = 2 & b = 0 holds
a "\/" b = 0

proof end;

PomocU10: for a, b being Element of ExNearLattice st a = 1 & b = 0 holds
a "\/" b = 1

proof end;

PomocU02: for a, b being Element of ExNearLattice st a = 0 & b = 2 holds
a "\/" b = 0

proof end;

PomocL21: for a, b being Element of ExNearLattice st a = 2 & b = 1 holds
a "/\" b = 1

proof end;

PomocL01: for a, b being Element of ExNearLattice st a = 0 & b = 1 holds
a "/\" b = 0

proof end;

PomocL20: for a, b being Element of ExNearLattice st a = 2 & b = 0 holds
a "/\" b = 2

proof end;

PomocL02: for a, b being Element of ExNearLattice st a = 0 & b = 2 holds
a "/\" b = 2
by PomocL20;

PomocL12: for a, b being Element of ExNearLattice st a = 1 & b = 2 holds
a "/\" b = 1

proof end;

PomocL10: for a, b being Element of ExNearLattice st a = 1 & b = 0 holds
a "/\" b = 0

proof end;

ExW31: ExNearLattice is satisfying_W3

proof end;

ExW32: ExNearLattice is satisfying_W3'

proof end;

registration

cluster ExNearLattice -> satisfying_W3 satisfying_W3' ;

coherence
( ExNearLattice is satisfying_W3 & ExNearLattice is satisfying_W3' ) by ExW31, ExW32;

end;

definition

let L be WA_Lattice;

:: LATTAD_1:def 12 is the version for generalized almost distributive

func LatRelStr L -> strict RelStr equals :: LATWAL_2:def 5
RelStr(# the carrier of L,(LatOrder L) #);

coherence
RelStr(# the carrier of L,(LatOrder L) #) is strict RelStr ;

end;

:: deftheorem defines LatRelStr LATWAL_2:def 5 :
for L being WA_Lattice holds LatRelStr L = RelStr(# the carrier of L,(LatOrder L) #);

theorem LemmaEqual0: :: LATWAL_2:29

for L being WA_Lattice
for x, y being Element of L
for xx, yy being Element of (LatRelStr L) st x = xx & y = yy holds
( x [= y iff xx <= yy )

proof end;

definition

let L be WA_Lattice;
let p be Element of L;

func p % -> Element of (LatRelStr L) equals :: LATWAL_2:def 6
p;

coherence
p is Element of (LatRelStr L) ;

end;

:: deftheorem defines % LATWAL_2:def 6 :
for L being WA_Lattice
for p being Element of L holds p % = p;

definition

let L be WA_Lattice;
let p be Element of (LatRelStr L);

func % p -> Element of L equals :: LATWAL_2:def 7
p;

coherence
p is Element of L ;

end;

:: deftheorem defines % LATWAL_2:def 7 :
for L being WA_Lattice
for p being Element of (LatRelStr L) holds % p = p;

registration

let L be WA_Lattice;

cluster LatRelStr L -> strict reflexive antisymmetric ;

coherence
( LatRelStr L is reflexive & LatRelStr L is antisymmetric ) ;

end;

registration

let L be WA_Lattice;

cluster LatRelStr L -> strict with_suprema with_infima ;

coherence
( LatRelStr L is with_suprema & LatRelStr L is with_infima )

proof end;

end;

registration

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

existence
ex b₁ being WA_Lattice st b₁ is strict by LATWAL_1:def 10;

end;

deffunc H₁( LattStr ) -> set = the carrier of $1;

deffunc H₂( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;

deffunc H₃( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;

theorem Th6: :: LATWAL_2:30

for L1, L2 being WA_Lattice st LatRelStr L1 = LatRelStr L2 holds
LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #)

proof end;

Lm1: now :: thesis: for A being non empty antisymmetric with_suprema RelStr
for a, b, c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) )

let A be non empty antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) )
let a, b be Element of A; :: thesis: for c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) )
thus for c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) ) by YELLOW_0:22; :: thesis: verum

end;

theorem Th19: :: LATWAL_2:31

for A being WA-Lattice ex L being strict WA_Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr L

proof end;

theorem :: LATWAL_2:32

LatRelStr ExNearLattice is WA-Lattice ;

definition

let A be RelStr ;
assume A1: ( A is with_suprema & A is with_infima & A is reflexive & A is antisymmetric ) ;

func wlatt A -> strict WA_Lattice means :WLatDef: :: LATWAL_2:def 8
RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr it;

existence
ex b₁ being strict WA_Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr b₁ by A1, Th19;
uniqueness
for b₁, b₂ being strict WA_Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr b₁ & RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr b₂ holds
b₁ = b₂ by Th6;

end;

:: deftheorem WLatDef defines wlatt LATWAL_2:def 8 :
for A being RelStr st A is with_suprema & A is with_infima & A is reflexive & A is antisymmetric holds
for b₂ being strict WA_Lattice holds
( b₂ = wlatt A iff RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr b₂ );

theorem :: LATWAL_2:33

wlatt (LatRelStr ExNearLattice) is WA_Lattice ;

registration

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

coherence
for b₁ being meet-associative join-absorbing Lattice holds b₁ is satisfying_W3

proof end;

end;

registration

cluster non empty Lattice-like -> join-idempotent meet-idempotent for LattStr ;

coherence
for b₁ being Lattice holds
( b₁ is join-idempotent & b₁ is meet-idempotent )

proof end;

end;

theorem Eq0: :: LATWAL_2:34

for L being Lattice holds LattRel L = LatOrder L

proof end;

theorem Eq1: :: LATWAL_2:35

for L being with_suprema with_infima Poset
for a, b being Element of L
for aa, bb being Element of (latt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )

proof end;

theorem Eq2: :: LATWAL_2:36

for L being WA-Lattice
for a, b being Element of L
for aa, bb being Element of (wlatt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )

proof end;

theorem :: LATWAL_2:37

for L being WA-Lattice st the InternalRel of L is transitive holds
wlatt L is Lattice

proof end;

definition

let L be WA-Lattice;
let A be set ;

pred A is_cycle_of L means :: LATWAL_2:def 9
for a, b being Element of L st a <> b & a in A & b in A holds
A = Segment (a,b);

end;

:: deftheorem defines is_cycle_of LATWAL_2:def 9 :
for L being WA-Lattice
for A being set holds
( A is_cycle_of L iff for a, b being Element of L st a <> b & a in A & b in A holds
A = Segment (a,b) );

theorem SingleCycle: :: LATWAL_2:38

for L being WA-Lattice
for a being Element of L holds {a} is_cycle_of L

proof end;

definition

let L be WA-Lattice;
let A be Subset of L;

attr A is cyclic means :: LATWAL_2:def 10
A is_cycle_of L;

end;

:: deftheorem defines cyclic LATWAL_2:def 10 :
for L being WA-Lattice
for A being Subset of L holds
( A is cyclic iff A is_cycle_of L );

registration

let L be WA-Lattice;

cluster cyclic for Element of bool the carrier of L;

existence
ex b₁ being Subset of L st b₁ is cyclic

proof end;

end;

definition

let L be WA-Lattice;
mode Cycle of L is cyclic Subset of L;

end;

theorem :: LATWAL_2:39

for L being WA-Lattice
for a, b, x being Element of L holds
( not x in Segment (a,b) or ( a <= x & x <= b ) or ( b <= x & x <= a ) )

proof end;

definition

let L be WA-Lattice;
let A be Subset of L;

attr A is tournament means :: LATWAL_2:def 11
for a, b being Element of L st a in A & b in A & not a <= b holds
b <= a;

end;

:: deftheorem defines tournament LATWAL_2:def 11 :
for L being WA-Lattice
for A being Subset of L holds
( A is tournament iff for a, b being Element of L st a in A & b in A & not a <= b holds
b <= a );

notation

let L be WA-Lattice;
let A be Subset of L;
antonym acyclic A for cyclic ;

end;

:: function(^(_,_), [
:: 0,0,0,0,0,
:: 0,1,1,3,1,
:: 0,1,2,2,2,
:: 0,3,2,3,3,
:: 0,1,2,3,4]),
:: function(v(_,_), [
:: 0,1,2,3,4,
:: 1,1,2,1,4,
:: 2,2,2,3,4,
:: 3,1,3,3,4,
:: 4,4,4,4,4]),

registration

cluster {0,1,2,3,4} -> non empty ;

coherence
not {0,1,2,3,4} is empty by ENUMSET1:def 3;

end;

registration

cluster -> natural for Element of {0,1,2,3,4};

coherence
for b₁ being Element of {0,1,2,3,4} holds b₁ is natural by ENUMSET1:def 3;

end;

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

proof end;

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

proof end;

definition

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

func x ex1234"\/" y -> Element of {0,1,2,3,4} equals :UPDef: :: LATWAL_2:def 12
1 if ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) )
max (x,y) if ( not ( x = 1 & y = 3 ) & not ( x = 3 & y = 1 ) )
;

coherence
( ( ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) ) implies 1 is Element of {0,1,2,3,4} ) & ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or max (x,y) is Element of {0,1,2,3,4} ) ) by LmB;
consistency
for b₁ being Element of {0,1,2,3,4} holds
( ( not ( x = 1 & y = 3 ) & not ( x = 3 & y = 1 ) ) or ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or ( b₁ = 1 iff b₁ = max (x,y) ) ) ;

func x ex1234"/\" y -> Element of {0,1,2,3,4} equals :ExMeetDef: :: LATWAL_2:def 13
3 if ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) )
min (x,y) if ( not ( x = 1 & y = 3 ) & not ( x = 3 & y = 1 ) )
;

correctness
coherence
( ( ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) ) implies 3 is Element of {0,1,2,3,4} ) & ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or min (x,y) is Element of {0,1,2,3,4} ) );
consistency
for b₁ being Element of {0,1,2,3,4} holds
( ( not ( x = 1 & y = 3 ) & not ( x = 3 & y = 1 ) ) or ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or ( b₁ = 3 iff b₁ = min (x,y) ) );
by LmA;

end;

:: deftheorem UPDef defines ex1234"\/" LATWAL_2:def 12 :
for x, y being Element of {0,1,2,3,4} holds
( ( ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) ) implies x ex1234"\/" y = 1 ) & ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or x ex1234"\/" y = max (x,y) ) );

:: deftheorem ExMeetDef defines ex1234"/\" LATWAL_2:def 13 :
for x, y being Element of {0,1,2,3,4} holds
( ( ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) ) implies x ex1234"/\" y = 3 ) & ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or x ex1234"/\" y = min (x,y) ) );

definition

func ex1234\/ -> BinOp of {0,1,2,3,4} means :EXUDef: :: LATWAL_2:def 14
for x, y being Element of {0,1,2,3,4} holds it . (x,y) = x ex1234"\/" y;

existence
ex b₁ being BinOp of {0,1,2,3,4} st
for x, y being Element of {0,1,2,3,4} holds b₁ . (x,y) = x ex1234"\/" y

proof end;

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

proof end;

func ex1234/\ -> BinOp of {0,1,2,3,4} means :EXNDef: :: LATWAL_2:def 15
for x, y being Element of {0,1,2,3,4} holds it . (x,y) = x ex1234"/\" y;

existence
ex b₁ being BinOp of {0,1,2,3,4} st
for x, y being Element of {0,1,2,3,4} holds b₁ . (x,y) = x ex1234"/\" y

proof end;

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

proof end;

end;

:: deftheorem EXUDef defines ex1234\/ LATWAL_2:def 14 :
for b₁ being BinOp of {0,1,2,3,4} holds
( b₁ = ex1234\/ iff for x, y being Element of {0,1,2,3,4} holds b₁ . (x,y) = x ex1234"\/" y );

:: deftheorem EXNDef defines ex1234/\ LATWAL_2:def 15 :
for b₁ being BinOp of {0,1,2,3,4} holds
( b₁ = ex1234/\ iff for x, y being Element of {0,1,2,3,4} holds b₁ . (x,y) = x ex1234"/\" y );

definition

func ExWALattice -> non empty LattStr equals :: LATWAL_2:def 16
LattStr(# {0,1,2,3,4},ex1234\/,ex1234/\ #);

coherence
LattStr(# {0,1,2,3,4},ex1234\/,ex1234/\ #) is non empty LattStr ;

end;

:: deftheorem defines ExWALattice LATWAL_2:def 16 :
ExWALattice = LattStr(# {0,1,2,3,4},ex1234\/,ex1234/\ #);

ExJoinAbs: ExWALattice is join-absorbing

proof end;

ExMeetAbs: ExWALattice is meet-absorbing

proof end;

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

proof end;

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

proof end;

Cosik1: not ExWALattice is join-associative

proof end;

Cosik2: not ExWALattice is meet-associative

proof end;

registration

cluster ExWALattice -> non empty non join-associative non meet-associative ;

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

end;

ExJoinComm: ExWALattice is join-commutative

proof end;

ExMeetComm: ExWALattice is meet-commutative

proof end;

registration

cluster ExWALattice -> non empty join-commutative meet-commutative meet-absorbing join-absorbing ;

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

end;

HelpL0: for a, b being Element of ExWALattice st b = 0 holds
a "/\" b = 0

proof end;

HelpU0: for a, b being Element of ExWALattice st b = 0 holds
a "\/" b = a

proof end;

HelpU12: for a, b being Element of ExWALattice st a = 1 & b = 2 holds
a "\/" b = 2

proof end;

HelpU13: for a, b being Element of ExWALattice st a = 1 & b = 3 holds
a "\/" b = 1

proof end;

HelpU23: for a, b being Element of ExWALattice st a = 2 & b = 3 holds
a "\/" b = 3

proof end;

HelpU4: for a, b being Element of ExWALattice st b = 4 holds
a "\/" b = 4

proof end;

HelpL12: for a, b being Element of ExWALattice st a = 1 & b = 2 holds
a "/\" b = 1

proof end;

HelpL13: for a, b being Element of ExWALattice st a = 1 & b = 3 holds
a "/\" b = 3

proof end;

HelpL23: for a, b being Element of ExWALattice st a = 2 & b = 3 holds
a "/\" b = 2

proof end;

HelpL4: for a, b being Element of ExWALattice st b = 4 holds
a "/\" b = a

proof end;

ExW31: ExWALattice is satisfying_W3

proof end;

ExW32: ExWALattice is satisfying_W3'

proof end;

registration

cluster ExWALattice -> non empty satisfying_W3 satisfying_W3' ;

coherence
( ExWALattice is satisfying_W3 & ExWALattice is satisfying_W3' ) by ExW31, ExW32;

end;