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


begin

definition
attrc1 is strict ;
struct BCIStr  ->  1-sorted ;
aggrBCIStr(# carrier, InternalDiff #) ->  BCIStr ;
sel InternalDiff c1 ->  BinOp of the carrier of c1;
end;

registration
cluster non empty strict for BCIStr ;
existence
 ex b1 being BCIStr st
( not b1 is empty & b1 is strict )
proofend;
end;

definition
let A be BCIStr ;
let x, y be Element of A;
funcx \ 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
attrc1 is strict ;
struct BCIStr_0  ->  BCIStr , ZeroStr ;
aggrBCIStr_0(# carrier, InternalDiff, ZeroF #) ->  BCIStr_0 ;
end;

registration
cluster non empty strict for BCIStr_0 ;
existence
 ex b1 being BCIStr_0 st
( not b1 is empty & b1 is strict )
proofend;
end;

definition
let IT be non empty BCIStr_0 ;
let x be Element of IT;
funcx `  ->  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 ;
attrIT 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;
attrIT 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;
attrIT is being_I  means :Def5: :: BCIALG_1:def 5
 for x being Element of IT holds x \ x = 0. IT;
attrIT is being_K  means :Def6: :: BCIALG_1:def 6
 for x, y being Element of IT holds (x \ y) \ x = 0. IT;
attrIT 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;
attrIT 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 Def6 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(# 1,op2,op0 #);
coherence
 BCIStr_0(# 1,op2,op0 #) is BCIStr_0 ;
end;

:: deftheorem  defines BCI-EXAMPLE BCIALG_1:def_9_:_
 BCI-EXAMPLE = BCIStr_0(# 1,op2,op0 #);

registration
cluster BCI-EXAMPLE  -> 1 -element strict ;
coherence
 ( BCI-EXAMPLE is strict & BCI-EXAMPLE is 1 -element ) by CARD_1:49, STRUCT_0:def_19;
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 )
proofend;
end;

registration
cluster non empty strict being_B being_C being_I being_BCI-4 being_BCK-5 for BCIStr_0 ;
existence
 ex b1 being non empty BCIStr_0 st
( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 & b1 is being_BCK-5 )
proofend;
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 b1 being BCI-algebra st
( 0. b1 = 0. X & the carrier of b1 c= the carrier of X & the InternalDiff of b1 = the InternalDiff of X || the carrier of b1 )
proofend;
end;

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

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

definition
let IT be non empty BCIStr_0 ;
let x, y be Element of IT;
predx <= y means :Def11: :: BCIALG_1:def 11
x \ y = 0. IT;
end;

:: deftheorem Def11 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
proofend;

theorem Th2: :: BCIALG_1:2
for X being BCI-algebra
for x being Element of X holds x \ (0. X) = x
proofend;

theorem Th3: :: BCIALG_1:3
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X &amp; y \ z = 0. X holds
x \ z = 0. X
proofend;

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 &amp; (z \ y) \ (z \ x) = 0. X )
proofend;

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 &amp; z \ y <= z \ x )
proofend;

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

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

theorem Th8: :: BCIALG_1:8
for X being BCI-algebra
for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y
proofend;

theorem Th9: :: BCIALG_1:9
for X being BCI-algebra
for x, y being Element of X holds (x \ y) ` = (x `) \ (y `)
proofend;

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

theorem :: BCIALG_1:11
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_BCI-4 &amp; ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X &amp; x \ (0. X) = x ) ) ) )
proofend;

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

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

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

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

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

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

theorem :: BCIALG_1:18
for X being BCI-algebra holds
( X is being_K iff X is BCK-algebra )
proofend;

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

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

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

theorem Th22: :: BCIALG_1:22
for X being BCI-algebra holds X is SubAlgebra of X
proofend;

definition
let X be BCI-algebra;
let IT be SubAlgebra of X;
attrIT 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 b1 being SubAlgebra of X holds b1 is proper
proofend;
end;

definition
let X be BCI-algebra;
let IT be Element of X;
attrIT is atom  means :Def14: :: BCIALG_1:def 14
 for z being Element of X st z \ IT = 0. X holds
z = IT;
end;

:: deftheorem Def14 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
proofend;
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
proofend;

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

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

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

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

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

theorem Th29: :: BCIALG_1:29
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff (x `) ` = x )
proofend;

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

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

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

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

definition
let X be BCI-algebra;
let a, b be Element of AtomSet X;
:: original:\
redefine funca \ 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
proofend;

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

definition
let X be BCI-algebra;
attrX is generated_by_atom  means :Def16: :: BCIALG_1:def 16
 for x being Element of X ex a being Element of AtomSet X st a <= x;
end;

:: deftheorem Def16 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
proofend;
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
proofend;

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

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

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

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

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

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

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) = {}
proofend;

::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 &amp; ( for x, y being Element of X st x \ y in it &amp; y in it holds
x in it ) );
existence
 ex b1 being non empty Subset of X st
( 0. X in b1 &amp; ( for x, y being Element of X st x \ y in b1 &amp; y in b1 holds
x in b1 ) )
proofend;
end;

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

definition
let X be BCI-algebra;
let IT be Ideal of X;
attrIT 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
proofend;

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

registration
let X be BCI-algebra;
cluster non empty closed for Ideal of X;
existence
 ex b1 being Ideal of X st b1 is closed
proofend;
end;

theorem :: BCIALG_1:43
for X being BCI-algebra holds {(0. X)} is closed Ideal of X
proofend;

theorem :: BCIALG_1:44
for X being BCI-algebra holds the carrier of X is closed Ideal of X
proofend;

