:: General Theory of Quasi-Commutative BCI-algebras
:: by Tao Sun , Weibo Pan , Chenglong Wu and Xiquan Liang
::
:: Received May 13, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let X be BCI-algebra;
let x, y be Element of X;
let m, n be Element of 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;
coherence
 (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n is Element of X ;
end;

:: deftheorem  defines Polynom BCIALG_5:def_1_:_
 for X being BCI-algebra
for x, y being Element of X
for m, n being Element of NAT holds Polynom (m,n,x,y) = (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n;

theorem Th1: :: BCIALG_5:1
for X being BCI-algebra
for x, y, z being Element of X st x <= y &amp; y <= z holds
x <= z
proofend;

theorem Th2: :: BCIALG_5:2
for X being BCI-algebra
for x, y being Element of X st x <= y &amp; y <= x holds
x = y
proofend;

theorem Th3: :: BCIALG_5:3
for n being Element of NAT
for X being BCK-algebra
for x, y being Element of X holds
( x \ y <= x &amp; (x,y) to_power (n + 1) <= (x,y) to_power n )
proofend;

theorem Th4: :: BCIALG_5:4
for n being Element of NAT
for X being BCK-algebra
for x being Element of X holds ((0. X),x) to_power n = 0. X
proofend;

theorem Th5: :: BCIALG_5:5
for m, n being Element of NAT
for X being BCK-algebra
for x, y being Element of X st m >= n holds
(x,y) to_power m <= (x,y) to_power n
proofend;

theorem Th6: :: BCIALG_5:6
for m, n being Element of NAT
for X being BCK-algebra
for x, y being Element of X st m > n &amp; (x,y) to_power n = (x,y) to_power m holds
for k being Element of NAT st k >= n holds
(x,y) to_power n = (x,y) to_power k
proofend;

theorem Th7: :: BCIALG_5:7
for X being BCI-algebra
for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y)
proofend;

theorem :: BCIALG_5:8
for X being BCI-algebra
for x, y being Element of X
for m, n being Element of NAT holds Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n
proofend;

theorem Th9: :: BCIALG_5:9
for X being BCI-algebra
for x, y being Element of X
for m, n being Element of NAT holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y)
proofend;

theorem Th10: :: BCIALG_5:10
for X being BCI-algebra
for x, y being Element of X
for m, n being Element of NAT holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)
proofend;

theorem :: BCIALG_5:11
for X being BCI-algebra
for y, x being Element of X
for n being Element of NAT holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)
proofend;

theorem :: BCIALG_5:12
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x)
proofend;

definition
let X be BCI-algebra;
attrX is quasi-commutative  means :Def2: :: 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;

:: deftheorem Def2 defines quasi-commutative BCIALG_5:def_2_:_
 for X being BCI-algebra holds
( X is quasi-commutative iff 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) );

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

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

definition
let i, j, m, n be Element of NAT ;
mode BCI-algebra of i,j,m,n ->  BCI-algebra means :Def3: :: BCIALG_5:def 3
 for x, y being Element of it holds Polynom (i,j,x,y) = Polynom (m,n,y,x);
existence
 ex b1 being BCI-algebra st
for x, y being Element of b1 holds Polynom (i,j,x,y) = Polynom (m,n,y,x)
proofend;
end;

:: deftheorem Def3 defines BCI-algebra BCIALG_5:def_3_:_
 for i, j, m, n being Element of NAT
for b5 being BCI-algebra holds
( b5 is BCI-algebra of i,j,m,n iff for x, y being Element of b5 holds Polynom (i,j,x,y) = Polynom (m,n,y,x) );

theorem Th13: :: BCIALG_5:13
for X being BCI-algebra
for i, j, m, n being Element of NAT holds
( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j )
proofend;

theorem Th14: :: BCIALG_5:14
for i, j, m, n being Element of NAT
for X being BCI-algebra of i,j,m,n
for k being Element of NAT holds X is BCI-algebra of i + k,j,m,n + k
proofend;

theorem :: BCIALG_5:15
for i, j, m, n being Element of NAT
for X being BCI-algebra of i,j,m,n
for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n
proofend;

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

