:: Automatization of {T}ernary {B}oolean {A}lgebras
:: by Wojciech Ku\'smierowski and Adam Grabowski
::
:: Received September 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

definition
attr c1 is strict ;
struct TBAStruct -> ComplStr ;
aggr TBAStruct(# carrier, Compl, TernOp #) -> TBAStruct ;
sel TernOp c1 -> TriOp of the carrier of c1;
end;

definition end;

definition
func op3 -> TriOp of means :: LATTBA_1:def 1
it . (0,0,0) = 0 ;
existence
ex b1 being TriOp of st b1 . (0,0,0) = 0
proof end;
uniqueness
for b1, b2 being TriOp of st b1 . (0,0,0) = 0 & b2 . (0,0,0) = 0 holds
b1 = b2
by FUNCT_2:51;
end;

:: deftheorem defines op3 LATTBA_1:def 1 :
for b1 being TriOp of holds
( b1 = op3 iff b1 . (0,0,0) = 0 );

registration
cluster non empty trivial for TBAStruct ;
existence
ex b1 being TBAStruct st
( b1 is trivial & not b1 is empty )
proof end;
end;

definition
let T be non empty TBAStruct ;
let a, b, c be Element of T;
func Tern (a,b,c) -> Element of T equals :: LATTBA_1:def 2
the TernOp of T . (a,b,c);
coherence
the TernOp of T . (a,b,c) is Element of T
;
end;

:: deftheorem defines Tern LATTBA_1:def 2 :
for T being non empty TBAStruct
for a, b, c being Element of T holds Tern (a,b,c) = the TernOp of T . (a,b,c);

definition
let T be non empty TBAStruct ;
attr T is ternary-distributive means :TDis: :: LATTBA_1:def 3
for a, b, c, d, e being Element of T holds Tern ((Tern (a,b,c)),d,(Tern (a,b,e))) = Tern (a,b,(Tern (c,d,e)));
attr T is ternary-left-idempotent means :TLIDef: :: LATTBA_1:def 4
for a, b being Element of T holds Tern (b,b,a) = b;
attr T is ternary-right-idempotent means :TRIDef: :: LATTBA_1:def 5
for a, b being Element of T holds Tern (a,b,b) = b;
attr T is ternary-left-absorbing means :TLADef: :: LATTBA_1:def 6
for a, b being Element of T holds Tern ((b ),b,a) = a;
attr T is ternary-right-absorbing means :TRADef: :: LATTBA_1:def 7
for a, b being Element of T holds Tern (a,b,(b )) = a;
end;

:: deftheorem TDis defines ternary-distributive LATTBA_1:def 3 :
for T being non empty TBAStruct holds
( T is ternary-distributive iff for a, b, c, d, e being Element of T holds Tern ((Tern (a,b,c)),d,(Tern (a,b,e))) = Tern (a,b,(Tern (c,d,e))) );

:: deftheorem TLIDef defines ternary-left-idempotent LATTBA_1:def 4 :
for T being non empty TBAStruct holds
( T is ternary-left-idempotent iff for a, b being Element of T holds Tern (b,b,a) = b );

:: deftheorem TRIDef defines ternary-right-idempotent LATTBA_1:def 5 :
for T being non empty TBAStruct holds
( T is ternary-right-idempotent iff for a, b being Element of T holds Tern (a,b,b) = b );

:: deftheorem TLADef defines ternary-left-absorbing LATTBA_1:def 6 :
for T being non empty TBAStruct holds
( T is ternary-left-absorbing iff for a, b being Element of T holds Tern ((b ),b,a) = a );

:: deftheorem TRADef defines ternary-right-absorbing LATTBA_1:def 7 :
for T being non empty TBAStruct holds
( T is ternary-right-absorbing iff for a, b being Element of T holds Tern (a,b,(b )) = a );

:: It seems that only three are enough
registration
coherence
for b1 being non empty TBAStruct st b1 is trivial holds
( b1 is ternary-distributive & b1 is ternary-left-idempotent & b1 is ternary-right-idempotent & b1 is ternary-left-absorbing & b1 is ternary-right-absorbing )
by STRUCT_0:def 10;
end;

definition end;

:: Section 4 of Grau: Associated Boolean Algebra
definition
let T be Ternary_Boolean_Algebra;
let x be Element of T;
func JoinTBA (T,x) -> BinOp of the carrier of T means :JoinDef: :: LATTBA_1:def 8
for a, b being Element of T holds it . (a,b) = Tern (a,x,b);
existence
ex b1 being BinOp of the carrier of T st
for a, b being Element of T holds b1 . (a,b) = Tern (a,x,b)
proof end;
uniqueness
for b1, b2 being BinOp of the carrier of T st ( for a, b being Element of T holds b1 . (a,b) = Tern (a,x,b) ) & ( for a, b being Element of T holds b2 . (a,b) = Tern (a,x,b) ) holds
b1 = b2
proof end;
func MeetTBA (T,x) -> BinOp of the carrier of T means :MeetDef: :: LATTBA_1:def 9
for a, b being Element of T holds it . (a,b) = Tern (a,(x ),b);
existence
ex b1 being BinOp of the carrier of T st
for a, b being Element of T holds b1 . (a,b) = Tern (a,(x ),b)
proof end;
uniqueness
for b1, b2 being BinOp of the carrier of T st ( for a, b being Element of T holds b1 . (a,b) = Tern (a,(x ),b) ) & ( for a, b being Element of T holds b2 . (a,b) = Tern (a,(x ),b) ) holds
b1 = b2
proof end;
end;

:: deftheorem JoinDef defines JoinTBA LATTBA_1:def 8 :
for T being Ternary_Boolean_Algebra
for x being Element of T
for b3 being BinOp of the carrier of T holds
( b3 = JoinTBA (T,x) iff for a, b being Element of T holds b3 . (a,b) = Tern (a,x,b) );

:: deftheorem MeetDef defines MeetTBA LATTBA_1:def 9 :
for T being Ternary_Boolean_Algebra
for x being Element of T
for b3 being BinOp of the carrier of T holds
( b3 = MeetTBA (T,x) iff for a, b being Element of T holds b3 . (a,b) = Tern (a,(x ),b) );

definition
let T be Ternary_Boolean_Algebra;
let x be Element of T;
func TBA2BA (T,x) -> non empty LattStr equals :: LATTBA_1:def 10
LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #);
correctness
coherence
LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #) is non empty LattStr
;
;
end;

:: deftheorem defines TBA2BA LATTBA_1:def 10 :
for T being Ternary_Boolean_Algebra
for x being Element of T holds TBA2BA (T,x) = LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #);

theorem Th32: :: LATTBA_1:1
for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern (a,b,a) = a
proof end;

theorem Lemma33: :: LATTBA_1:2
for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern ((Tern (a,b,c)),b,a) = Tern (a,b,c)
proof end;

theorem Th33: :: LATTBA_1:3
for T being Ternary_Boolean_Algebra
for a, b, c, d being Element of T holds Tern (a,b,(Tern (c,b,d))) = Tern ((Tern (a,b,c)),b,d)
proof end;

theorem :: LATTBA_1:4
for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern ((b ),b,a) = Tern (a,b,(b ))
proof end;

theorem Lemma34: :: LATTBA_1:5
for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern (a,(b ),b) = a
proof end;

theorem Lemma0: :: LATTBA_1:6
for T being Ternary_Boolean_Algebra
for a being Element of T holds (a )  = a
proof end;

theorem Th35: :: LATTBA_1:7
for T being Ternary_Boolean_Algebra
for a, b being Element of T holds Tern (a,b,(a )) = b
proof end;

theorem Th36a: :: LATTBA_1:8
for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern (a,b,c) = Tern (a,c,b)
proof end;

theorem Th36b: :: LATTBA_1:9
for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern (a,b,c) = Tern (b,c,a)
proof end;

theorem Th36c: :: LATTBA_1:10
for T being Ternary_Boolean_Algebra
for a, b, c being Element of T holds Tern (a,b,c) = Tern (c,b,a)
proof end;

theorem :: LATTBA_1:11
for T being Ternary_Boolean_Algebra
for a, b, c, x being Element of T holds Tern (a,b,c) = Tern ((Tern ((Tern (a,x,b)),(x ),(Tern (b,x,c)))),(x ),(Tern (c,x,a)))
proof end;

definition
let L be B_Lattice;
let a, b, c be Element of L;
func Ros (a,b,c) -> Element of L equals :: LATTBA_1:def 11
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a);
coherence
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) is Element of L
;
end;

