:: Several Classes of {BCK}-algebras and Their Properties
:: by Tao Sun , Dahai Hu and Xiquan Liang
::
:: Received September 19, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

definition
let IT be non empty BCIStr_0 ;
attrIT is commutative  means :Def1: :: BCIALG_3:def 1
 for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);
end;

:: deftheorem Def1 defines commutative BCIALG_3:def_1_:_
 for IT being non empty BCIStr_0 holds
( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );

registration
cluster BCI-EXAMPLE  ->  commutative ;
coherence
 BCI-EXAMPLE is commutative
proofend;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative for BCIStr_0 ;
existence
 ex b1 being BCK-algebra st b1 is commutative
proofend;
end;

theorem Th1: :: BCIALG_3:1
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
proofend;

theorem Th2: :: BCIALG_3:2
for X being BCK-algebra
for x, y being Element of X holds
( x \ (x \ y) <= y &amp; x \ (x \ y) <= x )
proofend;

theorem Th3: :: BCIALG_3:3
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proofend;

theorem Th4: :: BCIALG_3:4
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proofend;

theorem Th5: :: BCIALG_3:5
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
proofend;

theorem Th6: :: BCIALG_3:6
for X being non empty BCIStr_0 holds
( X is commutative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x &amp; (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )
proofend;

theorem :: BCIALG_3:7
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X st x \ y = x holds
y \ x = y
proofend;

theorem Th8: :: BCIALG_3:8
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x
proofend;

theorem :: BCIALG_3:9
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X )
proofend;

theorem :: BCIALG_3:10
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y &amp; (x \ y) \ ((x \ y) \ x) = x \ y )
proofend;

theorem :: BCIALG_3:11
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8;

definition
let X be BCI-algebra;
let a be Element of X;
attra is being_greatest  means :Def2: :: BCIALG_3:def 2
 for x being Element of X holds x \ a = 0. X;
attra is being_positive  means :: BCIALG_3:def 3
(0. X) \ a = 0. X;
end;

:: deftheorem Def2 defines being_greatest BCIALG_3:def_2_:_
 for X being BCI-algebra
for a being Element of X holds
( a is being_greatest iff for x being Element of X holds x \ a = 0. X );

:: deftheorem  defines being_positive BCIALG_3:def_3_:_
 for X being BCI-algebra
for a being Element of X holds
( a is being_positive iff (0. X) \ a = 0. X );

begin

definition
let IT be BCI-algebra;
attrIT is BCI-commutative  means :Def4: :: BCIALG_3:def 4
 for x, y being Element of IT st x \ y = 0. IT holds
x = y \ (y \ x);
attrIT is BCI-weakly-commutative  means :Def5: :: BCIALG_3:def 5
 for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x);
end;

:: deftheorem Def4 defines BCI-commutative BCIALG_3:def_4_:_
 for IT being BCI-algebra holds
( IT is BCI-commutative iff for x, y being Element of IT st x \ y = 0. IT holds
x = y \ (y \ x) );

:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def_5_:_
 for IT being BCI-algebra holds
( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) );

registration
cluster BCI-EXAMPLE  ->  BCI-commutative BCI-weakly-commutative ;
coherence
 ( BCI-EXAMPLE is BCI-commutative &amp; BCI-EXAMPLE is BCI-weakly-commutative )
proofend;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 BCI-commutative BCI-weakly-commutative for BCIStr_0 ;
existence
 ex b1 being BCI-algebra st
( b1 is BCI-commutative &amp; b1 is BCI-weakly-commutative )
proofend;
end;

theorem :: BCIALG_3:12
for X being BCI-algebra st ex a being Element of X st a is being_greatest holds
X is BCK-algebra
proofend;

theorem :: BCIALG_3:13
for X being BCI-algebra st X is p-Semisimple holds
( X is BCI-commutative &amp; X is BCI-weakly-commutative )
proofend;

theorem :: BCIALG_3:14
for X being commutative BCK-algebra holds
( X is BCI-commutative BCI-algebra &amp; X is BCI-weakly-commutative BCI-algebra )
proofend;

theorem :: BCIALG_3:15
for X being BCK-algebra st X is BCI-weakly-commutative BCI-algebra holds
X is BCI-commutative
proofend;

theorem Th16: :: BCIALG_3:16
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proofend;

theorem Th17: :: BCIALG_3:17
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )
proofend;

theorem :: BCIALG_3:18
for X being BCI-algebra holds
( X is BCI-commutative iff for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) )
proofend;

theorem :: BCIALG_3:19
for X being non empty BCIStr_0 holds
( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) )
proofend;

theorem :: BCIALG_3:20
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= z &amp; z \ y <= z \ x holds
x <= y )
proofend;

theorem :: BCIALG_3:21
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= y &amp; x <= z holds
x <= y \ (y \ z) )
proofend;

begin

definition
let IT be BCK-algebra;
attrIT is bounded  means :: BCIALG_3:def 6
 ex a being Element of IT st a is being_greatest ;
end;

:: deftheorem  defines bounded BCIALG_3:def_6_:_
 for IT being BCK-algebra holds
( IT is bounded iff ex a being Element of IT st a is being_greatest );

registration
cluster BCI-EXAMPLE  ->  bounded ;
coherence
 BCI-EXAMPLE is bounded
proofend;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded for BCIStr_0 ;
existence
 ex b1 being BCK-algebra st
( b1 is bounded &amp; b1 is commutative )
proofend;
end;

