:: by Wojciech Ku\'smierowski and Adam Grabowski

::

:: Received September 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

definition

attr c_{1} is strict ;

struct TBAStruct -> ComplStr ;

aggr TBAStruct(# carrier, Compl, TernOp #) -> TBAStruct ;

sel TernOp c_{1} -> TriOp of the carrier of c_{1};

end;
struct TBAStruct -> ComplStr ;

aggr TBAStruct(# carrier, Compl, TernOp #) -> TBAStruct ;

sel TernOp c

definition

attr c_{1} is strict ;

struct TBALattStr -> TBAStruct , LattStr ;

aggr TBALattStr(# carrier, L_join, L_meet, Compl, TernOp #) -> TBALattStr ;

end;
struct TBALattStr -> TBAStruct , LattStr ;

aggr TBALattStr(# carrier, L_join, L_meet, Compl, TernOp #) -> TBALattStr ;

definition

existence

ex b_{1} being TriOp of {0} st b_{1} . (0,0,0) = 0

for b_{1}, b_{2} being TriOp of {0} st b_{1} . (0,0,0) = 0 & b_{2} . (0,0,0) = 0 holds

b_{1} = b_{2}
by FUNCT_2:51;

end;
ex b

proof end;

uniqueness for b

b

:: deftheorem defines op3 LATTBA_1:def 1 :

for b_{1} being TriOp of {0} holds

( b_{1} = op3 iff b_{1} . (0,0,0) = 0 );

for b

( b

registration
end;

definition

let T be non empty TBAStruct ;

let a, b, c be Element of T;

coherence

the TernOp of T . (a,b,c) is Element of T ;

end;
let a, b, c be Element of T;

coherence

the TernOp of T . (a,b,c) is Element of T ;

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

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 ;

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

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;

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;

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;

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;

for a, b being Element of T holds Tern (a,b,(b `)) = a;

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

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

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

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

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

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

for b_{1} being non empty TBAStruct st b_{1} is trivial holds

( b_{1} is ternary-distributive & b_{1} is ternary-left-idempotent & b_{1} is ternary-right-idempotent & b_{1} is ternary-left-absorbing & b_{1} is ternary-right-absorbing )
by STRUCT_0:def 10;

end;

cluster non empty trivial -> non empty ternary-distributive ternary-left-idempotent ternary-right-idempotent ternary-left-absorbing ternary-right-absorbing for TBAStruct ;

coherence for b

( b

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;

ex b_{1} being BinOp of the carrier of T st

for a, b being Element of T holds b_{1} . (a,b) = Tern (a,x,b)

for b_{1}, b_{2} being BinOp of the carrier of T st ( for a, b being Element of T holds b_{1} . (a,b) = Tern (a,x,b) ) & ( for a, b being Element of T holds b_{2} . (a,b) = Tern (a,x,b) ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of the carrier of T st

for a, b being Element of T holds b_{1} . (a,b) = Tern (a,(x `),b)

for b_{1}, b_{2} being BinOp of the carrier of T st ( for a, b being Element of T holds b_{1} . (a,b) = Tern (a,(x `),b) ) & ( for a, b being Element of T holds b_{2} . (a,b) = Tern (a,(x `),b) ) holds

b_{1} = b_{2}

end;
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 for a, b being Element of T holds it . (a,b) = Tern (a,x,b);

ex b

for a, b being Element of T holds b

proof end;

uniqueness for b

b

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 for a, b being Element of T holds it . (a,b) = Tern (a,(x `),b);

ex b

for a, b being Element of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem JoinDef defines JoinTBA LATTBA_1:def 8 :

for T being Ternary_Boolean_Algebra

for x being Element of T

for b_{3} being BinOp of the carrier of T holds

( b_{3} = JoinTBA (T,x) iff for a, b being Element of T holds b_{3} . (a,b) = Tern (a,x,b) );

for T being Ternary_Boolean_Algebra

for x being Element of T

for b

( b

:: deftheorem MeetDef defines MeetTBA LATTBA_1:def 9 :

for T being Ternary_Boolean_Algebra

for x being Element of T

for b_{3} being BinOp of the carrier of T holds

( b_{3} = MeetTBA (T,x) iff for a, b being Element of T holds b_{3} . (a,b) = Tern (a,(x `),b) );

for T being Ternary_Boolean_Algebra

for x being Element of T

for b

( b

definition

let T be Ternary_Boolean_Algebra;

let x be Element of T;

coherence

LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #) is non empty LattStr ;

;

end;
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 LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #);

coherence

LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #) is non empty LattStr ;

;

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

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

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)

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 `))

for a, b being Element of T holds Tern ((b `),b,a) = Tern (a,b,(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)

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)

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)

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

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;

((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) is Element of L ;

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

((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) is Element of L ;

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

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;

ex b_{1} being TriOp of the carrier of B st

for a, b, c being Element of B holds b_{1} . (a,b,c) = Ros (a,b,c)

for b_{1}, b_{2} being TriOp of the carrier of B st ( for a, b, c being Element of B holds b_{1} . (a,b,c) = Ros (a,b,c) ) & ( for a, b, c being Element of B holds b_{2} . (a,b,c) = Ros (a,b,c) ) holds

b_{1} = b_{2}

end;
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 for a, b, c being Element of B holds it . (a,b,c) = Ros (a,b,c);

ex b

for a, b, c being Element of B holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem RosTrnDef defines RosTrn LATTBA_1:def 12 :

for B being B_Lattice

for b_{2} being TriOp of the carrier of B holds

( b_{2} = RosTrn B iff for a, b, c being Element of B holds b_{2} . (a,b,c) = Ros (a,b,c) );

for B being B_Lattice

for b

( b

definition

let B be Boolean Lattice;

TBAStruct(# the carrier of B,(comp B),(RosTrn B) #) is TBAStruct ;

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

TBAStruct(# the carrier of B,(comp B),(RosTrn B) #) is TBAStruct ;

:: deftheorem defines BA2TBA LATTBA_1:def 13 :

for B being Boolean Lattice holds BA2TBA B = TBAStruct(# the carrier of B,(comp B),(RosTrn B) #);

for B being Boolean Lattice holds BA2TBA B = TBAStruct(# the carrier of B,(comp B),(RosTrn B) #);

definition

let B be Boolean Lattice;

TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn B) #) is TBALattStr ;

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

TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn B) #) is TBALattStr ;

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

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

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

coherence

JoinTBA (T,x) is commutative

end;
let x be Element of T;

coherence

JoinTBA (T,x) is commutative

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

coherence

JoinTBA (T,x) is associative

end;
let x be Element of T;

coherence

JoinTBA (T,x) is associative

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

coherence

MeetTBA (T,x) is commutative

end;
let x be Element of T;

coherence

MeetTBA (T,x) is commutative

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

coherence

MeetTBA (T,x) is associative

end;
let x be Element of T;

coherence

MeetTBA (T,x) is associative

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

LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is Lattice-like

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

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 `

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 `

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;

( BA2TBA B is ternary-left-idempotent & BA2TBA B is ternary-right-idempotent & BA2TBA B is ternary-left-absorbing & BA2TBA B is ternary-right-absorbing )

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

registration

let B be Boolean Lattice;

( BA2TBAA B is ternary-left-idempotent & BA2TBAA B is ternary-right-idempotent & BA2TBAA B is ternary-left-absorbing & BA2TBAA B is ternary-right-absorbing )

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

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

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

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

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 T be Ternary_Boolean_Algebra;

let p be Element of T;

LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is distributive

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

registration

let T be Ternary_Boolean_Algebra;

let p be Element of T;

LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is bounded

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

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

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 `

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;

LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is complemented

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

registration

let T be Ternary_Boolean_Algebra;

let p be Element of T;

LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) is Boolean ;

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

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

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

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

( T is ternary-distributive & T is ternary-left-idempotent & T is ternary-right-idempotent & T is ternary-left-absorbing & T is ternary-right-absorbing );

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

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

for b_{1} being non empty TBAStruct st b_{1} is ternary-distributive & b_{1} is ternary-left-idempotent & b_{1} is ternary-right-idempotent & b_{1} is ternary-left-absorbing & b_{1} is ternary-right-absorbing holds

b_{1} is TBA-like
;

for b_{1} being non empty TBAStruct st b_{1} is TBA-like holds

( b_{1} is ternary-distributive & b_{1} is ternary-left-idempotent & b_{1} is ternary-right-idempotent & b_{1} is ternary-left-absorbing & b_{1} is ternary-right-absorbing )
;

end;

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 b

b

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 b

( b

registration

coherence

for b_{1} being non empty TBAStruct st b_{1} is TBA-like holds

b_{1} is satisfying_TBA1

end;
for b

b

proof end;