registration
let i, j, m, n be Element of NAT ;
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 for BCI-algebra of i,j,m,n;
existence
 ex b1 being BCI-algebra of i,j,m,n st b1 is being_BCK-5
proofend;
end;

definition
let i, j, m, n be Element of 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
for X being BCI-algebra
for i, j, m, n being Element of NAT holds
( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )
proofend;

theorem Th17: :: BCIALG_5:17
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n
for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k
proofend;

theorem Th18: :: BCIALG_5:18
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n
for k being Element of NAT holds X is BCK-algebra of i,j + k,m + k,n
proofend;

theorem Th19: :: BCIALG_5:19
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n
for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)
proofend;

theorem Th20: :: BCIALG_5:20
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n
for x, y being Element of X holds (x,y) to_power (j + 1) = (x,y) to_power (m + 1)
proofend;

theorem Th21: :: BCIALG_5:21
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n
proofend;

theorem Th22: :: BCIALG_5:22
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n
proofend;

:: The Reduction of the Type of Quasi-Commutative BCK-algebra
definition
let i, j, m, n be Element of NAT ;
func min (i,j,m,n) ->  ext-real number  equals :: BCIALG_5:def 4
 min ((min (i,j)),(min (m,n)));
correctness
coherence
min ((min (i,j)),(min (m,n))) is ext-real number ;
;
func max (i,j,m,n) ->  ext-real number  equals :: BCIALG_5:def 5
 max ((max (i,j)),(max (m,n)));
correctness
coherence
max ((max (i,j)),(max (m,n))) is ext-real number ;
;
end;

:: deftheorem  defines min BCIALG_5:def_4_:_
 for i, j, m, n being Element of NAT holds min (i,j,m,n) = min ((min (i,j)),(min (m,n)));

:: deftheorem  defines max BCIALG_5:def_5_:_
 for i, j, m, n being Element of NAT holds max (i,j,m,n) = max ((max (i,j)),(max (m,n)));

theorem :: BCIALG_5:23
for i, j, m, n being Element of NAT holds
( 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 )
proofend;

theorem :: BCIALG_5:24
for i, j, m, n being Element of NAT holds
( 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 )
proofend;

theorem Th25: :: BCIALG_5:25
for i, j, m, n being Element of NAT st i = min (i,j,m,n) holds
( i <= j &amp; i <= m &amp; i <= n )
proofend;

theorem Th26: :: BCIALG_5:26
for i, j, m, n being Element of NAT holds
( max (i,j,m,n) >= i &amp; max (i,j,m,n) >= j &amp; max (i,j,m,n) >= m &amp; max (i,j,m,n) >= n )
proofend;

theorem Th27: :: BCIALG_5:27
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) &amp; i = j holds
X is BCK-algebra of i,i,i,i
proofend;

theorem :: BCIALG_5:28
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) &amp; i < j &amp; i < n holds
X is BCK-algebra of i,i + 1,i,i + 1
proofend;

theorem :: BCIALG_5:29
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) &amp; i = n &amp; i = m holds
X is BCK-algebra of i,i,i,i
proofend;

theorem :: BCIALG_5:30
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i = n &amp; m < j holds
X is BCK-algebra of i,m + 1,m,i
proofend;

theorem :: BCIALG_5:31
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i = n holds
X is BCK-algebra of i,j,j,i
proofend;

theorem :: BCIALG_5:32
for i, j, m, n, l, k being Element of NAT
for X being BCK-algebra of i,j,m,n st l >= j &amp; k >= n holds
X is BCK-algebra of k,l,l,k
proofend;

theorem :: BCIALG_5:33
for i, j, m, n, k being Element of NAT
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
proofend;

theorem :: BCIALG_5:34
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i <= m &amp; j <= n holds
X is BCK-algebra of i,j,i,j
proofend;

theorem :: BCIALG_5:35
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i <= m &amp; i < n holds
X is BCK-algebra of i,j,i,i + 1
proofend;

theorem Th36: :: BCIALG_5:36
for X being BCI-algebra
for i, j, k being Element of NAT st X is BCI-algebra of i,j,j + k,i + k holds
X is BCK-algebra
proofend;

::Some Special Classes of Quasi-Commutative BCI-algebra
theorem Th37: :: BCIALG_5:37
for X being BCI-algebra holds
( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 )
proofend;