definition
let IT be bounded BCK-algebra;
attrIT is involutory  means :Def7: :: BCIALG_3:def 7
 for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x;
end;

:: deftheorem Def7 defines involutory BCIALG_3:def_7_:_
 for IT being bounded BCK-algebra holds
( IT is involutory iff for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x );

theorem Th22: :: BCIALG_3:22
for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )
proofend;

theorem Th23: :: BCIALG_3:23
for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) )
proofend;

theorem :: BCIALG_3:24
for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x )
proofend;

definition
let IT be BCK-algebra;
let a be Element of IT;
attra is being_Iseki  means :Def8: :: BCIALG_3:def 8
 for x being Element of IT holds
( x \ a = 0. IT &amp; a \ x = a );
end;

:: deftheorem Def8 defines being_Iseki BCIALG_3:def_8_:_
 for IT being BCK-algebra
for a being Element of IT holds
( a is being_Iseki iff for x being Element of IT holds
( x \ a = 0. IT &amp; a \ x = a ) );

definition
let IT be BCK-algebra;
attrIT is Iseki_extension  means :: BCIALG_3:def 9
 ex a being Element of IT st a is being_Iseki ;
end;

:: deftheorem  defines Iseki_extension BCIALG_3:def_9_:_
 for IT being BCK-algebra holds
( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki );

registration
cluster BCI-EXAMPLE  ->  Iseki_extension ;
coherence
 BCI-EXAMPLE is Iseki_extension
proofend;
end;

:: Commutative Ideal
definition
let X be BCK-algebra;
mode Commutative-Ideal of X ->  non empty Subset of X means :Def10: :: BCIALG_3:def 10
( 0. X in it &amp; ( for x, y, z being Element of X st (x \ y) \ z in it &amp; z in it holds
x \ (y \ (y \ x)) in it ) );
existence
 ex b1 being non empty Subset of X st
( 0. X in b1 &amp; ( for x, y, z being Element of X st (x \ y) \ z in b1 &amp; z in b1 holds
x \ (y \ (y \ x)) in b1 ) )
proofend;
end;

:: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def_10_:_
 for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is Commutative-Ideal of X iff ( 0. X in b2 &amp; ( for x, y, z being Element of X st (x \ y) \ z in b2 &amp; z in b2 holds
x \ (y \ (y \ x)) in b2 ) ) );

theorem :: BCIALG_3:25
for X being BCK-algebra
for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT
proofend;

theorem Th26: :: BCIALG_3:26
for X being BCK-algebra
for IT being non empty Subset of X
for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X
proofend;

theorem :: BCIALG_3:27
for X being BCK-algebra
for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT
proofend;

begin

definition
let IT be BCK-algebra;
attrIT is BCK-positive-implicative  means :Def11: :: BCIALG_3:def 11
 for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z);
attrIT is BCK-implicative  means :Def12: :: BCIALG_3:def 12
 for x, y being Element of IT holds x \ (y \ x) = x;
end;

:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def_11_:_
 for IT being BCK-algebra holds
( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) );

:: deftheorem Def12 defines BCK-implicative BCIALG_3:def_12_:_
 for IT being BCK-algebra holds
( IT is BCK-implicative iff for x, y being Element of IT holds x \ (y \ x) = x );

registration
cluster BCI-EXAMPLE  ->  BCK-positive-implicative BCK-implicative ;
coherence
 ( BCI-EXAMPLE is BCK-positive-implicative &amp; BCI-EXAMPLE is BCK-implicative )
proofend;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded Iseki_extension BCK-positive-implicative BCK-implicative for BCIStr_0 ;
existence
 ex b1 being BCK-algebra st
( b1 is Iseki_extension &amp; b1 is BCK-positive-implicative &amp; b1 is BCK-implicative &amp; b1 is bounded &amp; b1 is commutative )
proofend;
end;

theorem Th28: :: BCIALG_3:28
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y )
proofend;

theorem Th29: :: BCIALG_3:29
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )
proofend;

theorem :: BCIALG_3:30
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) )
proofend;

theorem :: BCIALG_3:31
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )
proofend;

theorem :: BCIALG_3:32
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y )
proofend;

theorem :: BCIALG_3:33
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) )
proofend;

theorem Th34: :: BCIALG_3:34
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra &amp; X is BCK-positive-implicative BCK-algebra ) )
proofend;

theorem Th35: :: BCIALG_3:35
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) )
proofend;

theorem :: BCIALG_3:36
for X being non empty BCIStr_0 holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x &amp; (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) )
proofend;

Lm1:  for X being bounded BCK-algebra st X is BCK-implicative holds
for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x
proofend;

theorem Th37: :: BCIALG_3:37
for X being bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff ( X is involutory &amp; X is BCK-positive-implicative ) )
proofend;

theorem :: BCIALG_3:38
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X )
proofend;

theorem :: BCIALG_3:39
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proofend;

theorem Th40: :: BCIALG_3:40
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) )
proofend;

theorem :: BCIALG_3:41
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) )
proofend;

theorem :: BCIALG_3:42
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) )
proofend;

theorem Th43: :: BCIALG_3:43
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )
proofend;

theorem :: BCIALG_3:44
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )
proofend;

theorem :: BCIALG_3:45
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )
proofend;

theorem Th46: :: BCIALG_3:46
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )
proofend;

theorem Th47: :: BCIALG_3:47
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )
proofend;

theorem :: BCIALG_3:48
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
proofend;