:: Several Classes of {BCI}-algebras and Their Properties
:: by Yuzhong Ding
::
:: Received February 23, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct BCIStr -> 1-sorted ;
aggr BCIStr(# carrier, InternalDiff #) -> BCIStr ;
sel InternalDiff c₁ -> BinOp of the carrier of c₁;

end;

registration

cluster non empty strict for BCIStr ;

existence
ex b₁ being BCIStr st
( not b₁ is empty & b₁ is strict )

proof end;

end;

definition

let A be BCIStr ;
let x, y be Element of A;

func x \ y -> Element of A equals :: BCIALG_1:def 1
the InternalDiff of A . (x,y);

coherence
the InternalDiff of A . (x,y) is Element of A ;

end;

:: deftheorem defines \ BCIALG_1:def 1 :
for A being BCIStr
for x, y being Element of A holds x \ y = the InternalDiff of A . (x,y);

definition

attr c₁ is strict ;
struct BCIStr_0 -> BCIStr , ZeroStr ;
aggr BCIStr_0(# carrier, InternalDiff, ZeroF #) -> BCIStr_0 ;

end;

registration

cluster non empty strict for BCIStr_0 ;

existence
ex b₁ being BCIStr_0 st
( not b₁ is empty & b₁ is strict )

proof end;

end;

definition

let IT be non empty BCIStr_0 ;
let x be Element of IT;

func x ` -> Element of IT equals :: BCIALG_1:def 2
(0. IT) \ x;

coherence
(0. IT) \ x is Element of IT ;

end;

:: deftheorem defines ` BCIALG_1:def 2 :
for IT being non empty BCIStr_0
for x being Element of IT holds x ` = (0. IT) \ x;

definition

let IT be non empty BCIStr_0 ;

attr IT is being_B means :Def3: :: BCIALG_1:def 3
for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT;

attr IT is being_C means :Def4: :: BCIALG_1:def 4
for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT;

attr IT is being_I means :Def5: :: BCIALG_1:def 5
for x being Element of IT holds x \ x = 0. IT;

attr IT is being_K means :: BCIALG_1:def 6
for x, y being Element of IT holds (x \ y) \ x = 0. IT;

attr IT is being_BCI-4 means :Def7: :: BCIALG_1:def 7
for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y;

attr IT is being_BCK-5 means :Def8: :: BCIALG_1:def 8
for x being Element of IT holds x ` = 0. IT;

end;

:: deftheorem Def3 defines being_B BCIALG_1:def 3 :
for IT being non empty BCIStr_0 holds
( IT is being_B iff for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT );

:: deftheorem Def4 defines being_C BCIALG_1:def 4 :
for IT being non empty BCIStr_0 holds
( IT is being_C iff for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT );

:: deftheorem Def5 defines being_I BCIALG_1:def 5 :
for IT being non empty BCIStr_0 holds
( IT is being_I iff for x being Element of IT holds x \ x = 0. IT );

:: deftheorem defines being_K BCIALG_1:def 6 :
for IT being non empty BCIStr_0 holds
( IT is being_K iff for x, y being Element of IT holds (x \ y) \ x = 0. IT );

:: deftheorem Def7 defines being_BCI-4 BCIALG_1:def 7 :
for IT being non empty BCIStr_0 holds
( IT is being_BCI-4 iff for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y );

:: deftheorem Def8 defines being_BCK-5 BCIALG_1:def 8 :
for IT being non empty BCIStr_0 holds
( IT is being_BCK-5 iff for x being Element of IT holds x ` = 0. IT );

definition

func BCI-EXAMPLE -> BCIStr_0 equals :: BCIALG_1:def 9
BCIStr_0(# {0},op2,op0 #);

coherence
BCIStr_0(# {0},op2,op0 #) is BCIStr_0 ;

end;

:: deftheorem defines BCI-EXAMPLE BCIALG_1:def 9 :
BCI-EXAMPLE = BCIStr_0(# {0},op2,op0 #);

registration

cluster BCI-EXAMPLE -> 1 -element strict ;

coherence
( BCI-EXAMPLE is strict & BCI-EXAMPLE is 1 -element ) ;

end;

registration

cluster BCI-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5 ;

coherence
( BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) by STRUCT_0:def 10;

end;

registration

cluster non empty strict being_B being_C being_I being_BCI-4 being_BCK-5 for BCIStr_0 ;

existence
ex b₁ being non empty BCIStr_0 st
( b₁ is strict & b₁ is being_B & b₁ is being_C & b₁ is being_I & b₁ is being_BCI-4 & b₁ is being_BCK-5 )

proof end;

end;

definition

mode BCI-algebra is non empty being_B being_C being_I being_BCI-4 BCIStr_0 ;

end;

definition

mode BCK-algebra is being_BCK-5 BCI-algebra;

end;

definition

let X be BCI-algebra;

mode SubAlgebra of X -> BCI-algebra means :Def10: :: BCIALG_1:def 10
( 0. it = 0. X & the carrier of it c= the carrier of X & the InternalDiff of it = the InternalDiff of X || the carrier of it );

existence
ex b₁ being BCI-algebra st
( 0. b₁ = 0. X & the carrier of b₁ c= the carrier of X & the InternalDiff of b₁ = the InternalDiff of X || the carrier of b₁ )

proof end;

end;

:: deftheorem Def10 defines SubAlgebra BCIALG_1:def 10 :
for X, b₂ being BCI-algebra holds
( b₂ is SubAlgebra of X iff ( 0. b₂ = 0. X & the carrier of b₂ c= the carrier of X & the InternalDiff of b₂ = the InternalDiff of X || the carrier of b₂ ) );

::T1.1.11

theorem Th1: :: BCIALG_1:1

for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) )

proof end;

definition

let IT be non empty BCIStr_0 ;
let x, y be Element of IT;

pred x <= y means :: BCIALG_1:def 11
x \ y = 0. IT;

end;

:: deftheorem defines <= BCIALG_1:def 11 :
for IT being non empty BCIStr_0
for x, y being Element of IT holds
( x <= y iff x \ y = 0. IT );

Lm1: for X being BCI-algebra
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X

proof end;

theorem Th2: :: BCIALG_1:2

for X being BCI-algebra
for x being Element of X holds x \ (0. X) = x

proof end;

theorem Th3: :: BCIALG_1:3

for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X

proof end;

theorem Th4: :: BCIALG_1:4

for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )

proof end;

theorem :: BCIALG_1:5

for X being BCI-algebra
for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x ) by Th4;

theorem :: BCIALG_1:6

for X being BCI-algebra
for x, y being Element of X st x \ y = 0. X holds
(y \ x) ` = 0. X

proof end;

theorem Th7: :: BCIALG_1:7

for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y

proof end;

theorem Th8: :: BCIALG_1:8

for X being BCI-algebra
for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y

proof end;

theorem Th9: :: BCIALG_1:9

for X being BCI-algebra
for x, y being Element of X holds (x \ y) ` = (x `) \ (y `)

proof end;

theorem Th10: :: BCIALG_1:10

for X being BCI-algebra
for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X

proof end;

theorem :: BCIALG_1:11

for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )

proof end;

theorem :: BCIALG_1:12

for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds
X is BCK-algebra

proof end;

theorem :: BCIALG_1:13

for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
X is BCK-algebra

proof end;

theorem :: BCIALG_1:14

for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
X is BCK-algebra

proof end;

theorem :: BCIALG_1:15

for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
X is BCK-algebra

proof end;

theorem :: BCIALG_1:16

for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds
X is BCK-algebra

proof end;

theorem :: BCIALG_1:17

for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds
X is BCK-algebra

proof end;

theorem :: BCIALG_1:18

for X being BCI-algebra holds
( X is being_K iff X is BCK-algebra )

proof end;

definition

let X be BCI-algebra;

func BCK-part X -> non empty Subset of X equals :: BCIALG_1:def 12
{ x where x is Element of X : 0. X <= x } ;

coherence
{ x where x is Element of X : 0. X <= x } is non empty Subset of X

proof end;

end;

:: deftheorem defines BCK-part BCIALG_1:def 12 :
for X being BCI-algebra holds BCK-part X = { x where x is Element of X : 0. X <= x } ;

theorem Th19: :: BCIALG_1:19

for X being BCI-algebra holds 0. X in BCK-part X

proof end;

theorem :: BCIALG_1:20

for X being BCI-algebra
for x, y being Element of BCK-part X holds x \ y in BCK-part X

proof end;

theorem :: BCIALG_1:21

for X being BCI-algebra
for x being Element of X
for y being Element of BCK-part X holds x \ y <= x

proof end;

theorem Th22: :: BCIALG_1:22

for X being BCI-algebra holds X is SubAlgebra of X

proof end;

definition

let X be BCI-algebra;
let IT be SubAlgebra of X;

attr IT is proper means :Def13: :: BCIALG_1:def 13
IT <> X;

end;

:: deftheorem Def13 defines proper BCIALG_1:def 13 :
for X being BCI-algebra
for IT being SubAlgebra of X holds
( IT is proper iff IT <> X );

registration

let X be BCI-algebra;

cluster non empty being_B being_C being_I being_BCI-4 non proper for SubAlgebra of X;

existence
not for b₁ being SubAlgebra of X holds b₁ is proper

proof end;

end;

definition

let X be BCI-algebra;
let IT be Element of X;

attr IT is atom means :: BCIALG_1:def 14
for z being Element of X st z \ IT = 0. X holds
z = IT;

end;

:: deftheorem defines atom BCIALG_1:def 14 :
for X being BCI-algebra
for IT being Element of X holds
( IT is atom iff for z being Element of X st z \ IT = 0. X holds
z = IT );

definition

let X be BCI-algebra;

func AtomSet X -> non empty Subset of X equals :: BCIALG_1:def 15
{ x where x is Element of X : x is atom } ;

coherence
{ x where x is Element of X : x is atom } is non empty Subset of X

proof end;

end;

:: deftheorem defines AtomSet BCIALG_1:def 15 :
for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ;

theorem Th23: :: BCIALG_1:23

for X being BCI-algebra holds 0. X in AtomSet X

proof end;

theorem Th24: :: BCIALG_1:24

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )

proof end;

theorem :: BCIALG_1:25

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u )

proof end;

theorem :: BCIALG_1:26

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) )

proof end;

theorem :: BCIALG_1:27

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) )

proof end;

theorem Th28: :: BCIALG_1:28

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z )

proof end;

theorem Th29: :: BCIALG_1:29

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff (x `) ` = x )

proof end;

theorem Th30: :: BCIALG_1:30

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )

proof end;

theorem Th31: :: BCIALG_1:31

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )

proof end;

theorem :: BCIALG_1:32

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )

proof end;

theorem Th33: :: BCIALG_1:33

for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of X holds a \ x in AtomSet X

proof end;

definition

let X be BCI-algebra;
let a, b be Element of AtomSet X;
:: original: \
redefine func a \ b -> Element of AtomSet X;
coherence
a \ b is Element of AtomSet X by Th33;

end;

theorem Th34: :: BCIALG_1:34

for X being BCI-algebra
for x being Element of X holds x ` in AtomSet X

proof end;

theorem Th35: :: BCIALG_1:35

for X being BCI-algebra
for x being Element of X ex a being Element of AtomSet X st a <= x

proof end;

definition

let X be BCI-algebra;

attr X is generated_by_atom means :: BCIALG_1:def 16
for x being Element of X ex a being Element of AtomSet X st a <= x;

end;

:: deftheorem defines generated_by_atom BCIALG_1:def 16 :
for X being BCI-algebra holds
( X is generated_by_atom iff for x being Element of X ex a being Element of AtomSet X st a <= x );

definition

let X be BCI-algebra;
let a be Element of AtomSet X;

func BranchV a -> non empty Subset of X equals :: BCIALG_1:def 17
{ x where x is Element of X : a <= x } ;

coherence
{ x where x is Element of X : a <= x } is non empty Subset of X

proof end;

end;

:: deftheorem defines BranchV BCIALG_1:def 17 :
for X being BCI-algebra
for a being Element of AtomSet X holds BranchV a = { x where x is Element of X : a <= x } ;

theorem :: BCIALG_1:36

for X being BCI-algebra holds X is generated_by_atom by Th35;

theorem :: BCIALG_1:37

for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV b holds a \ x = a \ b

proof end;

theorem Th38: :: BCIALG_1:38

for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a

proof end;

Lm2: for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BranchV a holds a \ x = 0. X

proof end;

theorem Th39: :: BCIALG_1:39

for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b holds x \ y in BranchV (a \ b)

proof end;

theorem :: BCIALG_1:40

for X being BCI-algebra
for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ y in BCK-part X

proof end;

theorem :: BCIALG_1:41

for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X

proof end;

theorem :: BCIALG_1:42

for X being BCI-algebra
for a, b being Element of AtomSet X st a <> b holds
(BranchV a) /\ (BranchV b) = {}

proof end;

::Ideal

definition

let X be BCI-algebra;

mode Ideal of X -> non empty Subset of X means :Def18: :: BCIALG_1:def 18
( 0. X in it & ( for x, y being Element of X st x \ y in it & y in it holds
x in it ) );

existence
ex b₁ being non empty Subset of X st
( 0. X in b₁ & ( for x, y being Element of X st x \ y in b₁ & y in b₁ holds
x in b₁ ) )

proof end;

end;

:: deftheorem Def18 defines Ideal BCIALG_1:def 18 :
for X being BCI-algebra
for b₂ being non empty Subset of X holds
( b₂ is Ideal of X iff ( 0. X in b₂ & ( for x, y being Element of X st x \ y in b₂ & y in b₂ holds
x in b₂ ) ) );

definition

let X be BCI-algebra;
let IT be Ideal of X;

attr IT is closed means :Def19: :: BCIALG_1:def 19
for x being Element of IT holds x ` in IT;

end;

:: deftheorem Def19 defines closed BCIALG_1:def 19 :
for X being BCI-algebra
for IT being Ideal of X holds
( IT is closed iff for x being Element of IT holds x ` in IT );

Lm3: for X being BCI-algebra holds {(0. X)} is Ideal of X

proof end;

Lm4: for X being BCI-algebra
for X1 being Ideal of X st X1 = {(0. X)} holds
for x being Element of X1 holds x ` in {(0. X)}

proof end;

registration

let X be BCI-algebra;

cluster non empty closed for Ideal of X;

existence
ex b₁ being Ideal of X st b₁ is closed

proof end;

end;

theorem :: BCIALG_1:43

for X being BCI-algebra holds {(0. X)} is closed Ideal of X

proof end;

theorem :: BCIALG_1:44

for X being BCI-algebra holds the carrier of X is closed Ideal of X

proof end;

theorem :: BCIALG_1:45

for X being BCI-algebra holds BCK-part X is closed Ideal of X

proof end;

Lm5: for X being BCI-algebra
for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT

proof end;

theorem :: BCIALG_1:46

for X being BCI-algebra
for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of X st x in IT & y <= x holds
y in IT

proof end;

definition

let IT be BCI-algebra;

attr IT is associative means :Def20: :: BCIALG_1:def 20
for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z);

attr IT is quasi-associative means :: BCIALG_1:def 21
for x being Element of IT holds (x `) ` = x ` ;