theorem :: BCIALG_1:45
for X being BCI-algebra holds BCK-part X is closed Ideal of X
proofend;

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

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 &amp; y <= x holds
y in IT
proofend;

begin

definition
let IT be BCI-algebra;
attrIT is associative  means :Def20: :: BCIALG_1:def 20
 for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z);
attrIT is quasi-associative  means :Def21: :: BCIALG_1:def 21
 for x being Element of IT holds (x `) ` = x ` ;
attrIT is positive-implicative  means :Def22: :: BCIALG_1:def 22
 for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)));
attrIT 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);
attrIT is implicative  means :Def24: :: BCIALG_1:def 24
 for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x);
attrIT is weakly-implicative  means :: BCIALG_1:def 25
 for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x;
attrIT is p-Semisimple  means :Def26: :: BCIALG_1:def 26
 for x, y being Element of IT holds x \ (x \ y) = y;
attrIT is alternative  means :Def27: :: BCIALG_1:def 27
 for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y &amp; (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 Def21 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 Def22 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 Def27 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 &amp; (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 &amp; BCI-EXAMPLE is positive-implicative &amp; BCI-EXAMPLE is p-Semisimple &amp; BCI-EXAMPLE is associative &amp; BCI-EXAMPLE is weakly-implicative &amp; BCI-EXAMPLE is weakly-positive-implicative )
proofend;
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 b1 being BCI-algebra st
( b1 is implicative &amp; b1 is positive-implicative &amp; b1 is p-Semisimple &amp; b1 is associative &amp; b1 is weakly-implicative &amp; b1 is weakly-positive-implicative )
proofend;
end;

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

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

theorem Th47: :: BCIALG_1:47
for X being BCI-algebra holds
( X is associative iff for x being Element of X holds x ` = x )
proofend;

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

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 &amp; x \ (0. X) = x ) )
proofend;

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 &amp; x ` = x ) )
proofend;

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 &amp; x \ (0. X) = x ) )
proofend;

begin

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

theorem :: BCIALG_1:53
for X being BCI-algebra st X is p-Semisimple holds
BCK-part X = {(0. X)}
proofend;

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

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

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

theorem Th55: :: 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 )
proofend;

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

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

Lm10:  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) &amp; (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )
proofend;

Lm11:  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
proofend;

Lm12:  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
proofend;

Lm13:  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
proofend;

Lm14:  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 `)
proofend;

Lm15:  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
proofend;

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

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

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

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

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

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

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

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

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

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

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

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 &amp; x \ (0. X) = x ) )
proofend;

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

begin

Lm16:  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) `
proofend;

Lm17:  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) `
proofend;

Lm18:  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
proofend;

Lm19:  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
proofend;

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

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

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

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

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

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

begin

theorem Th76: :: BCIALG_1:76
for X being BCI-algebra
for x, y being Element of X st X is alternative holds
( x ` = x &amp; x \ (x \ y) = y &amp; (x \ y) \ y = x )
proofend;

theorem :: BCIALG_1:77
for X being BCI-algebra
for x, a, b being Element of X st X is alternative &amp; x \ a = x \ b holds
a = b
proofend;

theorem :: BCIALG_1:78
for X being BCI-algebra
for a, x, b being Element of X st X is alternative &amp; a \ x = b \ x holds
a = b
proofend;

theorem :: BCIALG_1:79
for X being BCI-algebra
for x, y being Element of X st X is alternative &amp; x \ y = 0. X holds
x = y
proofend;

theorem :: BCIALG_1:80
for X being BCI-algebra
for x, a, b being Element of X st X is alternative &amp; (x \ a) \ b = 0. X holds
( a = x \ b &amp; b = x \ a )
proofend;

Lm21:  for X being BCI-algebra holds
( X is alternative iff X is associative )
proofend;

Lm22:  for X being BCI-algebra st X is alternative holds
X is implicative
proofend;

registration
cluster non empty being_B being_C being_I being_BCI-4 alternative  ->  associative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is alternative holds
b1 is associative by Lm21;
cluster non empty being_B being_C being_I being_BCI-4 associative  ->  alternative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is associative holds
b1 is alternative by Lm21;
cluster non empty being_B being_C being_I being_BCI-4 alternative  ->  implicative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is alternative holds
b1 is implicative by Lm22;
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
proofend;

theorem :: BCIALG_1:82
for X being BCI-algebra
for y, x being Element of X st X is alternative holds
y \ (y \ (x \ (x \ y))) = y
proofend;

begin

Lm23:  for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative
proofend;

Lm24:  for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra
proofend;

registration
cluster non empty being_B being_C being_I being_BCI-4 associative  ->  weakly-positive-implicative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is associative holds
b1 is weakly-positive-implicative by Lm23;
cluster non empty being_B being_C being_I being_BCI-4 p-Semisimple  ->  weakly-positive-implicative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is p-Semisimple holds
b1 is weakly-positive-implicative by Lm24;
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 &amp; x \ (0. X) = x &amp; (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )
proofend;

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

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

Lm26:  for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )
proofend;

registration
cluster non empty being_B being_C being_I being_BCI-4 positive-implicative  ->  weakly-positive-implicative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is positive-implicative holds
b1 is weakly-positive-implicative by Lm26;
cluster non empty being_B being_C being_I being_BCI-4 alternative  ->  weakly-positive-implicative for BCIStr_0 ;
coherence
 for b1 being BCI-algebra st b1 is alternative holds
b1 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 Lm25;

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 &amp; x \ (0. X) = x &amp; x \ y = ((x \ y) \ y) \ (y `) &amp; (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )
proofend;