:: Several Classes of {BCK}-algebras and Their Properties :: by Tao Sun , Dahai Hu and Xiquan Liang :: :: Received September 19, 2007 :: Copyright (c) 2007-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, BCIALG_1, BINOP_1, SUBSET_1, XXREAL_0, SUPINF_2, XXREAL_2, CARD_FIL, BCIALG_3; notations XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1; constructors BCIALG_1; registrations STRUCT_0, BCIALG_1; requirements SUBSET; begin :: The Basics of General Theory of commutative BCK-algebra definition let IT be non empty BCIStr_0; attr IT is commutative means :: BCIALG_3:def 1 for x,y being Element of IT holds x\(x\y ) = y\(y\x); end; registration cluster BCI-EXAMPLE -> commutative; end; registration cluster commutative for BCK-algebra; end; reserve X for BCK-algebra; reserve x,y for Element of X; reserve IT for non empty Subset of X; theorem :: BCIALG_3:1 X is commutative BCK-algebra iff for x,y being Element of X holds x\(x\y) <= y\(y\x); theorem :: BCIALG_3:2 for X being BCK-algebra holds for x,y being Element of X holds x\ (x\y) <= y & x\(x\y) <= x; theorem :: BCIALG_3:3 X is commutative BCK-algebra iff for x,y being Element of X holds x\y = x\(y\(y\x)); theorem :: BCIALG_3:4 X is commutative BCK-algebra iff for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y))); theorem :: BCIALG_3:5 X is commutative BCK-algebra iff for x,y being Element of X st x <= y holds x= y\(y\x); theorem :: 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 & (x\z)\(x\y) = (y\z)\(y\x) ); theorem :: BCIALG_3:7 X is commutative BCK-algebra implies for x,y being Element of X st x\y =x holds y\x=y; theorem :: BCIALG_3:8 X is commutative BCK-algebra implies for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x; theorem :: BCIALG_3:9 X is commutative BCK-algebra implies for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X); theorem :: BCIALG_3:10 X is commutative BCK-algebra implies for x,y being Element of X holds x\(y\(y\x))=x\y & (x\y)\((x\y)\x)=x\y; theorem :: BCIALG_3:11 X is commutative BCK-algebra implies for x,y,a being Element of X st x <= a holds (a\y)\((a\y)\(a\x)) = (a\y)\(x\y); definition let X be BCI-algebra; let a be Element of X; attr a is being_greatest means :: BCIALG_3:def 2 for x being Element of X holds x\a=0.X; attr a is being_positive means :: BCIALG_3:def 3 0.X\a=0.X; end; begin :: Several Classes of BCI-algebra---commutative BCI-algebra definition let IT be BCI-algebra; attr IT is BCI-commutative means :: BCIALG_3:def 4 for x,y being Element of IT st x\y= 0.IT holds x = y\(y\x); attr IT is BCI-weakly-commutative means :: BCIALG_3:def 5 for x,y being Element of IT holds (x\(x\y))\(0.IT\(x\y)) = y\(y\x); end; registration cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative; end; registration cluster BCI-commutative BCI-weakly-commutative for BCI-algebra; end; theorem :: BCIALG_3:12 for X being BCI-algebra holds ((ex a be Element of X st a is being_greatest) implies X is BCK-algebra); theorem :: BCIALG_3:13 for X being BCI-algebra holds (X is p-Semisimple implies X is BCI-commutative & X is BCI-weakly-commutative ); theorem :: BCIALG_3:14 for X being commutative BCK-algebra holds X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra; theorem :: BCIALG_3:15 X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative; theorem :: 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))) ); theorem :: 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) ); theorem :: BCIALG_3:18 for X being BCI-algebra holds (X is BCI-commutative iff for a being Element of AtomSet(X),x,y being Element of BranchV(a) holds x\(x\y) = y\(y\x) ) ; 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 & x\0.X = x & x\ (x\y) = y\(y\(x\(x\y))) ); 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 & z\y<=z\x holds x<=y ); 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 & x<=z holds x<=y\(y\z) ); begin :: Several Classes of BCK-algebra---bounded BCK-algebra definition let IT be BCK-algebra; attr IT is bounded means :: BCIALG_3:def 6 ex a be Element of IT st a is being_greatest; end; registration cluster BCI-EXAMPLE -> bounded; end; registration cluster bounded commutative for BCK-algebra; end; definition let IT be bounded BCK-algebra; attr IT is involutory means :: 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; theorem :: 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) ); theorem :: 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) ); 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 holds x <= a\y implies y <= a\x ); definition let IT be BCK-algebra; let a be Element of IT; attr a is being_Iseki means :: BCIALG_3:def 8 for x being Element of IT holds x\a=0.IT & a\x=a; end; definition let IT be BCK-algebra; attr IT is Iseki_extension means :: BCIALG_3:def 9 ex a be Element of IT st a is being_Iseki; end; registration cluster BCI-EXAMPLE -> Iseki_extension; end; :: Commutative Ideal definition let X be BCK-algebra; mode Commutative-Ideal of X -> non empty Subset of X means :: BCIALG_3:def 10 0.X in it & for x,y,z being Element of X st (x\y)\z in it & z in it holds x\(y\(y\x)) in it; end; theorem :: BCIALG_3:25 IT is Commutative-Ideal of X implies for x,y being Element of X st x\y in IT holds x\(y\(y\x)) in IT; theorem :: BCIALG_3:26 for X being BCK-algebra st IT is Commutative-Ideal of X holds IT is Ideal of X; theorem :: BCIALG_3:27 IT is Commutative-Ideal of X implies for x,y being Element of X st x\( x\y) in IT holds (y\(y\x))\(x\y) in IT; begin :: Several Classes of BCK-algebra---implicative BCK-algebra definition let IT be BCK-algebra; attr IT is BCK-positive-implicative means :: BCIALG_3:def 11 for x,y,z being Element of IT holds (x\y)\z=(x\z)\(y\z); attr IT is BCK-implicative means :: BCIALG_3:def 12 for x,y being Element of IT holds x \(y\x)=x; end; registration cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative; end; registration cluster Iseki_extension BCK-positive-implicative BCK-implicative bounded commutative for BCK-algebra; end; theorem :: BCIALG_3:28 X is BCK-positive-implicative BCK-algebra iff for x,y being Element of X holds x\y = (x\y)\y; theorem :: BCIALG_3:29 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))); theorem :: BCIALG_3:30 X is BCK-positive-implicative BCK-algebra iff for x,y being Element of X holds x\y = (x\y)\(x\(x\y)); theorem :: BCIALG_3:31 X is BCK-positive-implicative BCK-algebra iff for x,y,z being Element of X holds (x\z)\(y\z) <= (x\y)\z; theorem :: BCIALG_3:32 X is BCK-positive-implicative BCK-algebra iff for x,y being Element of X holds x\y <= (x\y)\y; theorem :: BCIALG_3:33 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); theorem :: BCIALG_3:34 X is BCK-implicative BCK-algebra iff X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra; theorem :: BCIALG_3:35 X is BCK-implicative BCK-algebra iff for x,y being Element of X holds (x\(x\y))\(x\y) = (y\(y\x)); 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 & (x\z)\(x\y) = ((y\z)\(y\ x))\(x\y) ); theorem :: BCIALG_3:37 for X being bounded BCK-algebra,a being Element of X st a is being_greatest holds (X is BCK-implicative iff X is involutory & X is BCK-positive-implicative ); theorem :: BCIALG_3:38 X is BCK-implicative BCK-algebra iff for x,y being Element of X holds x\(x\(y\x)) = 0.X; theorem :: BCIALG_3:39 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))); theorem :: BCIALG_3:40 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); theorem :: BCIALG_3:41 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)); theorem :: BCIALG_3:42 X is BCK-implicative BCK-algebra iff for x,y being Element of X holds (x\(x\y)) = (y\(y\x))\(x\y); theorem :: BCIALG_3:43 for X being bounded commutative BCK-algebra,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 ); theorem :: BCIALG_3:44 for X being bounded commutative BCK-algebra,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 ); theorem :: BCIALG_3:45 for X being bounded commutative BCK-algebra,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) ); theorem :: BCIALG_3:46 for X being bounded commutative BCK-algebra,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 ); theorem :: BCIALG_3:47 for X being bounded commutative BCK-algebra,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) ); theorem :: BCIALG_3:48 for X being bounded commutative BCK-algebra,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) );