attr IT is positive-implicative means :: BCIALG_1:def 22
for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)));

attr IT is weakly-positive-implicative means :Def23: :: BCIALG_1:def 23
for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z);

attr IT is implicative means :Def24: :: BCIALG_1:def 24
for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x);

attr IT is weakly-implicative means :: BCIALG_1:def 25
for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x;

attr IT is p-Semisimple means :Def26: :: BCIALG_1:def 26
for x, y being Element of IT holds x \ (x \ y) = y;

attr IT is alternative means :: BCIALG_1:def 27
for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) );

end;

:: deftheorem Def20 defines associative BCIALG_1:def 20 :
for IT being BCI-algebra holds
( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) );

:: deftheorem defines quasi-associative BCIALG_1:def 21 :
for IT being BCI-algebra holds
( IT is quasi-associative iff for x being Element of IT holds (x `) ` = x ` );

:: deftheorem defines positive-implicative BCIALG_1:def 22 :
for IT being BCI-algebra holds
( IT is positive-implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) );

:: deftheorem Def23 defines weakly-positive-implicative BCIALG_1:def 23 :
for IT being BCI-algebra holds
( IT is weakly-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) );

:: deftheorem Def24 defines implicative BCIALG_1:def 24 :
for IT being BCI-algebra holds
( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) );

:: deftheorem defines weakly-implicative BCIALG_1:def 25 :
for IT being BCI-algebra holds
( IT is weakly-implicative iff for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x );

:: deftheorem Def26 defines p-Semisimple BCIALG_1:def 26 :
for IT being BCI-algebra holds
( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y );

:: deftheorem defines alternative BCIALG_1:def 27 :
for IT being BCI-algebra holds
( IT is alternative iff for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) );

registration

cluster BCI-EXAMPLE -> associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple ;

coherence
( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) by STRUCT_0:def 10;

end;

registration

cluster non empty being_B being_C being_I being_BCI-4 associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple for BCIStr_0 ;

existence
ex b₁ being BCI-algebra st
( b₁ is implicative & b₁ is positive-implicative & b₁ is p-Semisimple & b₁ is associative & b₁ is weakly-implicative & b₁ is weakly-positive-implicative )

proof end;

end;

Lm6: for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds
X is associative

proof end;

Lm7: for X being BCI-algebra st ( for x being Element of X holds x ` = x ) holds
for x, y being Element of X holds x \ y = y \ x

proof end;

theorem Th47: :: BCIALG_1:47

for X being BCI-algebra holds
( X is associative iff for x being Element of X holds x ` = x )

proof end;

theorem Th48: :: BCIALG_1:48

for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )

proof end;

theorem Th49: :: BCIALG_1:49

for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )

proof end;

theorem Th50: :: BCIALG_1:50

for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) )

proof end;

theorem :: BCIALG_1:51

for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) )

proof end;

theorem :: BCIALG_1:52

for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds x is atom )

proof end;

theorem :: BCIALG_1:53

for X being BCI-algebra st X is p-Semisimple holds
BCK-part X = {(0. X)}

proof end;

Lm8: for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )

proof end;

theorem Th54: :: BCIALG_1:54

for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds (x `) ` = x )

proof end;

theorem :: BCIALG_1:55

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) ;

theorem Th56: :: BCIALG_1:56

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )

proof end;

theorem Th57: :: BCIALG_1:57

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) )

proof end;

Lm9: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z, u being Element of X holds
( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )

proof end;

Lm10: for X being BCI-algebra st X is p-Semisimple holds
for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y

proof end;

Lm11: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z

proof end;

Lm12: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st x \ y = x \ z holds
y = z

proof end;

Lm13: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `)

