:: 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
attr c1 is strict ;
struct TBALattStr -> TBAStruct , LattStr ;
aggr TBALattStr(# carrier, L_join, L_meet, Compl, TernOp #) -> TBALattStr ;
end;

definition
func op3 -> TriOp of {0} means :: LATTBA_1:def 1
it . (0,0,0) = 0 ;
existence
ex b1 being TriOp of {0} st b1 . (0,0,0) = 0
proof end;
uniqueness
for b1, b2 being TriOp of {0} 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 {0} 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
cluster non empty trivial -> non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing for TBAStruct ;
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
mode Ternary_Boolean_Algebra is non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing TBAStruct ;
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),(RosTrn B) #);
coherence
TBAStruct(# the carrier of B,(comp B),(RosTrn 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),(RosTrn 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),(RosTrn B) #);
coherence
TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn 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),(RosTrn 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;
cluster BA2TBAA B -> Lattice-like ;
coherence
BA2TBAA B is Lattice-like
proof end;
end;

theorem TBACompl: :: LATTBA_1:12
for B being Boolean Lattice
for x being Element of B
for xx being Element of (BA2TBA B) 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 (BA2TBAA B) st xx = x holds
x ` = xx `
proof end;

registration
let B be Boolean Lattice;
cluster BA2TBA B -> ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing ;
coherence
( BA2TBA B is ternary-left-idempotent & BA2TBA B is ternary-right-idempotent & BA2TBA B is ternary-left-absorbing & BA2TBA B is ternary-right-absorbing )
proof end;
end;

registration
let B be Boolean Lattice;
cluster BA2TBAA B -> ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing ;
coherence
( BA2TBAA B is ternary-left-idempotent & BA2TBAA B is ternary-right-idempotent & BA2TBAA B is ternary-left-absorbing & BA2TBAA B is ternary-right-absorbing )
proof end;
end;

theorem TBA1: :: LATTBA_1:14
for B being Boolean Lattice st ( for v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v0,v1) = v0 ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v2,v0,v1) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v0,v2,v1) ) & ( for v3, v2, v1, v0 being Element of (BA2TBAA B) 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 (BA2TBAA B) 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 (BA2TBAA B) holds Tern (v0,v1,v2) = ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) holds
for v1, v2, v3, v4 being Element of (BA2TBAA B) 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 (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v2,v0,v1)
proof end;

LemacikB: for B being Boolean Lattice
for v2, v1, v0 being Element of (BA2TBAA B) 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 (BA2TBAA B)
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 (BA2TBAA B) holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)
proof end;

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

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

registration
let B be Boolean Lattice;
cluster BA2TBAA B -> ternary-distributive ;
coherence
BA2TBAA B is ternary-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)) #) -> 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 ;
attr T is TBA-like means :: LATTBA_1:def 16
( T is ternary-distributive & T is ternary-left-idempotent & T is ternary-right-idempotent & T is ternary-left-absorbing & T is ternary-right-absorbing );
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
cluster non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing -> non empty TBA-like for TBAStruct ;
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 ;
cluster non empty TBA-like -> non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing for TBAStruct ;
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
cluster non empty TBA-like -> non empty satisfying_TBA1 for TBAStruct ;
coherence
for b1 being non empty TBAStruct st b1 is TBA-like holds
b1 is satisfying_TBA1
proof end;
end;