theorem Th38: :: BCIALG_5:38
for X being BCI-algebra holds
( X is commutative BCK-algebra iff X is BCI-algebra of 0 , 0 , 0 , 0 )
proofend;

notation
let X be BCI-algebra;
synonym  p-Semisimple-part X for  AtomSet X;
end;

theorem :: BCIALG_5:39
for X being BCI-algebra
for B, P being non empty Subset of X
for X being BCI-algebra st B = BCK-part X &amp; P = p-Semisimple-part X holds
B /\ P = {(0. X)}
proofend;

theorem :: BCIALG_5:40
for X being BCI-algebra
for P being non empty Subset of X
for X being BCI-algebra st P = p-Semisimple-part X holds
( X is BCK-algebra iff P = {(0. X)} )
proofend;

theorem :: BCIALG_5:41
for X being BCI-algebra
for B being non empty Subset of X
for X being BCI-algebra st B = BCK-part X holds
( X is p-Semisimple BCI-algebra iff B = {(0. X)} )
proofend;

theorem Th42: :: BCIALG_5:42
for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of 0 ,1, 0 , 0
proofend;

theorem :: BCIALG_5:43
for X being BCI-algebra
for n, j, m being Element of NAT st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of n + j,n,m,(m + j) + 1
proofend;

theorem :: BCIALG_5:44
for X being BCI-algebra st X is associative BCI-algebra holds
( X is BCI-algebra of 0 ,1, 0 , 0 &amp; X is BCI-algebra of 1, 0 , 0 , 0 )
proofend;

theorem :: BCIALG_5:45
for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds
X is BCI-algebra of 0 ,1,1,1
proofend;

theorem :: BCIALG_5:46
for X being BCI-algebra st X is positive-implicative BCI-algebra holds
X is BCI-algebra of 0 ,1,1,1
proofend;

theorem :: BCIALG_5:47
for X being BCI-algebra st X is implicative BCI-algebra holds
X is BCI-algebra of 0 ,1, 0 , 0
proofend;

theorem :: BCIALG_5:48
for X being BCI-algebra st X is alternative BCI-algebra holds
X is BCI-algebra of 0 ,1, 0 , 0
proofend;

theorem Th49: :: BCIALG_5:49
for X being BCI-algebra holds
( X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0 ,1, 0 ,1 )
proofend;

theorem Th50: :: BCIALG_5:50
for X being BCI-algebra holds
( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 )
proofend;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative  ->  commutative for BCIStr_0 ;
coherence
 for b1 being BCK-algebra st b1 is BCK-implicative holds
b1 is commutative by BCIALG_3:34;
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative  ->  BCK-positive-implicative for BCIStr_0 ;
coherence
 for b1 being BCK-algebra st b1 is BCK-implicative holds
b1 is BCK-positive-implicative by BCIALG_3:34;
end;

theorem :: BCIALG_5:51
for X being BCI-algebra holds
( X is BCK-algebra of 1, 0 , 0 , 0 iff ( X is BCK-algebra of 0 , 0 , 0 , 0 &amp; X is BCK-algebra of 0 ,1, 0 ,1 ) )
proofend;

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

theorem :: BCIALG_5:53
for n being Element of NAT
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) )
proofend;

theorem :: BCIALG_5:54
for X being BCI-algebra st X is BCI-algebra of 0 ,1, 0 , 0 holds
X is BCI-commutative BCI-algebra
proofend;

theorem :: BCIALG_5:55
for X being BCI-algebra
for n, m being Element of NAT st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra
proofend;

theorem :: BCIALG_5:56
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st j = 0 &amp; m > 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
proofend;

theorem :: BCIALG_5:57
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st m = 0 &amp; j > 0 holds
X is BCK-algebra of 0 ,1, 0 ,1
proofend;

theorem :: BCIALG_5:58
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st n = 0 &amp; i <> 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
proofend;

theorem :: BCIALG_5:59
for i, j, m, n being Element of NAT
for X being BCK-algebra of i,j,m,n st i = 0 &amp; n <> 0 holds
X is BCK-algebra of 0 ,1, 0 ,1
proofend;