proof end;

Lm14: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st y \ x = z \ x holds
y = z

proof end;

theorem :: BCIALG_1:58

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) )

proof end;

theorem Th59: :: BCIALG_1:59

for X being BCI-algebra holds
( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z )

proof end;

theorem :: BCIALG_1:60

for X being BCI-algebra holds
( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z )

proof end;

theorem :: BCIALG_1:61

for X being BCI-algebra holds
( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u )

proof end;

theorem Th62: :: BCIALG_1:62

for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds
x = 0. X )

proof end;

theorem Th63: :: BCIALG_1:63

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) )

proof end;

theorem :: BCIALG_1:64

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) )

proof end;

theorem :: BCIALG_1:65

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )

proof end;

theorem :: BCIALG_1:66

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )

proof end;

theorem :: BCIALG_1:67

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds
y = z )

proof end;

theorem :: BCIALG_1:68

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds
y = z )

proof end;

theorem :: BCIALG_1:69

for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )

proof end;

theorem :: BCIALG_1:70

for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) )

proof end;

Lm15: for X being BCI-algebra st ( for x being Element of X holds x ` <= x ) holds
for x, y being Element of X holds (x \ y) ` = (y \ x) `

proof end;

Lm16: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) holds
for x, y being Element of X holds (x `) \ y = (x \ y) `

proof end;

Lm17: for X being BCI-algebra st ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) holds
for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X

proof end;

Lm18: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) holds
X is quasi-associative

proof end;

Lm19: for X being BCI-algebra holds
( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )

proof end;

theorem Th71: :: BCIALG_1:71

for X being BCI-algebra holds
( X is quasi-associative iff for x being Element of X holds x ` <= x )

