:: General Theory of Quasi-Commutative BCI-algebras :: by Tao Sun , Weibo Pan , Chenglong Wu and Xiquan Liang :: :: Received May 13, 2008 :: Copyright (c) 2008-2021 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 NUMBERS, BCIALG_1, SUBSET_1, POLYEQ_1, XBOOLE_0, POWER, ARYTM_3, FUNCT_1, STRUCT_0, XXREAL_0, SUPINF_2, CARD_1, ARYTM_1, NAT_1, BINOP_1, TARSKI, CHORD, FILTER_0, BCIALG_3, BCIALG_5; notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1, ORDINAL1, NUMBERS, XXREAL_0, REAL_1, FUNCT_2, XCMPLX_0, NAT_1, BCIALG_2, BCIALG_3; constructors REAL_1, NAT_1, BCIALG_2, BCIALG_3, XREAL_0, NUMBERS; registrations BCIALG_1, STRUCT_0, ORDINAL1, XXREAL_0, XREAL_0, BCIALG_3, NAT_1, BCIALG_2; requirements SUBSET, NUMERALS, REAL, ARITHM; begin :: The Basics of General Theory of Quasi-Commutative BCI-algebra definition let X be BCI-algebra; let x,y be Element of X; let m,n be Nat; func Polynom (m,n,x,y) -> Element of X equals :: BCIALG_5:def 1 (((x,(x\y)) to_power (m+1)),(y \x)) to_power n; end; reserve X for BCI-algebra; reserve x,y,z for Element of X; reserve i,j,k,l,m,n for Nat; reserve f,g for sequence of the carrier of X; theorem :: BCIALG_5:1 x <= y & y <= z implies x <= z; theorem :: BCIALG_5:2 x <= y & y <= x implies x = y; theorem :: BCIALG_5:3 for X being BCK-algebra,x,y being Element of X holds x\y <= x & ( x,y) to_power (n+1) <= (x,y) to_power n; theorem :: BCIALG_5:4 for X being BCK-algebra,x being Element of X holds (0.X,x) to_power n = 0.X; theorem :: BCIALG_5:5 for X being BCK-algebra,x,y being Element of X st m>=n holds (x,y) to_power m <= (x,y) to_power n; theorem :: BCIALG_5:6 for X being BCK-algebra, x,y being Element of X st m>n & (x,y) to_power n = (x,y) to_power m holds for k being Nat st k >=n holds ( x,y) to_power n = (x,y) to_power k; theorem :: BCIALG_5:7 Polynom (0,0,x,y) = x\(x\y); theorem :: BCIALG_5:8 Polynom (m,n,x,y) = (((Polynom (0,0,x,y),(x\y)) to_power m),(y\x)) to_power n ; theorem :: BCIALG_5:9 Polynom (m+1,n,x,y) = Polynom (m,n,x,y) \ (x\y); theorem :: BCIALG_5:10 Polynom (m,n+1,x,y) = Polynom (m,n,x,y) \ (y\x); theorem :: BCIALG_5:11 Polynom (n+1,n+1,y,x) <= Polynom (n,n+1,x,y); theorem :: BCIALG_5:12 Polynom (n,n+1,x,y) <= Polynom (n,n,y,x); definition let X be BCI-algebra; attr X is quasi-commutative means :: BCIALG_5:def 2 ex i,j,m,n being Element of NAT st for x,y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x); end; registration cluster BCI-EXAMPLE -> quasi-commutative; end; registration cluster quasi-commutative for BCI-algebra; end; definition let i,j,m,n be Nat; mode BCI-algebra of i,j,m,n -> BCI-algebra means :: BCIALG_5:def 3 for x,y being Element of it holds Polynom (i,j,x,y) = Polynom (m,n,y,x); end; theorem :: BCIALG_5:13 X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j; theorem :: BCIALG_5:14 for X being BCI-algebra of i,j,m,n holds for k being Element of NAT holds X is BCI-algebra of i+k,j,m,n+k; theorem :: BCIALG_5:15 for X being BCI-algebra of i,j,m,n holds for k being Element of NAT holds X is BCI-algebra of i,j+k,m+k,n; registration cluster quasi-commutative for BCK-algebra; end; registration let i,j,m,n be Nat; cluster being_BCK-5 for BCI-algebra of i,j,m,n; end; definition let i,j,m,n be Nat; mode BCK-algebra of i,j,m,n is being_BCK-5 BCI-algebra of i,j,m,n; end; theorem :: BCIALG_5:16 X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j; theorem :: BCIALG_5:17 for X being BCK-algebra of i,j,m,n holds for k being Element of NAT holds X is BCK-algebra of i+k,j,m,n+k; theorem :: BCIALG_5:18 for X being BCK-algebra of i,j,m,n holds for k being Element of NAT holds X is BCK-algebra of i,j+k,m+k,n; theorem :: BCIALG_5:19 for X being BCK-algebra of i,j,m,n holds for x,y being Element of X holds (x,y) to_power (i+1) = (x,y) to_power (n+1); theorem :: BCIALG_5:20 for X being BCK-algebra of i,j,m,n holds for x,y being Element of X holds (x,y) to_power (j+1) = (x,y) to_power (m+1); theorem :: BCIALG_5:21 for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j ,j,n; theorem :: BCIALG_5:22 for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j ,m,n; :: The Reduction of the Type of Quasi-Commutative BCK-algebra definition let i,j,m,n; func min(i,j,m,n) -> ExtReal equals :: BCIALG_5:def 4 min(min(i,j),min(m,n)); func max(i,j,m,n) -> ExtReal equals :: BCIALG_5:def 5 max(max(i,j),max(m,n)); end; theorem :: BCIALG_5:23 min(i,j,m,n) = i or min(i,j,m,n) = j or min(i,j,m,n) = m or min(i,j,m, n) = n ; theorem :: BCIALG_5:24 max(i,j,m,n) = i or max(i,j,m,n) = j or max(i,j,m,n) = m or max(i,j,m, n) = n ; theorem :: BCIALG_5:25 i = min(i,j,m,n) implies i<=j & i<=m & i<=n; theorem :: BCIALG_5:26 max(i,j,m,n) >= i & max(i,j,m,n) >= j & max(i,j,m,n) >= m & max( i,j,m,n) >= n; theorem :: BCIALG_5:27 for X being BCK-algebra of i,j,m,n st i = min(i,j,m,n) holds ( i = j implies X is BCK-algebra of i,i,i,i ); theorem :: BCIALG_5:28 for X being BCK-algebra of i,j,m,n st i = min(i,j,m,n) holds ( i < j & i < n implies X is BCK-algebra of i,i+1,i,i+1 ); theorem :: BCIALG_5:29 for X being BCK-algebra of i,j,m,n st i = min(i,j,m,n) holds ( i = n & i = m implies X is BCK-algebra of i,i,i,i ); theorem :: BCIALG_5:30 for X being BCK-algebra of i,j,m,n st i = n & m < j holds X is BCK-algebra of i,m+1,m,i; theorem :: BCIALG_5:31 for X being BCK-algebra of i,j,m,n st i = n holds X is BCK-algebra of i,j,j,i ; theorem :: BCIALG_5:32 for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds X is BCK-algebra of k,l,l,k; theorem :: BCIALG_5:33 for X being BCK-algebra of i,j,m,n st k >= max(i,j,m,n) holds X is BCK-algebra of k,k,k,k; theorem :: BCIALG_5:34 for X being BCK-algebra of i,j,m,n st i <= m & j <= n holds X is BCK-algebra of i,j,i,j; theorem :: BCIALG_5:35 for X being BCK-algebra of i,j,m,n holds ( i <= m & i < n implies X is BCK-algebra of i,j,i,i+1 ); theorem :: BCIALG_5:36 X is BCI-algebra of i,j,j+k,i+k implies X is BCK-algebra; ::Some Special Classes of Quasi-Commutative BCI-algebra theorem :: BCIALG_5:37 X is BCI-algebra of 0,0,0,0 iff X is BCK-algebra of 0,0,0,0; theorem :: BCIALG_5:38 X is commutative BCK-algebra iff X is BCI-algebra of 0,0,0,0; notation let X be BCI-algebra; synonym p-Semisimple-part(X) for AtomSet(X); end; reserve B,P for non empty Subset of X; theorem :: BCIALG_5:39 for X being BCI-algebra st B = BCK-part(X) & P = p-Semisimple-part(X) holds B /\ P = {0.X}; theorem :: BCIALG_5:40 for X being BCI-algebra st P = p-Semisimple-part(X) holds (X is BCK-algebra iff P = {0.X}); theorem :: BCIALG_5:41 for X being BCI-algebra st B = BCK-part(X) holds (X is p-Semisimple BCI-algebra iff B = {0.X}); theorem :: BCIALG_5:42 X is p-Semisimple BCI-algebra implies X is BCI-algebra of 0,1,0, 0; theorem :: BCIALG_5:43 X is p-Semisimple BCI-algebra implies X is BCI-algebra of n+j,n,m,m+j+ 1; theorem :: BCIALG_5:44 X is associative BCI-algebra implies X is BCI-algebra of 0,1,0,0 & X is BCI-algebra of 1,0,0,0; theorem :: BCIALG_5:45 X is weakly-positive-implicative BCI-algebra implies X is BCI-algebra of 0,1,1,1; theorem :: BCIALG_5:46 X is positive-implicative BCI-algebra implies X is BCI-algebra of 0,1, 1,1; theorem :: BCIALG_5:47 X is implicative BCI-algebra implies X is BCI-algebra of 0,1,0,0; theorem :: BCIALG_5:48 X is alternative BCI-algebra implies X is BCI-algebra of 0,1,0,0; theorem :: BCIALG_5:49 X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0,1,0,1; theorem :: BCIALG_5:50 X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1,0,0,0; registration cluster BCK-implicative -> commutative for BCK-algebra; cluster BCK-implicative -> BCK-positive-implicative for BCK-algebra; end; theorem :: BCIALG_5:51 X is BCK-algebra of 1,0,0,0 iff X is BCK-algebra of 0,0,0,0 & X is BCK-algebra of 0,1,0,1; theorem :: BCIALG_5:52 for X being quasi-commutative BCK-algebra holds (X is BCK-algebra of 0 ,1,0,1 iff for x,y being Element of X holds x\y = (x\y)\y ); theorem :: BCIALG_5:53 for X being quasi-commutative BCK-algebra holds (X is BCK-algebra of n ,n+1,n,n+1 iff for x,y being Element of X holds (x,y) to_power (n+1) = (x,y) to_power (n+2) ); theorem :: BCIALG_5:54 X is BCI-algebra of 0,1,0,0 implies X is BCI-commutative BCI-algebra; theorem :: BCIALG_5:55 X is BCI-algebra of n,0,m,m implies X is BCI-commutative BCI-algebra; theorem :: BCIALG_5:56 for X being BCK-algebra of i,j,m,n holds ( j = 0 & m > 0 implies X is BCK-algebra of 0,0,0,0 ); theorem :: BCIALG_5:57 for X being BCK-algebra of i,j,m,n holds ( m = 0 & j > 0 implies X is BCK-algebra of 0,1,0,1 ); theorem :: BCIALG_5:58 for X being BCK-algebra of i,j,m,n holds ( n = 0 & i <> 0 implies X is BCK-algebra of 0,0,0,0 ); theorem :: BCIALG_5:59 for X being BCK-algebra of i,j,m,n holds ( i = 0 & n <> 0 implies X is BCK-algebra of 0,1,0,1 );