:: deftheorem defines Ros LATTBA_1:def 11 :
for L being B_Lattice
for a, b, c being Element of L holds Ros (a,b,c) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a);

definition
let B be B_Lattice;
func RosTrn B -> TriOp of the carrier of B means :RosTrnDef: :: LATTBA_1:def 12
for a, b, c being Element of B holds it . (a,b,c) = Ros (a,b,c);
existence
ex b1 being TriOp of the carrier of B st
for a, b, c being Element of B holds b1 . (a,b,c) = Ros (a,b,c)
proof end;
uniqueness
for b1, b2 being TriOp of the carrier of B st ( for a, b, c being Element of B holds b1 . (a,b,c) = Ros (a,b,c) ) & ( for a, b, c being Element of B holds b2 . (a,b,c) = Ros (a,b,c) ) holds
b1 = b2
proof end;
end;

:: deftheorem RosTrnDef defines RosTrn LATTBA_1:def 12 :
for B being B_Lattice
for b2 being TriOp of the carrier of B holds
( b2 = RosTrn B iff for a, b, c being Element of B holds b2 . (a,b,c) = Ros (a,b,c) );

definition
let B be Boolean Lattice;
func BA2TBA B -> TBAStruct equals :: LATTBA_1:def 13
TBAStruct(# the carrier of B,(comp B),() #);
coherence
TBAStruct(# the carrier of B,(comp B),() #) is TBAStruct
;
end;

:: deftheorem defines BA2TBA LATTBA_1:def 13 :
for B being Boolean Lattice holds BA2TBA B = TBAStruct(# the carrier of B,(comp B),() #);

definition
let B be Boolean Lattice;
func BA2TBAA B -> TBALattStr equals :: LATTBA_1:def 14
TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),() #);
coherence
TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),() #) is TBALattStr
;
end;

:: deftheorem defines BA2TBAA LATTBA_1:def 14 :
for B being Boolean Lattice holds BA2TBAA B = TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),() #);