proof end;

theorem Th72: :: BCIALG_1:72

for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` )

proof end;

theorem Th73: :: BCIALG_1:73

for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` )

proof end;

theorem :: BCIALG_1:74

for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )

proof end;

theorem :: BCIALG_1:75

for X being BCI-algebra holds
( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )

proof end;

theorem Th76: :: BCIALG_1:76

for X being BCI-algebra
for x, y being Element of X st X is alternative holds
( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )

proof end;

theorem :: BCIALG_1:77

for X being BCI-algebra
for x, a, b being Element of X st X is alternative & x \ a = x \ b holds
a = b

proof end;

theorem :: BCIALG_1:78

for X being BCI-algebra
for x, a, b being Element of X st X is alternative & a \ x = b \ x holds
a = b

proof end;

theorem :: BCIALG_1:79

for X being BCI-algebra
for x, y being Element of X st X is alternative & x \ y = 0. X holds
x = y

proof end;

theorem :: BCIALG_1:80

for X being BCI-algebra
for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds
( a = x \ b & b = x \ a )

proof end;

Lm20: for X being BCI-algebra holds
( X is alternative iff X is associative )

proof end;

Lm21: for X being BCI-algebra st X is alternative holds
X is implicative
by Th76;

registration

cluster non empty being_B being_C being_I being_BCI-4 alternative -> associative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is alternative holds
b₁ is associative by Lm20;