registration
let B be Boolean Lattice;
cluster BA2TBA B -> non empty ;
coherence
not BA2TBA B is empty
;
end;

registration
let B be Boolean Lattice;
cluster BA2TBAA B -> non empty ;
coherence
not BA2TBAA B is empty
;
end;

ThCom: for T being Ternary_Boolean_Algebra
for x, a, b being Element of T holds (JoinTBA (T,x)) . (a,b) = (JoinTBA (T,x)) . (b,a)

proof end;

registration
let T be Ternary_Boolean_Algebra;
let x be Element of T;
cluster JoinTBA (T,x) -> commutative ;
coherence
JoinTBA (T,x) is commutative
proof end;
end;

ThAssoc: for T being Ternary_Boolean_Algebra
for x, a, b, c being Element of T holds (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c)))

proof end;

registration
let T be Ternary_Boolean_Algebra;
let x be Element of T;
cluster JoinTBA (T,x) -> associative ;
coherence
JoinTBA (T,x) is associative
proof end;
end;

ThCom1: for T being Ternary_Boolean_Algebra
for x, a, b being Element of T holds (MeetTBA (T,x)) . (a,b) = (MeetTBA (T,x)) . (b,a)

proof end;

registration
let T be Ternary_Boolean_Algebra;
let x be Element of T;
cluster MeetTBA (T,x) -> commutative ;
coherence
MeetTBA (T,x) is commutative
proof end;
end;

ThV2: for T being Ternary_Boolean_Algebra
for x, a, b, c being Element of T holds (MeetTBA (T,x)) . (((MeetTBA (T,x)) . (a,b)),c) = (MeetTBA (T,x)) . (a,((MeetTBA (T,x)) . (b,c)))

proof end;

registration
let T be Ternary_Boolean_Algebra;
let x be Element of T;
cluster MeetTBA (T,x) -> associative ;
coherence
MeetTBA (T,x) is associative
proof end;
end;

V4: for T being Ternary_Boolean_Algebra
for x being Element of T holds MeetTBA (T,x) absorbs JoinTBA (T,x)

proof end;

V3: for T being Ternary_Boolean_Algebra
for x being Element of T holds JoinTBA (T,x) absorbs MeetTBA (T,x)

proof end;

registration
let T be Ternary_Boolean_Algebra;
let p be Element of T;
cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> Lattice-like ;
coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is Lattice-like
proof end;
end;

registration
let B be Boolean Lattice;
coherence
proof end;
end;

theorem TBACompl: :: LATTBA_1:12
for B being Boolean Lattice
for x being Element of B
for xx being Element of () st xx = x holds
x  = xx 
proof end;

theorem TBAComplA: :: LATTBA_1:13
for B being Boolean Lattice
for x being Element of B
for xx being Element of () st xx = x holds
x  = xx 
proof end;

registration
let B be Boolean Lattice;
coherence
proof end;
end;

registration
let B be Boolean Lattice;
coherence
proof end;
end;

theorem TBA1: :: LATTBA_1:14
for B being Boolean Lattice st ( for v1, v0 being Element of () holds Tern (v0,v0,v1) = v0 ) & ( for v2, v1, v0 being Element of () holds Tern (v0,v1,v2) = Tern (v2,v0,v1) ) & ( for v2, v1, v0 being Element of () holds Tern (v0,v1,v2) = Tern (v0,v2,v1) ) & ( for v3, v2, v1, v0 being Element of () holds Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3))) ) holds
for v1, v2, v3, v4, v5 being Element of () holds Tern ((Tern (v1,v2,v3)),v4,(Tern (v1,v2,v5))) = Tern (v1,v2,(Tern (v3,v4,v5)))
proof end;

theorem TBA2: :: LATTBA_1:15
for B being Boolean Lattice st ( for v2, v1, v0 being Element of () holds Tern (v0,v1,v2) = ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of () holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of () holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) & ( for v2, v1, v0 being Element of () holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v2, v1, v0 being Element of () holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) holds
for v1, v2, v3, v4 being Element of () holds Tern ((Tern (v1,v2,v3)),v2,v4) = Tern (v1,v2,(Tern (v3,v2,v4)))
proof end;

LemacikA: for B being Boolean Lattice
for v2, v1, v0 being Element of () holds Tern (v0,v1,v2) = Tern (v2,v0,v1)

proof end;

LemacikB: for B being Boolean Lattice
for v2, v1, v0 being Element of () holds Tern (v0,v1,v2) = Tern (v0,v2,v1)

proof end;

theorem :: LATTBA_1:16
for B being Boolean Lattice
for v0, v1 being Element of ()
for a, b being Element of B st a = v0 & b = v1 holds
v0 "\/" v1 = a "\/" b ;

LemacikD: for B being Boolean Lattice
for v0, v2, v1 being Element of () holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)

proof end;

LemacikE: for B being Boolean Lattice
for v0, v2, v1 being Element of () holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2)

proof end;

LemacikC: for B being Boolean Lattice
for v3, v2, v1, v0 being Element of () holds Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3)))

proof end;

registration
let B be Boolean Lattice;
coherence
proof end;
end;

registration
let T be Ternary_Boolean_Algebra;
let p be Element of T;
cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> distributive ;
coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is distributive
proof end;
end;

registration
let T be Ternary_Boolean_Algebra;
let p be Element of T;
cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> bounded ;
coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is bounded
proof end;
end;

theorem TopTBA: :: LATTBA_1:17
for T being Ternary_Boolean_Algebra
for p being Element of T holds Top LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p
proof end;

theorem BotTBA: :: LATTBA_1:18
for T being Ternary_Boolean_Algebra
for p being Element of T holds Bottom LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p
proof end;

registration
let T be Ternary_Boolean_Algebra;
let p be Element of T;
cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> complemented ;
coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is complemented
proof end;
end;

registration
let T be Ternary_Boolean_Algebra;
let p be Element of T;
cluster LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) -> Boolean ;
coherence
LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is Boolean
;
end;

definition
let T be non empty TBAStruct ;
attr T is satisfying_TBA1 means :: LATTBA_1:def 15
for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x ),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) ),(Tern (u,(Tern (v6,w,v)),z))) = y;
end;

:: deftheorem defines satisfying_TBA1 LATTBA_1:def 15 :
for T being non empty TBAStruct holds
( T is satisfying_TBA1 iff for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x ),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) ),(Tern (u,(Tern (v6,w,v)),z))) = y );

theorem TBALemma: :: LATTBA_1:19
for T being non empty TBAStruct st ( for v4, v3, v2, v1, v0 being Element of T holds Tern ((Tern (v0,v1,v2)),v3,(Tern (v0,v1,v4))) = Tern (v0,v1,(Tern (v2,v3,v4))) ) & ( for v1, v0 being Element of T holds Tern (v0,v1,v1) = v1 ) & ( for v1, v0 being Element of T holds Tern (v0,v1,(v1 )) = v0 ) & ( for v1, v0 being Element of T holds Tern (v0,v0,v1) = v0 ) holds
for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x ),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y
proof end;

definition
let T be non empty TBAStruct ;
end;

:: deftheorem defines TBA-like LATTBA_1:def 16 :
for T being non empty TBAStruct holds
( T is TBA-like iff ( T is ternary-distributive & T is ternary-left-idempotent & T is ternary-right-idempotent & T is ternary-left-absorbing & T is ternary-right-absorbing ) );

registration
coherence
for b1 being non empty TBAStruct st b1 is ternary-distributive & b1 is ternary-left-idempotent & b1 is ternary-right-idempotent & b1 is ternary-left-absorbing & b1 is ternary-right-absorbing holds
b1 is TBA-like
;
coherence
for b1 being non empty TBAStruct st b1 is TBA-like holds
( b1 is ternary-distributive & b1 is ternary-left-idempotent & b1 is ternary-right-idempotent & b1 is ternary-left-absorbing & b1 is ternary-right-absorbing )
;
end;

registration
coherence
for b1 being non empty TBAStruct st b1 is TBA-like holds
b1 is satisfying_TBA1
proof end;
end;