cluster non empty being_B being_C being_I being_BCI-4 associative -> alternative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is associative holds
b₁ is alternative ;

cluster non empty being_B being_C being_I being_BCI-4 alternative -> implicative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is alternative holds
b₁ is implicative by Lm21;

end;

theorem :: BCIALG_1:81

for X being BCI-algebra
for x, y being Element of X st X is alternative holds
(x \ (x \ y)) \ (y \ x) = x

proof end;

theorem :: BCIALG_1:82

for X being BCI-algebra
for x, y being Element of X st X is alternative holds
y \ (y \ (x \ (x \ y))) = y

proof end;

Lm22: for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative

proof end;

Lm23: for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra

proof end;

registration

cluster non empty being_B being_C being_I being_BCI-4 associative -> weakly-positive-implicative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is associative holds
b₁ is weakly-positive-implicative by Lm22;

cluster non empty being_B being_C being_I being_BCI-4 p-Semisimple -> weakly-positive-implicative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is p-Semisimple holds
b₁ is weakly-positive-implicative by Lm23;

end;

theorem :: BCIALG_1:83

for X being non empty BCIStr_0 holds
( X is implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )

proof end;

theorem Th84: :: BCIALG_1:84

for X being BCI-algebra holds
( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )

proof end;

Lm24: for X being BCI-algebra
for x, y being Element of X st X is weakly-positive-implicative holds
(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)

proof end;

Lm25: for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )

proof end;

registration

cluster non empty being_B being_C being_I being_BCI-4 positive-implicative -> weakly-positive-implicative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is positive-implicative holds
b₁ is weakly-positive-implicative by Lm25;

cluster non empty being_B being_C being_I being_BCI-4 alternative -> weakly-positive-implicative for BCIStr_0 ;

coherence
for b₁ being BCI-algebra st b₁ is alternative holds
b₁ is weakly-positive-implicative ;

end;

theorem :: BCIALG_1:85

for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds
for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by Lm24;

theorem :: BCIALG_1:86

for X being non empty BCIStr_0 holds
( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )

proof end;