:: BCIALG_5 semantic presentation

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 & y <= z holds
x <= z
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X st x <= y & y <= z holds
x <= z
let x, y, z be Element of X; ::_thesis: ( x <= y & y <= z implies x <= z )
assume  ( x <= y & y <= z ) ; ::_thesis: x <= z
then  ( x \ y = 0. X & y \ z = 0. X ) by BCIALG_1:def_11;
hence  x \ z = 0. X by BCIALG_1:3; :: according to BCIALG_1:def_11 ::_thesis: verum
end;

theorem Th2: :: BCIALG_5:2
for X being BCI-algebra
for x, y being Element of X st x <= y & y <= x holds
x = y
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X st x <= y & y <= x holds
x = y
let x, y be Element of X; ::_thesis: ( x <= y & y <= x implies x = y )
assume  ( x <= y & y <= x ) ; ::_thesis: x = y
then  ( x \ y = 0. X & y \ x = 0. X ) by BCIALG_1:def_11;
hence  x = y by BCIALG_1:def_7; ::_thesis: verum
end;

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 & (x,y) to_power (n + 1) <= (x,y) to_power n )
proof
let n be Element of NAT ; ::_thesis: for X being BCK-algebra
for x, y being Element of X holds
( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )
let X be BCK-algebra; ::_thesis: for x, y being Element of X holds
( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )
let x, y be Element of X; ::_thesis: ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )
(((x,y) to_power n) \ y) \ ((x,y) to_power n) = (((x,y) to_power n) \ ((x,y) to_power n)) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then A1: ((x,y) to_power n) \ y <= (x,y) to_power n by BCIALG_1:def_11;
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence  ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n ) by A1, BCIALG_1:def_11, BCIALG_2:4; ::_thesis: verum
end;

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
proof
let n be Element of NAT ; ::_thesis: for X being BCK-algebra
for x being Element of X holds ((0. X),x) to_power n = 0. X
let X be BCK-algebra; ::_thesis: for x being Element of X holds ((0. X),x) to_power n = 0. X
let x be Element of X; ::_thesis: ((0. X),x) to_power n = 0. X
defpred S1[ Element of NAT ] means ( $1 <= n implies ((0. X),x) to_power $1 = 0. X );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_((0._X),x)_to_power_k_=_0._X_)_&_k_+_1_<=_n_holds_
((0._X),x)_to_power_(k_+_1)_=_0._X
let k be Element of NAT ; ::_thesis: ( ( k <= n implies ((0. X),x) to_power k = 0. X ) & k + 1 <= n implies ((0. X),x) to_power (k + 1) = 0. X )
assume A1: ( k <= n implies ((0. X),x) to_power k = 0. X ) ; ::_thesis: ( k + 1 <= n implies ((0. X),x) to_power (k + 1) = 0. X )
set m = k + 1;
assume  k + 1 <= n ; ::_thesis: ((0. X),x) to_power (k + 1) = 0. X
then ((0. X),x) to_power (k + 1) = x ` by A1, BCIALG_2:4, NAT_1:13
.= 0. X by BCIALG_1:def_8 ;
hence  ((0. X),x) to_power (k + 1) = 0. X ; ::_thesis: verum
end;
then A2: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A3: S1[ 0 ] by BCIALG_2:1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  ((0. X),x) to_power n = 0. X ; ::_thesis: verum
end;

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
proof
let m, n be Element of NAT ; ::_thesis: 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
let X be BCK-algebra; ::_thesis: for x, y being Element of X st m >= n holds
(x,y) to_power m <= (x,y) to_power n
let x, y be Element of X; ::_thesis: ( m >= n implies (x,y) to_power m <= (x,y) to_power n )
assume  m >= n ; ::_thesis: (x,y) to_power m <= (x,y) to_power n
then  m - n is Element of NAT by NAT_1:21;
then consider k being Element of NAT  such that
A1: k = m - n ;
((x,y) to_power k) \ x = ((x \ x),y) to_power k by BCIALG_2:7
.= ((0. X),y) to_power k by BCIALG_1:def_5
.= 0. X by Th4 ;
then  (x,y) to_power k <= x by BCIALG_1:def_11;
then  (((x,y) to_power k),y) to_power n <= (x,y) to_power n by BCIALG_2:19;
then  (x,y) to_power (k + n) <= (x,y) to_power n by BCIALG_2:10;
hence  (x,y) to_power m <= (x,y) to_power n by A1; ::_thesis: verum
end;

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 & (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
proof
let m, n be Element of NAT ; ::_thesis: for X being BCK-algebra
for x, y being Element of X st m > n & (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
let X be BCK-algebra; ::_thesis: for x, y being Element of X st m > n & (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
let x, y be Element of X; ::_thesis: ( m > n & (x,y) to_power n = (x,y) to_power m implies for k being Element of NAT st k >= n holds
(x,y) to_power n = (x,y) to_power k )
assume that
A1: m > n and
A2: (x,y) to_power n = (x,y) to_power m ; ::_thesis: for k being Element of NAT st k >= n holds
(x,y) to_power n = (x,y) to_power k
 ( m - n is Element of NAT & m - n > n - n ) by A1, NAT_1:21, XREAL_1:9;
then  m - n >= 1 by NAT_1:14;
then  (m - n) + n >= 1 + n by XREAL_1:6;
then A3: (x,y) to_power n <= (x,y) to_power (n + 1) by A2, Th5;
A4: (x,y) to_power (n + 1) <= (x,y) to_power n by Th3;
 for k being Element of NAT st k >= n holds
(x,y) to_power n = (x,y) to_power k
proof
let k be Element of NAT ; ::_thesis: ( k >= n implies (x,y) to_power n = (x,y) to_power k )
assume  k >= n ; ::_thesis: (x,y) to_power n = (x,y) to_power k
then  k - n is Element of NAT by NAT_1:21;
then consider k1 being Element of NAT  such that
A5: k1 = k - n ;
 (x,y) to_power n = (((x,y) to_power n),y) to_power k1
proof
defpred S1[ Element of NAT ] means ( $1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power $1 );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_k1_implies_(x,y)_to_power_n_=_(((x,y)_to_power_n),y)_to_power_k_)_&_k_+_1_<=_k1_holds_
(x,y)_to_power_n_=_(((x,y)_to_power_n),y)_to_power_(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( k <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power k ) & k + 1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) )
assume A6: ( k <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power k ) ; ::_thesis: ( k + 1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) )
set m = k + 1;
A7: (((x,y) to_power n),y) to_power (k + 1) = ((((x,y) to_power n),y) to_power k) \ y by BCIALG_2:4
.= ((((x,y) to_power n) \ y),y) to_power k by BCIALG_2:7
.= (((x,y) to_power (n + 1)),y) to_power k by BCIALG_2:4
.= (((x,y) to_power n),y) to_power k by A4, A3, Th2 ;
assume  k + 1 <= k1 ; ::_thesis: (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1)
hence  (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) by A6, A7, NAT_1:13; ::_thesis: verum
end;
then A8: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A9: S1[ 0 ] by BCIALG_2:1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A8);
hence  (x,y) to_power n = (((x,y) to_power n),y) to_power k1 ; ::_thesis: verum
end;
then  (x,y) to_power n = (x,y) to_power (n + k1) by BCIALG_2:10;
hence  (x,y) to_power n = (x,y) to_power k by A5; ::_thesis: verum
end;
hence  for k being Element of NAT st k >= n holds
(x,y) to_power n = (x,y) to_power k ; ::_thesis: verum
end;

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)
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y)
let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) = x \ (x \ y)
Polynom (0,0,x,y) = (x,(x \ y)) to_power (0 + 1) by BCIALG_2:1
.= x \ (x \ y) by BCIALG_2:2 ;
hence  Polynom (0,0,x,y) = x \ (x \ y) ; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: 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
let x, y be Element of X; ::_thesis: 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
let m, n be Element of NAT ; ::_thesis: Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n
((Polynom (0,0,x,y)),(x \ y)) to_power m = ((x \ (x \ y)),(x \ y)) to_power m by Th7
.= ((x,(x \ y)) to_power m) \ (x \ y) by BCIALG_2:7
.= (x,(x \ y)) to_power (m + 1) by BCIALG_2:4 ;
hence  Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n ; ::_thesis: verum
end;

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)
proof
let X be BCI-algebra; ::_thesis: 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)
let x, y be Element of X; ::_thesis: for m, n being Element of NAT holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y)
let m, n be Element of NAT ; ::_thesis: Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y)
Polynom ((m + 1),n,x,y) = (((x,(y \ x)) to_power n),(x \ y)) to_power ((m + 1) + 1) by BCIALG_2:11
.= ((((x,(y \ x)) to_power n),(x \ y)) to_power (m + 1)) \ (x \ y) by BCIALG_2:4
.= ((((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n) \ (x \ y) by BCIALG_2:11 ;
hence  Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y) ; ::_thesis: verum
end;

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)
proof
let X be BCI-algebra; ::_thesis: 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)
let x, y be Element of X; ::_thesis: for m, n being Element of NAT holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)
let m, n be Element of NAT ; ::_thesis: Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)
consider f being Function of NAT, the carrier of X such that
A1: (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power (n + 1) = f . (n + 1) and
A2: f . 0 = (x,(x \ y)) to_power (m + 1) and
A3: for k being Element of NAT st k < n + 1 holds
f . (k + 1) = (f . k) \ (y \ x) by BCIALG_2:def_1;
consider g being Function of NAT, the carrier of X such that
A4: (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n = g . n and
A5: g . 0 = (x,(x \ y)) to_power (m + 1) and
A6: for k being Element of NAT st k < n holds
g . (k + 1) = (g . k) \ (y \ x) by BCIALG_2:def_1;
defpred S1[ Element of NAT ] means ( $1 <= n implies f . $1 = g . $1 );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_f_._k_=_g_._k_)_&_k_+_1_<=_n_holds_
f_._(k_+_1)_=_g_._(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( k <= n implies f . k = g . k ) & k + 1 <= n implies f . (k + 1) = g . (k + 1) )
assume A7: ( k <= n implies f . k = g . k ) ; ::_thesis: ( k + 1 <= n implies f . (k + 1) = g . (k + 1) )
set m = k + 1;
assume A8: k + 1 <= n ; ::_thesis: f . (k + 1) = g . (k + 1)
then  k + 1 <= n + 1 by NAT_1:13;
then  k < n + 1 by NAT_1:13;
then A9: f . (k + 1) = (f . k) \ (y \ x) by A3;
 k < n by A8, NAT_1:13;
hence  f . (k + 1) = g . (k + 1) by A6, A7, A9; ::_thesis: verum
end;
then A10: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A11: S1[ 0 ] by A2, A5;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A11, A10);
then  f . n = g . n ;
hence  Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) by A1, A3, A4, XREAL_1:29; ::_thesis: verum
end;

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)
proof
let X be BCI-algebra; ::_thesis: 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)
let y, x be Element of X; ::_thesis: for n being Element of NAT holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)
let n be Element of NAT ; ::_thesis: Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)
 (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5;
then  (y \ (y \ x)) \ x = 0. X by BCIALG_1:7;
then  y \ (y \ x) <= x by BCIALG_1:def_11;
then  ((y \ (y \ x)),(x \ y)) to_power (n + 1) <= (x,(x \ y)) to_power (n + 1) by BCIALG_2:19;
then  ((((y \ (y \ x)),(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:19;
then  ((((y \ (y \ x)),(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:11;
then  (((((y,(y \ x)) to_power 1),(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:2;
hence  Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) by BCIALG_2:10; ::_thesis: verum
end;

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)
proof
let X be BCI-algebra; ::_thesis: 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)
let x, y be Element of X; ::_thesis: for n being Element of NAT holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x)
let n be Element of NAT ; ::_thesis: Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x)
 (x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5;
then  (x \ (x \ y)) \ y = 0. X by BCIALG_1:7;
then  x \ (x \ y) <= y by BCIALG_1:def_11;
then  ((x \ (x \ y)),(x \ y)) to_power n <= (y,(x \ y)) to_power n by BCIALG_2:19;
then  ((((x \ (x \ y)),(x \ y)) to_power n),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power n),(y \ x)) to_power (n + 1) by BCIALG_2:19;
then  (((((x,(x \ y)) to_power 1),(x \ y)) to_power n),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power n),(y \ x)) to_power (n + 1) by BCIALG_2:2;
then  (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power n),(y \ x)) to_power (n + 1) by BCIALG_2:10;
hence  Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x) by BCIALG_2:11; ::_thesis: verum
end;

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
proof
 for x, y being Element of BCI-EXAMPLE holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by STRUCT_0:def_10;
hence  BCI-EXAMPLE is quasi-commutative by Def2; ::_thesis: verum
end;
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
proof
take  BCI-EXAMPLE ; ::_thesis: BCI-EXAMPLE is quasi-commutative
thus  BCI-EXAMPLE is quasi-commutative ; ::_thesis: verum
end;
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)
proof
 for x, y being Element of BCI-EXAMPLE holds Polynom (i,j,x,y) = Polynom (m,n,y,x) by STRUCT_0:def_10;
hence  ex b1 being BCI-algebra st
for x, y being Element of b1 holds Polynom (i,j,x,y) = Polynom (m,n,y,x) ; ::_thesis: verum
end;
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 )
proof
let X be BCI-algebra; ::_thesis: 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 )
let i, j, m, n be Element of NAT ; ::_thesis: ( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j )
thus  ( X is BCI-algebra of i,j,m,n implies X is BCI-algebra of m,n,i,j ) ::_thesis: ( X is BCI-algebra of m,n,i,j implies X is BCI-algebra of i,j,m,n )
proof
assume  X is BCI-algebra of i,j,m,n ; ::_thesis: X is BCI-algebra of m,n,i,j
then  for x, y being Element of X holds Polynom (m,n,x,y) = Polynom (i,j,y,x) by Def3;
hence  X is BCI-algebra of m,n,i,j by Def3; ::_thesis: verum
end;
assume  X is BCI-algebra of m,n,i,j ; ::_thesis: X is BCI-algebra of i,j,m,n
then  for x, y being Element of X holds Polynom (m,n,y,x) = Polynom (i,j,x,y) by Def3;
hence  X is BCI-algebra of i,j,m,n by Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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
let X be BCI-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCI-algebra of i + k,j,m,n + k
let k be Element of NAT ; ::_thesis: X is BCI-algebra of i + k,j,m,n + k
 for x, y being Element of X holds Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x)
proof
let x, y be Element of X; ::_thesis: Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x)
A1: ((Polynom (m,n,y,x)),(x \ y)) to_power k = Polynom (m,(n + k),y,x) by BCIALG_2:10;
((Polynom (i,j,x,y)),(x \ y)) to_power k = (((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power k),(y \ x)) to_power j by BCIALG_2:11
.= (((x,(x \ y)) to_power ((i + 1) + k)),(y \ x)) to_power j by BCIALG_2:10
.= Polynom ((i + k),j,x,y) ;
hence  Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) by A1, Def3; ::_thesis: verum
end;
hence  X is BCI-algebra of i + k,j,m,n + k by Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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
let X be BCI-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n
let k be Element of NAT ; ::_thesis: X is BCI-algebra of i,j + k,m + k,n
 for x, y being Element of X holds Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)
A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11
.= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10
.= Polynom ((m + k),n,y,x) ;
 ((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10;
hence  Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; ::_thesis: verum
end;
hence  X is BCI-algebra of i,j + k,m + k,n by Def3; ::_thesis: verum
end;

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
proof
take  BCI-EXAMPLE ; ::_thesis: BCI-EXAMPLE is quasi-commutative
thus  BCI-EXAMPLE is quasi-commutative ; ::_thesis: verum
end;
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
proof
 for x, y being Element of BCI-EXAMPLE holds Polynom (i,j,x,y) = Polynom (m,n,y,x) by STRUCT_0:def_10;
then reconsider B = BCI-EXAMPLE as BCI-algebra of i,j,m,n by Def3;
take  B ; ::_thesis: B is being_BCK-5
thus  B is being_BCK-5 ; ::_thesis: verum
end;
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 )
proof
let X be BCI-algebra; ::_thesis: 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 )
let i, j, m, n be Element of NAT ; ::_thesis: ( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )
thus  ( X is BCK-algebra of i,j,m,n implies X is BCK-algebra of m,n,i,j ) ::_thesis: ( X is BCK-algebra of m,n,i,j implies X is BCK-algebra of i,j,m,n )
proof
assume A1: X is BCK-algebra of i,j,m,n ; ::_thesis: X is BCK-algebra of m,n,i,j
then  for x, y being Element of X holds Polynom (m,n,x,y) = Polynom (i,j,y,x) by Def3;
hence  X is BCK-algebra of m,n,i,j by A1, Def3; ::_thesis: verum
end;
assume A2: X is BCK-algebra of m,n,i,j ; ::_thesis: X is BCK-algebra of i,j,m,n
then  for x, y being Element of X holds Polynom (m,n,y,x) = Polynom (i,j,x,y) by Def3;
hence  X is BCK-algebra of i,j,m,n by A2, Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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
let X be BCK-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k
let k be Element of NAT ; ::_thesis: X is BCK-algebra of i + k,j,m,n + k
 for x, y being Element of X holds Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x)
proof
let x, y be Element of X; ::_thesis: Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x)
A1: ((Polynom (m,n,y,x)),(x \ y)) to_power k = Polynom (m,(n + k),y,x) by BCIALG_2:10;
((Polynom (i,j,x,y)),(x \ y)) to_power k = (((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power k),(y \ x)) to_power j by BCIALG_2:11
.= (((x,(x \ y)) to_power ((i + 1) + k)),(y \ x)) to_power j by BCIALG_2:10
.= Polynom ((i + k),j,x,y) ;
hence  Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) by A1, Def3; ::_thesis: verum
end;
hence  X is BCK-algebra of i + k,j,m,n + k by Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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
let X be BCK-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCK-algebra of i,j + k,m + k,n
let k be Element of NAT ; ::_thesis: X is BCK-algebra of i,j + k,m + k,n
 for x, y being Element of X holds Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)
A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11
.= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10
.= Polynom ((m + k),n,y,x) ;
 ((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10;
hence  Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; ::_thesis: verum
end;
hence  X is BCK-algebra of i,j + k,m + k,n by Def3; ::_thesis: verum
end;

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)
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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)
let X be BCK-algebra of i,j,m,n; ::_thesis: for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)
let x, y be Element of X; ::_thesis: (x,y) to_power (i + 1) = (x,y) to_power (n + 1)
A1: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then A2: Polynom ((m + 1),n,(x \ y),x) = ((x \ y),(x \ (x \ y))) to_power n by BCIALG_2:5
.= ((x \ (x \ (x \ y))),(x \ (x \ y))) to_power n by BCIALG_1:8
.= (((x,(x \ (x \ y))) to_power 1),(x \ (x \ y))) to_power n by BCIALG_2:2
.= (x,(x \ (x \ y))) to_power (n + 1) by BCIALG_2:10
.= (x,y) to_power (n + 1) by BCIALG_2:8 ;
 X is BCI-algebra of m,n,i,j by Th13;
then A3: X is BCI-algebra of m + 1,n,i,j + 1 by Th14;
Polynom (i,(j + 1),x,(x \ y)) = (x,(x \ (x \ y))) to_power (i + 1) by A1, BCIALG_2:5
.= (x,y) to_power (i + 1) by BCIALG_2:8 ;
hence  (x,y) to_power (i + 1) = (x,y) to_power (n + 1) by A2, A3, Def3; ::_thesis: verum
end;

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)
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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)
let X be BCK-algebra of i,j,m,n; ::_thesis: for x, y being Element of X holds (x,y) to_power (j + 1) = (x,y) to_power (m + 1)
let x, y be Element of X; ::_thesis: (x,y) to_power (j + 1) = (x,y) to_power (m + 1)
A1: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then A2: Polynom ((i + 1),j,(x \ y),x) = ((x \ y),(x \ (x \ y))) to_power j by BCIALG_2:5
.= ((x \ (x \ (x \ y))),(x \ (x \ y))) to_power j by BCIALG_1:8
.= (((x,(x \ (x \ y))) to_power 1),(x \ (x \ y))) to_power j by BCIALG_2:2
.= (x,(x \ (x \ y))) to_power (j + 1) by BCIALG_2:10
.= (x,y) to_power (j + 1) by BCIALG_2:8 ;
A3: X is BCI-algebra of i + 1,j,m,n + 1 by Th14;
Polynom (m,(n + 1),x,(x \ y)) = (x,(x \ (x \ y))) to_power (m + 1) by A1, BCIALG_2:5
.= (x,y) to_power (m + 1) by BCIALG_2:8 ;
hence  (x,y) to_power (j + 1) = (x,y) to_power (m + 1) by A2, A3, Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n
let X be BCK-algebra of i,j,m,n; ::_thesis: X is BCK-algebra of i,j,j,n
 for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (j,n,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) = Polynom (j,n,y,x)
 Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
hence  Polynom (i,j,x,y) = Polynom (j,n,y,x) by Th20; ::_thesis: verum
end;
hence  X is BCK-algebra of i,j,j,n by Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n
let X be BCK-algebra of i,j,m,n; ::_thesis: X is BCK-algebra of n,j,m,n
 for x, y being Element of X holds Polynom (n,j,x,y) = Polynom (m,n,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (n,j,x,y) = Polynom (m,n,y,x)
 Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
hence  Polynom (n,j,x,y) = Polynom (m,n,y,x) by Th19; ::_thesis: verum
end;
hence  X is BCK-algebra of n,j,m,n by Def3; ::_thesis: verum
end;

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 )
proof
let i, j, m, n be Element of NAT ; ::_thesis: ( 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 )
A1: ( min (m,n) = m or min (m,n) = n ) by XXREAL_0:15;
 ( min (i,j) = i or min (i,j) = j ) by XXREAL_0:15;
hence  ( 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 ) by A1, XXREAL_0:15; ::_thesis: verum
end;

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 )
proof
let i, j, m, n be Element of NAT ; ::_thesis: ( 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 )
A1: ( max (m,n) = m or max (m,n) = n ) by XXREAL_0:16;
 ( max (i,j) = i or max (i,j) = j ) by XXREAL_0:16;
hence  ( 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 ) by A1, XXREAL_0:16; ::_thesis: verum
end;

theorem Th25: :: BCIALG_5:25
for i, j, m, n being Element of NAT st i = min (i,j,m,n) holds
( i <= j & i <= m & i <= n )
proof
let i, j, m, n be Element of NAT ; ::_thesis: ( i = min (i,j,m,n) implies ( i <= j & i <= m & i <= n ) )
A1: min (m,n) <= n by XXREAL_0:17;
assume  i = min (i,j,m,n) ; ::_thesis: ( i <= j & i <= m & i <= n )
then A2: ( i <= min (i,j) & i <= min (m,n) ) by XXREAL_0:17;
 ( min (i,j) <= j & min (m,n) <= m ) by XXREAL_0:17;
hence  ( i <= j & i <= m & i <= n ) by A2, A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th26: :: BCIALG_5:26
for i, j, m, n being Element of NAT holds
( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n )
proof
let i, j, m, n be Element of NAT ; ::_thesis: ( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n )
A1: ( max (m,n) >= m & max (m,n) >= n ) by XXREAL_0:25;
A2: ( max (i,j,m,n) >= max (i,j) & max (i,j,m,n) >= max (m,n) ) by XXREAL_0:25;
 ( max (i,j) >= i & max (i,j) >= j ) by XXREAL_0:25;
hence  ( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n ) by A1, A2, XXREAL_0:2; ::_thesis: verum
end;

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) & i = j holds
X is BCK-algebra of i,i,i,i
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = j holds
X is BCK-algebra of i,i,i,i
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = min (i,j,m,n) & i = j implies X is BCK-algebra of i,i,i,i )
assume A1: i = min (i,j,m,n) ; ::_thesis: ( not i = j or X is BCK-algebra of i,i,i,i )
assume A2: i = j ; ::_thesis: X is BCK-algebra of i,i,i,i
A3: for x, y being Element of X holds Polynom (i,i,x,y) <= Polynom (i,i,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (i,i,x,y) <= Polynom (i,i,y,x)
 i <= n by A1, Th25;
then A4: (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power i by Th5;
 i <= m by A1, Th25;
then  i + 1 <= m + 1 by XREAL_1:6;
then A5: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19;
 Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
hence  Polynom (i,i,x,y) <= Polynom (i,i,y,x) by A2, A5, A4, Th1; ::_thesis: verum
end;
 for x, y being Element of X holds Polynom (i,i,y,x) = Polynom (i,i,x,y)
proof
let x, y be Element of X; ::_thesis: Polynom (i,i,y,x) = Polynom (i,i,x,y)
 Polynom (i,i,x,y) <= Polynom (i,i,y,x) by A3;
then A6: (Polynom (i,i,x,y)) \ (Polynom (i,i,y,x)) = 0. X by BCIALG_1:def_11;
 Polynom (i,i,y,x) <= Polynom (i,i,x,y) by A3;
then  (Polynom (i,i,y,x)) \ (Polynom (i,i,x,y)) = 0. X by BCIALG_1:def_11;
hence  Polynom (i,i,y,x) = Polynom (i,i,x,y) by A6, BCIALG_1:def_7; ::_thesis: verum
end;
hence  X is BCK-algebra of i,i,i,i by Def3; ::_thesis: verum
end;

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) & i < j & i < n holds
X is BCK-algebra of i,i + 1,i,i + 1
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i < j & i < n holds
X is BCK-algebra of i,i + 1,i,i + 1
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = min (i,j,m,n) & i < j & i < n implies X is BCK-algebra of i,i + 1,i,i + 1 )
assume A1: i = min (i,j,m,n) ; ::_thesis: ( not i < j or not i < n or X is BCK-algebra of i,i + 1,i,i + 1 )
assume that
A2: i < j and
A3: i < n ; ::_thesis: X is BCK-algebra of i,i + 1,i,i + 1
 for x, y being Element of X holds Polynom (i,(i + 1),x,y) = Polynom (i,(i + 1),y,x)
proof
 ( n - i is Element of NAT & n - i > i - i ) by A3, NAT_1:21, XREAL_1:9;
then  n - i >= 1 by NAT_1:14;
then A4: (n - i) + i >= 1 + i by XREAL_1:6;
 m >= i by A1, Th25;
then A5: m + 1 >= i + 1 by XREAL_1:6;
 ( j - i is Element of NAT & j - i > i - i ) by A2, NAT_1:21, XREAL_1:9;
then  j - i >= 1 by NAT_1:14;
then A6: (j - i) + i >= 1 + i by XREAL_1:6;
let x, y be Element of X; ::_thesis: Polynom (i,(i + 1),x,y) = Polynom (i,(i + 1),y,x)
A7: i + 1 < n + 1 by A3, XREAL_1:6;
 (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (n + 1) by Th19;
then A8: (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (m + 1) by A7, A5, Th6;
A9: ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power (n + 1) ) by Def3, Th19;
 (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (i + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (n + 1) by Th19;
then  (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (i + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j by A7, A6, Th6;
hence  Polynom (i,(i + 1),x,y) = Polynom (i,(i + 1),y,x) by A7, A8, A9, A4, Th6; ::_thesis: verum
end;
hence  X is BCK-algebra of i,i + 1,i,i + 1 by Def3; ::_thesis: verum
end;

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) & i = n & i = m holds
X is BCK-algebra of i,i,i,i
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = n & i = m holds
X is BCK-algebra of i,i,i,i
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = min (i,j,m,n) & i = n & i = m implies X is BCK-algebra of i,i,i,i )
assume A1: i = min (i,j,m,n) ; ::_thesis: ( not i = n or not i = m or X is BCK-algebra of i,i,i,i )
assume A2: ( i = n & i = m ) ; ::_thesis: X is BCK-algebra of i,i,i,i
then  for x, y being Element of X holds Polynom (i,i,x,y) = Polynom (i,j,y,x) by Def3;
then A3: X is BCK-algebra of i,i,i,j by Def3;
 i = min (i,i,i,j) by A1, A2;
hence  X is BCK-algebra of i,i,i,i by A3, Th27; ::_thesis: verum
end;

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 & m < j holds
X is BCK-algebra of i,m + 1,m,i
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = n & m < j implies X is BCK-algebra of i,m + 1,m,i )
assume that
A1: i = n and
A2: m < j ; ::_thesis: X is BCK-algebra of i,m + 1,m,i
 for x, y being Element of X holds Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x)
proof
 ( j - m is Element of NAT & j - m > m - m ) by A2, NAT_1:21, XREAL_1:9;
then  j - m >= 1 by NAT_1:14;
then A3: (j - m) + m >= 1 + m by XREAL_1:6;
let x, y be Element of X; ::_thesis: Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x)
A4: m + 1 < j + 1 by A2, XREAL_1:6;
 ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (m + 1) ) by Def3, Th20;
hence  Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x) by A1, A4, A3, Th6; ::_thesis: verum
end;
hence  X is BCK-algebra of i,m + 1,m,i by Def3; ::_thesis: verum
end;

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
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = n holds
X is BCK-algebra of i,j,j,i
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = n implies X is BCK-algebra of i,j,j,i )
assume  i = n ; ::_thesis: X is BCK-algebra of i,j,j,i
then reconsider X = X as BCK-algebra of i,j,m,i ;
 for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (j,i,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) = Polynom (j,i,y,x)
 Polynom (i,j,x,y) = Polynom (m,i,y,x) by Def3;
hence  Polynom (i,j,x,y) = Polynom (j,i,y,x) by Th20; ::_thesis: verum
end;
hence  X is BCK-algebra of i,j,j,i by Def3; ::_thesis: verum
end;

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 & k >= n holds
X is BCK-algebra of k,l,l,k
proof
let i, j, m, n, l, k be Element of NAT ; ::_thesis: 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
let X be BCK-algebra of i,j,m,n; ::_thesis: ( l >= j & k >= n implies X is BCK-algebra of k,l,l,k )
assume that
A1: l >= j and
A2: k >= n ; ::_thesis: X is BCK-algebra of k,l,l,k
 l - j is Element of NAT by A1, NAT_1:21;
then consider t being Element of NAT  such that
A3: t = l - j ;
 k - n is Element of NAT by A2, NAT_1:21;
then consider t1 being Element of NAT  such that
A4: t1 = k - n ;
 X is BCK-algebra of n,j,m,n by Th22;
then  X is BCK-algebra of n,j,j,n by Th21;
then  X is BCK-algebra of n + t1,j,j,n + t1 by Th17;
then  X is BCK-algebra of k,j + t,j + t,k by A4, Th18;
hence  X is BCK-algebra of k,l,l,k by A3; ::_thesis: verum
end;

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
proof
let i, j, m, n, k be Element of NAT ; ::_thesis: 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
let X be BCK-algebra of i,j,m,n; ::_thesis: ( k >= max (i,j,m,n) implies X is BCK-algebra of k,k,k,k )
assume A1: k >= max (i,j,m,n) ; ::_thesis: X is BCK-algebra of k,k,k,k
 max (i,j,m,n) >= n by Th26;
then  k - n is Element of NAT by A1, NAT_1:21, XXREAL_0:2;
then consider t1 being Element of NAT  such that
A2: t1 = k - n ;
 max (i,j,m,n) >= j by Th26;
then  k - j is Element of NAT by A1, NAT_1:21, XXREAL_0:2;
then consider t being Element of NAT  such that
A3: t = k - j ;
 X is BCK-algebra of n,j,m,n by Th22;
then  X is BCK-algebra of n,j,j,n by Th21;
then  X is BCK-algebra of n + t1,j,j,n + t1 by Th17;
then  X is BCK-algebra of k,j + t,j + t,k by A2, Th18;
hence  X is BCK-algebra of k,k,k,k by A3; ::_thesis: verum
end;

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 & j <= n holds
X is BCK-algebra of i,j,i,j
proof
let i, j, m, n be Element of NAT ; ::_thesis: 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
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i <= m & j <= n implies X is BCK-algebra of i,j,i,j )
assume that
A1: i <= m and
A2: j <= n ; ::_thesis: X is BCK-algebra of i,j,i,j
A3: for x, y being Element of X holds Polynom (i,j,x,y) <= Polynom (i,j,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) <= Polynom (i,j,y,x)
 i + 1 <= m + 1 by A1, XREAL_1:6;
then A4: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19;
 ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power j ) by A2, Def3, Th5;
hence  Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A4, Th1; ::_thesis: verum
end;
 for x, y being Element of X holds Polynom (i,j,y,x) = Polynom (i,j,x,y)
proof
let x, y be Element of X; ::_thesis: Polynom (i,j,y,x) = Polynom (i,j,x,y)
 Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A3;
then A5: (Polynom (i,j,x,y)) \ (Polynom (i,j,y,x)) = 0. X by BCIALG_1:def_11;
 Polynom (i,j,y,x) <= Polynom (i,j,x,y) by A3;
then  (Polynom (i,j,y,x)) \ (Polynom (i,j,x,y)) = 0. X by BCIALG_1:def_11;
hence  Polynom (i,j,y,x) = Polynom (i,j,x,y) by A5, BCIALG_1:def_7; ::_thesis: verum
end;
hence  X is BCK-algebra of i,j,i,j by Def3; ::_thesis: verum
end;

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 & i < n holds
X is BCK-algebra of i,j,i,i + 1
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i <= m & i < n holds
X is BCK-algebra of i,j,i,i + 1
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i <= m & i < n implies X is BCK-algebra of i,j,i,i + 1 )
assume that
A1: i <= m and
A2: i < n ; ::_thesis: X is BCK-algebra of i,j,i,i + 1
 for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (i,(i + 1),y,x)
proof
 ( n - i is Element of NAT & n - i > i - i ) by A2, NAT_1:21, XREAL_1:9;
then  n - i >= 1 by NAT_1:14;
then A3: (n - i) + i >= 1 + i by XREAL_1:6;
let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) = Polynom (i,(i + 1),y,x)
A4: i + 1 < n + 1 by A2, XREAL_1:6;
A5: ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + 1) ) by Def3, Th19;
 ( (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (n + 1) & m + 1 >= i + 1 ) by A1, Th19, XREAL_1:6;
then  (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (m + 1) by A4, Th6;
hence  Polynom (i,j,x,y) = Polynom (i,(i + 1),y,x) by A4, A5, A3, Th6; ::_thesis: verum
end;
hence  X is BCK-algebra of i,j,i,i + 1 by Def3; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: 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
let i, j, k be Element of NAT ; ::_thesis: ( X is BCI-algebra of i,j,j + k,i + k implies X is BCK-algebra )
assume A1: X is BCI-algebra of i,j,j + k,i + k ; ::_thesis: X is BCK-algebra
 for y being Element of X holds (0. X) \ y = 0. X
proof
let y be Element of X; ::_thesis: (0. X) \ y = 0. X
A2: (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) = ((((y,y) to_power (j + k)) \ y),((0. X) \ y)) to_power (i + k) by BCIALG_2:4
.= ((((y \ y),y) to_power (j + k)),((0. X) \ y)) to_power (i + k) by BCIALG_2:7
.= ((((0. X),y) to_power (j + k)),((0. X) \ y)) to_power (i + k) by BCIALG_1:def_5
.= ((((0. X),((0. X) \ y)) to_power (i + k)),y) to_power (j + k) by BCIALG_2:11
.= (((((0. X),(0. X)) to_power (i + k)) \ (((0. X),y) to_power (i + k))),y) to_power (j + k) by BCIALG_2:18
.= (((0. X) \ (((0. X),y) to_power (i + k))),y) to_power (j + k) by BCIALG_2:6
.= (((0. X),y) to_power (j + k)) \ (((0. X),y) to_power (i + k)) by BCIALG_2:7
.= (((((0. X),y) to_power j),y) to_power k) \ (((0. X),y) to_power (i + k)) by BCIALG_2:10
.= (((((0. X),y) to_power j),y) to_power k) \ (((((0. X),y) to_power i),y) to_power k) by BCIALG_2:10 ;
A3: (((((0. X),y) to_power j),y) to_power k) \ (((((0. X),y) to_power i),y) to_power k) <= (((0. X),y) to_power j) \ (((0. X),y) to_power i) by BCIALG_2:21;
 Polynom (i,j,(0. X),y) = Polynom ((j + k),(i + k),y,(0. X)) by A1, Def3;
then  ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j = (((y,(y \ (0. X))) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_1:2;
then  ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j = (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_1:2;
then A4: ((((0. X),y) to_power j),((0. X) \ y)) to_power (i + 1) = (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_2:11;
((((0. X),y) to_power j),((0. X) \ y)) to_power (i + 1) = ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j by BCIALG_2:11
.= (((((0. X),(0. X)) to_power (i + 1)) \ (((0. X),y) to_power (i + 1))),y) to_power j by BCIALG_2:18
.= (((0. X) \ (((0. X),y) to_power (i + 1))),y) to_power j by BCIALG_2:6
.= (((0. X),y) to_power j) \ (((0. X),y) to_power (i + 1)) by BCIALG_2:7 ;
then  ((((0. X),y) to_power j) \ (((0. X),y) to_power (i + 1))) \ ((((0. X),y) to_power j) \ (((0. X),y) to_power i)) = 0. X by A4, A2, A3, BCIALG_1:def_11;
then  (0. X) \ ((((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1))) = 0. X by BCIALG_1:11;
then A5: 0. X <= (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) by BCIALG_1:def_11;
(((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) = (((0. X),y) to_power i) \ ((((0. X),y) to_power i) \ y) by BCIALG_2:4
.= (((0. X),y) to_power i) \ ((((0. X) \ y),y) to_power i) by BCIALG_2:7 ;
then  (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) <= (0. X) \ ((0. X) \ y) by BCIALG_2:21;
then  0. X <= (0. X) \ ((0. X) \ y) by A5, Th1;
then  (0. X) \ ((0. X) \ ((0. X) \ y)) = 0. X by BCIALG_1:def_11;
hence  (0. X) \ y = 0. X by BCIALG_1:8; ::_thesis: verum
end;
then  for x being Element of X holds x ` = 0. X ;
hence  X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum
end;

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 )
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 )
thus  ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 ) ::_thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )
proof
assume A1: X is BCI-algebra of 0 , 0 , 0 , 0 ; ::_thesis: X is BCK-algebra of 0 , 0 , 0 , 0
then  X is BCI-algebra of 0 , 0 ,0 + 0,0 + 0 ;
then reconsider X = X as BCK-algebra by Th36;
 for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by A1, Def3;
hence  X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum
end;
thus  ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 ) ; ::_thesis: verum
end;

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 )
proof
let X be BCI-algebra; ::_thesis: ( X is commutative BCK-algebra iff X is BCI-algebra of 0 , 0 , 0 , 0 )
thus  ( X is commutative BCK-algebra implies X is BCI-algebra of 0 , 0 , 0 , 0 ) ::_thesis: ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is commutative BCK-algebra )
proof
assume A1: X is commutative BCK-algebra ; ::_thesis: X is BCI-algebra of 0 , 0 , 0 , 0
 for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) = Polynom (0,0,y,x)
A2: x \ (x \ y) = y \ (y \ x) by A1, BCIALG_3:def_1;
(((x,(x \ y)) to_power 1),(y \ x)) to_power 0 = (x,(x \ y)) to_power 1 by BCIALG_2:1
.= y \ (y \ x) by A2, BCIALG_2:2
.= (y,(y \ x)) to_power 1 by BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence  Polynom (0,0,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum
end;
assume A3: X is BCI-algebra of 0 , 0 , 0 , 0 ; ::_thesis: X is commutative BCK-algebra
 for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x)
A4: Polynom (0,0,x,y) = Polynom (0,0,y,x) by A3, Def3;
x \ (x \ y) = (x,(x \ y)) to_power 1 by BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by A4, BCIALG_2:1
.= (y,(y \ x)) to_power 1 by BCIALG_2:1
.= y \ (y \ x) by BCIALG_2:2 ;
hence  x \ (x \ y) = y \ (y \ x) ; ::_thesis: verum
end;
hence  X is commutative BCK-algebra by A3, Th37, BCIALG_3:def_1; ::_thesis: verum
end;

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 & P = p-Semisimple-part X holds
B /\ P = {(0. X)}
proof
let X be BCI-algebra; ::_thesis: for B, P being non empty Subset of X
for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds
B /\ P = {(0. X)}
let B, P be non empty Subset of X; ::_thesis: for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds
B /\ P = {(0. X)}
let X be BCI-algebra; ::_thesis: ( B = BCK-part X & P = p-Semisimple-part X implies B /\ P = {(0. X)} )
assume that
A1: B = BCK-part X and
A2: P = p-Semisimple-part X ; ::_thesis: B /\ P = {(0. X)}
thus  B /\ P c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= B /\ P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B /\ P or x in {(0. X)} )
assume A3: x in B /\ P ; ::_thesis: x in {(0. X)}
then A4: x in P by XBOOLE_0:def_4;
A5: x in B by A3, XBOOLE_0:def_4;
then A6: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) by A1;
reconsider x = x as Element of X by A1, A5;
A7: (0. X) \ x = 0. X by A6, BCIALG_1:def_11;
 ex x2 being Element of X st
( x = x2 & x2 is minimal ) by A2, A4;
then  x = 0. X by A7, BCIALG_1:def_14;
hence  x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
 ( 0. X in BCK-part X & 0. X in p-Semisimple-part X ) by BCIALG_1:19;
then  0. X in B /\ P by A1, A2, XBOOLE_0:def_4;
then  for x being set st x in {(0. X)} holds
x in B /\ P by TARSKI:def_1;
hence  {(0. X)} c= B /\ P by TARSKI:def_3; ::_thesis: verum
end;

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)} )
proof
let X be BCI-algebra; ::_thesis: 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)} )
let P be non empty Subset of X; ::_thesis: for X being BCI-algebra st P = p-Semisimple-part X holds
( X is BCK-algebra iff P = {(0. X)} )
let X be BCI-algebra; ::_thesis: ( P = p-Semisimple-part X implies ( X is BCK-algebra iff P = {(0. X)} ) )
assume A1: P = p-Semisimple-part X ; ::_thesis: ( X is BCK-algebra iff P = {(0. X)} )
thus  ( X is BCK-algebra implies P = {(0. X)} ) ::_thesis: ( P = {(0. X)} implies X is BCK-algebra )
proof
assume A2: X is BCK-algebra ; ::_thesis: P = {(0. X)}
thus  P c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in {(0. X)} )
assume A3: x in P ; ::_thesis: x in {(0. X)}
then A4: ex x1 being Element of X st
( x = x1 & x1 is minimal ) by A1;
reconsider x = x as Element of X by A1, A3;
(0. X) \ x = x `
.= 0. X by A2, BCIALG_1:def_8 ;
then  x = 0. X by A4, BCIALG_1:def_14;
hence  x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
 0. X in P by A1;
then  for x being set st x in {(0. X)} holds
x in P by TARSKI:def_1;
hence  {(0. X)} c= P by TARSKI:def_3; ::_thesis: verum
end;
assume A5: P = {(0. X)} ; ::_thesis: X is BCK-algebra
 for x being Element of X holds (0. X) \ x = 0. X
proof
let x be Element of X; ::_thesis: (0. X) \ x = 0. X
 0. X in P by A5, TARSKI:def_1;
then  (0. X) \ x in P by A1, BCIALG_1:33;
hence  (0. X) \ x = 0. X by A5, TARSKI:def_1; ::_thesis: verum
end;
then  for x being Element of X holds x ` = 0. X ;
hence  X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum
end;

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)} )
proof
let X be BCI-algebra; ::_thesis: 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)} )
let B be non empty Subset of X; ::_thesis: for X being BCI-algebra st B = BCK-part X holds
( X is p-Semisimple BCI-algebra iff B = {(0. X)} )
let X be BCI-algebra; ::_thesis: ( B = BCK-part X implies ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) )
assume A1: B = BCK-part X ; ::_thesis: ( X is p-Semisimple BCI-algebra iff B = {(0. X)} )
thus  ( X is p-Semisimple BCI-algebra implies B = {(0. X)} ) ::_thesis: ( B = {(0. X)} implies X is p-Semisimple BCI-algebra )
proof
assume A2: X is p-Semisimple BCI-algebra ; ::_thesis: B = {(0. X)}
thus  B c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in {(0. X)} )
assume A3: x in B ; ::_thesis: x in {(0. X)}
then A4: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) by A1;
reconsider x = x as Element of X by A1, A3;
 (x `) ` = x by A2, BCIALG_1:def_26;
then  (0. X) ` = x by A4, BCIALG_1:def_11;
then  x = 0. X by BCIALG_1:def_5;
hence  x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in B )
assume A5: x in {(0. X)} ; ::_thesis: x in B
then reconsider x = x as Element of X by TARSKI:def_1;
 x = 0. X by A5, TARSKI:def_1;
then  x ` = 0. X by BCIALG_1:def_5;
then  0. X <= x by BCIALG_1:def_11;
hence  x in B by A1; ::_thesis: verum
end;
assume A6: B = {(0. X)} ; ::_thesis: X is p-Semisimple BCI-algebra
 for x being Element of X holds (x `) ` = x
proof
let x be Element of X; ::_thesis: (x `) ` = x
(0. X) \ (x \ ((0. X) \ ((0. X) \ x))) = ((0. X),(x \ ((0. X) \ ((0. X) \ x)))) to_power 1 by BCIALG_2:2
.= (((0. X),x) to_power 1) \ (((0. X),((0. X) \ ((0. X) \ x))) to_power 1) by BCIALG_2:18
.= (((0. X),x) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:8
.= 0. X by BCIALG_1:def_5 ;
then  0. X <= x \ ((0. X) \ ((0. X) \ x)) by BCIALG_1:def_11;
then  x \ ((0. X) \ ((0. X) \ x)) in B by A1;
then A7: x \ ((0. X) \ ((0. X) \ x)) = 0. X by A6, TARSKI:def_1;
((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
hence  (x `) ` = x by A7, BCIALG_1:def_7; ::_thesis: verum
end;
hence  X is p-Semisimple BCI-algebra by BCIALG_1:54; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 )
assume A1: X is p-Semisimple BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1, 0 , 0
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x)
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2
.= (y,(y \ x)) to_power 1 by A1, BCIALG_1:def_26
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence  Polynom (0,1,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of 0 ,1, 0 , 0 by Def3; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: 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
let n, j, m be Element of NAT ; ::_thesis: ( X is p-Semisimple BCI-algebra implies X is BCI-algebra of n + j,n,m,(m + j) + 1 )
assume A1: X is p-Semisimple BCI-algebra ; ::_thesis: X is BCI-algebra of n + j,n,m,(m + j) + 1
A2: for x, y being Element of X holds Polynom (n,n,x,y) = y
proof
let x, y be Element of X; ::_thesis: Polynom (n,n,x,y) = y
defpred S1[ Element of NAT ] means ( $1 <= n implies Polynom ($1,$1,x,y) = y );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_Polynom_(k,k,x,y)_=_y_)_&_k_+_1_<=_n_holds_
Polynom_((k_+_1),(k_+_1),x,y)_=_y
let k be Element of NAT ; ::_thesis: ( ( k <= n implies Polynom (k,k,x,y) = y ) & k + 1 <= n implies Polynom ((k + 1),(k + 1),x,y) = y )
assume A3: ( k <= n implies Polynom (k,k,x,y) = y ) ; ::_thesis: ( k + 1 <= n implies Polynom ((k + 1),(k + 1),x,y) = y )
set m = k + 1;
A4: Polynom ((k + 1),(k + 1),x,y) = (Polynom (k,(k + 1),x,y)) \ (x \ y) by Th9
.= ((Polynom (k,k,x,y)) \ (y \ x)) \ (x \ y) by Th10 ;
assume  k + 1 <= n ; ::_thesis: Polynom ((k + 1),(k + 1),x,y) = y
then  Polynom ((k + 1),(k + 1),x,y) = x \ (x \ y) by A1, A3, A4, BCIALG_1:def_26, NAT_1:13;
hence  Polynom ((k + 1),(k + 1),x,y) = y by A1, BCIALG_1:def_26; ::_thesis: verum
end;
then A5: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
Polynom (0,0,x,y) = x \ (x \ y) by Th7
.= y by A1, BCIALG_1:def_26 ;
then A6: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5);
hence  Polynom (n,n,x,y) = y ; ::_thesis: verum
end;
A7: for x, y being Element of X holds Polynom (m,(m + 1),x,y) = x
proof
let x, y be Element of X; ::_thesis: Polynom (m,(m + 1),x,y) = x
defpred S1[ Element of NAT ] means ( $1 <= m implies Polynom ($1,($1 + 1),x,y) = x );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_m_implies_Polynom_(k,(k_+_1),x,y)_=_x_)_&_k_+_1_<=_m_holds_
Polynom_((k_+_1),((k_+_1)_+_1),x,y)_=_x
let k be Element of NAT ; ::_thesis: ( ( k <= m implies Polynom (k,(k + 1),x,y) = x ) & k + 1 <= m implies Polynom ((k + 1),((k + 1) + 1),x,y) = x )
assume A8: ( k <= m implies Polynom (k,(k + 1),x,y) = x ) ; ::_thesis: ( k + 1 <= m implies Polynom ((k + 1),((k + 1) + 1),x,y) = x )
set l = k + 1;
A9: Polynom ((k + 1),((k + 1) + 1),x,y) = (Polynom (k,((k + 1) + 1),x,y)) \ (x \ y) by Th9
.= ((Polynom (k,(k + 1),x,y)) \ (y \ x)) \ (x \ y) by Th10 ;
assume  k + 1 <= m ; ::_thesis: Polynom ((k + 1),((k + 1) + 1),x,y) = x
then  Polynom ((k + 1),((k + 1) + 1),x,y) = (x \ (x \ y)) \ (y \ x) by A8, A9, BCIALG_1:7, NAT_1:13
.= y \ (y \ x) by A1, BCIALG_1:def_26 ;
hence  Polynom ((k + 1),((k + 1) + 1),x,y) = x by A1, BCIALG_1:def_26; ::_thesis: verum
end;
then A10: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
Polynom (0,1,x,y) = (Polynom (0,0,x,y)) \ (y \ x) by Th10
.= (x \ (x \ y)) \ (y \ x) by Th7
.= y \ (y \ x) by A1, BCIALG_1:def_26
.= x by A1, BCIALG_1:def_26 ;
then A11: S1[ 0 ] ;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A10);
hence  Polynom (m,(m + 1),x,y) = x ; ::_thesis: verum
end;
 for x, y being Element of X holds Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x)
proof
let x, y be Element of X; ::_thesis: Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x)
defpred S1[ Element of NAT ] means ( $1 <= j implies Polynom ((n + $1),n,x,y) = Polynom (m,((m + $1) + 1),y,x) );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_j_implies_Polynom_((n_+_k),n,x,y)_=_Polynom_(m,((m_+_k)_+_1),y,x)_)_&_k_+_1_<=_j_holds_
Polynom_((n_+_(k_+_1)),n,x,y)_=_Polynom_(m,((m_+_(k_+_1))_+_1),y,x)
let k be Element of NAT ; ::_thesis: ( ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) & k + 1 <= j implies Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) )
assume A12: ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) ; ::_thesis: ( k + 1 <= j implies Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) )
set l = k + 1;
assume  k + 1 <= j ; ::_thesis: Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x)
then  Polynom ((n + (k + 1)),n,x,y) = (Polynom (m,((m + k) + 1),y,x)) \ (x \ y) by A12, Th9, NAT_1:13
.= Polynom (m,(((m + k) + 1) + 1),y,x) by Th10 ;
hence  Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) ; ::_thesis: verum
end;
then A13: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
Polynom ((n + 0),n,x,y) = y by A2
.= Polynom (m,((m + 0) + 1),y,x) by A7 ;
then A14: S1[ 0 ] ;
 for j being Element of NAT holds S1[j] from NAT_1:sch_1(A14, A13);
hence  Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of n + j,n,m,(m + j) + 1 by Def3; ::_thesis: verum
end;

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 & X is BCI-algebra of 1, 0 , 0 , 0 )
proof
let X be BCI-algebra; ::_thesis: ( X is associative BCI-algebra implies ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) )
assume A1: X is associative BCI-algebra ; ::_thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )
 for x being Element of X holds (x `) ` = x
proof
let x be Element of X; ::_thesis: (x `) ` = x
 x ` = x by A1, BCIALG_1:47;
hence  (x `) ` = x ; ::_thesis: verum
end;
then A2: X is p-Semisimple by BCIALG_1:54;
 for x, y being Element of X holds Polynom (1,0,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (1,0,x,y) = Polynom (0,0,y,x)
 x \ (x \ y) = y by A2, BCIALG_1:def_26;
then A3: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_1:48;
(((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 = (x,(x \ y)) to_power 2 by BCIALG_2:1
.= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3
.= (y,(y \ x)) to_power 1 by A3, BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence  Polynom (1,0,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum
end;
hence  ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) by A2, Def3, Th42; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: ( X is weakly-positive-implicative BCI-algebra implies X is BCI-algebra of 0 ,1,1,1 )
assume A1: X is weakly-positive-implicative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1,1,1
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (1,1,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (1,1,y,x)
A2: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A1, BCIALG_1:85;
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2
.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2
.= (((y \ (y \ x)) \ (y \ x)),(x \ y)) to_power 1 by A2, BCIALG_2:2
.= (((y,(y \ x)) to_power 2),(x \ y)) to_power 1 by BCIALG_2:3 ;
hence  Polynom (0,1,x,y) = Polynom (1,1,y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of 0 ,1,1,1 by Def3; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: ( X is positive-implicative BCI-algebra implies X is BCI-algebra of 0 ,1,1,1 )
assume A1: X is positive-implicative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1,1,1
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (1,1,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (1,1,y,x)
A2: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A1, BCIALG_1:85;
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2
.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2
.= (((y \ (y \ x)) \ (y \ x)),(x \ y)) to_power 1 by A2, BCIALG_2:2
.= (((y,(y \ x)) to_power 2),(x \ y)) to_power 1 by BCIALG_2:3 ;
hence  Polynom (0,1,x,y) = Polynom (1,1,y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of 0 ,1,1,1 by Def3; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: ( X is implicative BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 )
assume A1: X is implicative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1, 0 , 0
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x)
A2: (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by A1, BCIALG_1:def_24;
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2
.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2
.= (y,(y \ x)) to_power 1 by A2, BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence  Polynom (0,1,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of 0 ,1, 0 , 0 by Def3; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: ( X is alternative BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 )
assume A1: X is alternative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1, 0 , 0
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x)
A2: (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by A1, BCIALG_1:76;
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2
.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2
.= (y,(y \ x)) to_power 1 by A2, BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence  Polynom (0,1,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum
end;
hence  X is BCI-algebra of 0 ,1, 0 , 0 by Def3; ::_thesis: verum
end;

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 )
proof
let X be BCI-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0 ,1, 0 ,1 )
thus  ( X is BCK-positive-implicative BCK-algebra implies X is BCK-algebra of 0 ,1, 0 ,1 ) ::_thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x)
 (x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5;
then  (x \ (x \ y)) \ y = 0. X by BCIALG_1:7;
then A2: x \ (x \ y) <= y by BCIALG_1:def_11;
 x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A1, BCIALG_3:28;
then  x \ (x \ y) <= y \ (x \ y) by A2, BCIALG_1:5;
then  (x \ (x \ y)) \ (y \ x) <= (y \ (x \ y)) \ (y \ x) by BCIALG_1:5;
then A3: (x \ (x \ y)) \ (y \ x) <= (y \ (y \ x)) \ (x \ y) by BCIALG_1:7;
 (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5;
then  (y \ (y \ x)) \ x = 0. X by BCIALG_1:7;
then  y \ (y \ x) <= x by BCIALG_1:def_11;
then A4: (y \ (y \ x)) \ (y \ x) <= x \ (y \ x) by BCIALG_1:5;
 y \ (y \ x) = (y \ (y \ x)) \ (y \ x) by A1, BCIALG_3:28;
then  (y \ (y \ x)) \ (x \ y) <= (x \ (y \ x)) \ (x \ y) by A4, BCIALG_1:5;
then  (y \ (y \ x)) \ (x \ y) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:7;
then A5: (x \ (x \ y)) \ (y \ x) = (y \ (y \ x)) \ (x \ y) by A3, Th2;
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2
.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2
.= ((y \ (y \ x)),(x \ y)) to_power 1 by A5, BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 1 by BCIALG_2:2 ;
hence  Polynom (0,1,x,y) = Polynom (0,1,y,x) ; ::_thesis: verum
end;
hence  X is BCK-algebra of 0 ,1, 0 ,1 by A1, Def3; ::_thesis: verum
end;
assume A6: X is BCK-algebra of 0 ,1, 0 ,1 ; ::_thesis: X is BCK-positive-implicative BCK-algebra
 for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
A7: Polynom (0,1,x,(x \ y)) = Polynom (0,1,(x \ y),x) by A6, Def3;
A8: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by A6, BCIALG_1:def_8 ;
then A9: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
A10: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8
.= x \ y by A8, BCIALG_1:2 ;
(x \ (x \ (x \ y))) \ ((x \ y) \ x) = ((x,(x \ (x \ y))) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2
.= ((((x \ y),((x \ y) \ x)) to_power 1),(x \ (x \ y))) to_power 1 by A7, BCIALG_2:2
.= (((x \ y) \ ((x \ y) \ x)),(x \ (x \ y))) to_power 1 by BCIALG_2:2
.= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ;
hence  x \ y = (x \ y) \ y by A10, A9; ::_thesis: verum
end;
hence  X is BCK-positive-implicative BCK-algebra by A6, BCIALG_3:28; ::_thesis: verum
end;

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 )
proof
let X be BCI-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 )
thus  ( X is BCK-implicative BCK-algebra implies X is BCK-algebra of 1, 0 , 0 , 0 ) ::_thesis: ( X is BCK-algebra of 1, 0 , 0 , 0 implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: X is BCK-algebra of 1, 0 , 0 , 0
 for x, y being Element of X holds Polynom (1,0,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (1,0,x,y) = Polynom (0,0,y,x)
A2: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_3:35;
(((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 = (x,(x \ y)) to_power 2 by BCIALG_2:1
.= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3
.= (y,(y \ x)) to_power 1 by A2, BCIALG_2:2
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence  Polynom (1,0,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum
end;
hence  X is BCK-algebra of 1, 0 , 0 , 0 by A1, Def3; ::_thesis: verum
end;
assume A3: X is BCK-algebra of 1, 0 , 0 , 0 ; ::_thesis: X is BCK-implicative BCK-algebra
 for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
A4: Polynom (1,0,x,y) = Polynom (0,0,y,x) by A3, Def3;
(x \ (x \ y)) \ (x \ y) = (x,(x \ y)) to_power 2 by BCIALG_2:3
.= (((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 by BCIALG_2:1
.= (y,(y \ x)) to_power 1 by A4, BCIALG_2:1
.= y \ (y \ x) by BCIALG_2:2 ;
hence  (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; ::_thesis: verum
end;
hence  X is BCK-implicative BCK-algebra by A3, BCIALG_3:35; ::_thesis: verum
end;

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 & X is BCK-algebra of 0 ,1, 0 ,1 ) )
proof
let X be BCI-algebra; ::_thesis: ( 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 ) )
thus  ( X is BCK-algebra of 1, 0 , 0 , 0 implies ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ) ::_thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-algebra of 1, 0 , 0 , 0 )
proof
assume  X is BCK-algebra of 1, 0 , 0 , 0 ; ::_thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 )
then  X is BCK-implicative BCK-algebra by Th50;
hence  ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) by Th38, Th49; ::_thesis: verum
end;
assume  ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ; ::_thesis: X is BCK-algebra of 1, 0 , 0 , 0
then  ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) by Th38, Th49;
then  X is BCK-implicative BCK-algebra by BCIALG_3:34;
hence  X is BCK-algebra of 1, 0 , 0 , 0 by Th50; ::_thesis: verum
end;

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 )
proof
let X be quasi-commutative BCK-algebra; ::_thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y )
thus  ( X is BCK-algebra of 0 ,1, 0 ,1 implies for x, y being Element of X holds x \ y = (x \ y) \ y ) ::_thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ y ) implies X is BCK-algebra of 0 ,1, 0 ,1 )
proof
assume A1: X is BCK-algebra of 0 ,1, 0 ,1 ; ::_thesis: for x, y being Element of X holds x \ y = (x \ y) \ y
 for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
A2: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then A3: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
A4: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8
.= x \ y by A2, BCIALG_1:2 ;
A5: Polynom (0,1,x,(x \ y)) = Polynom (0,1,(x \ y),x) by A1, Def3;
(x \ (x \ (x \ y))) \ ((x \ y) \ x) = ((x,(x \ (x \ y))) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2
.= ((((x \ y),((x \ y) \ x)) to_power 1),(x \ (x \ y))) to_power 1 by A5, BCIALG_2:2
.= (((x \ y) \ ((x \ y) \ x)),(x \ (x \ y))) to_power 1 by BCIALG_2:2
.= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ;
hence  x \ y = (x \ y) \ y by A4, A3; ::_thesis: verum
end;
hence  for x, y being Element of X holds x \ y = (x \ y) \ y ; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ y = (x \ y) \ y ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1
then  X is BCK-positive-implicative BCK-algebra by BCIALG_3:28;
hence  X is BCK-algebra of 0 ,1, 0 ,1 by Th49; ::_thesis: verum
end;

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) )
proof
let n be Element of NAT ; ::_thesis: 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) )
let X be quasi-commutative BCK-algebra; ::_thesis: ( 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) )
thus  ( X is BCK-algebra of n,n + 1,n,n + 1 implies for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) ::_thesis: ( ( for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) implies X is BCK-algebra of n,n + 1,n,n + 1 )
proof
assume A1: X is BCK-algebra of n,n + 1,n,n + 1 ; ::_thesis: for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2)
 for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2)
proof
let x, y be Element of X; ::_thesis: (x,y) to_power (n + 1) = (x,y) to_power (n + 2)
A2: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then A3: (((x,(x \ (x \ y))) to_power (n + 1)),((x \ y) \ x)) to_power (n + 1) = (((x,y) to_power (n + 1)),(0. X)) to_power (n + 1) by BCIALG_2:8
.= (x,y) to_power (n + 1) by BCIALG_2:5 ;
A4: ((((x \ y),((x \ y) \ x)) to_power (n + 1)),(x \ (x \ y))) to_power (n + 1) = ((x \ y),(x \ (x \ y))) to_power (n + 1) by A2, BCIALG_2:5
.= ((x,(x \ (x \ y))) to_power (n + 1)) \ y by BCIALG_2:7
.= ((x,y) to_power (n + 1)) \ y by BCIALG_2:8
.= (x,y) to_power ((n + 1) + 1) by BCIALG_2:4 ;
 Polynom (n,(n + 1),x,(x \ y)) = Polynom (n,(n + 1),(x \ y),x) by A1, Def3;
hence  (x,y) to_power (n + 1) = (x,y) to_power (n + 2) by A3, A4; ::_thesis: verum
end;
hence  for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ; ::_thesis: verum
end;
assume A5: for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ; ::_thesis: X is BCK-algebra of n,n + 1,n,n + 1
 for x, y being Element of X holds Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x)
 (x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5;
then  (x \ (x \ y)) \ y = 0. X by BCIALG_1:7;
then  x \ (x \ y) <= y by BCIALG_1:def_11;
then  ((x \ (x \ y)),(x \ y)) to_power (n + 1) <= (y,(x \ y)) to_power (n + 1) by BCIALG_2:19;
then  (((x,(x \ y)) to_power 1),(x \ y)) to_power (n + 1) <= (y,(x \ y)) to_power (n + 1) by BCIALG_2:2;
then A6: (x,(x \ y)) to_power (1 + (n + 1)) <= (y,(x \ y)) to_power (n + 1) by BCIALG_2:10;
 (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5;
then  (y \ (y \ x)) \ x = 0. X by BCIALG_1:7;
then  y \ (y \ x) <= x by BCIALG_1:def_11;
then  ((y \ (y \ x)),(y \ x)) to_power (n + 1) <= (x,(y \ x)) to_power (n + 1) by BCIALG_2:19;
then  (((y,(y \ x)) to_power 1),(y \ x)) to_power (n + 1) <= (x,(y \ x)) to_power (n + 1) by BCIALG_2:2;
then A7: (y,(y \ x)) to_power (1 + (n + 1)) <= (x,(y \ x)) to_power (n + 1) by BCIALG_2:10;
 (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (n + 2) by A5;
then  (((y,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) by A7, BCIALG_2:19;
then A8: (((y,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:11;
 (x,(x \ y)) to_power (n + 1) = (x,(x \ y)) to_power (n + 2) by A5;
then  (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by A6, BCIALG_2:19;
then  (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((y,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) by BCIALG_2:11;
hence  Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x) by A8, Th2; ::_thesis: verum
end;
hence  X is BCK-algebra of n,n + 1,n,n + 1 by Def3; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 implies X is BCI-commutative BCI-algebra )
assume A1: X is BCI-algebra of 0 ,1, 0 , 0 ; ::_thesis: X is BCI-commutative BCI-algebra
 for x, y being Element of X st y \ x = 0. X holds
y = x \ (x \ y)
proof
let x, y be Element of X; ::_thesis: ( y \ x = 0. X implies y = x \ (x \ y) )
 Polynom (0,1,x,y) = Polynom (0,0,y,x) by A1, Def3;
then  ((x,(x \ y)) to_power 1) \ (y \ x) = (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:2;
then  (x \ (x \ y)) \ (y \ x) = (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:2;
then A2: (x \ (x \ y)) \ (y \ x) = (y,(y \ x)) to_power 1 by BCIALG_2:1;
assume  y \ x = 0. X ; ::_thesis: y = x \ (x \ y)
then  (x \ (x \ y)) \ (0. X) = y \ (0. X) by A2, BCIALG_2:2;
then  y = (x \ (x \ y)) \ (0. X) by BCIALG_1:2;
hence  y = x \ (x \ y) by BCIALG_1:2; ::_thesis: verum
end;
then  for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x) ;
hence  X is BCI-commutative BCI-algebra by BCIALG_3:def_4; ::_thesis: verum
end;

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
proof
let X be BCI-algebra; ::_thesis: for n, m being Element of NAT st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra
let n, m be Element of NAT ; ::_thesis: ( X is BCI-algebra of n, 0 ,m,m implies X is BCI-commutative BCI-algebra )
A1: for x, y being Element of X st x \ y = 0. X holds
(y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 )
defpred S1[ Element of NAT ] means ( $1 <= m implies (y,(y \ x)) to_power ($1 + 1) <= (y,(y \ x)) to_power 1 );
assume A2: x \ y = 0. X ; ::_thesis: (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_m_implies_(y,(y_\_x))_to_power_(k_+_1)_<=_(y,(y_\_x))_to_power_1_)_&_k_+_1_<=_m_holds_
(y,(y_\_x))_to_power_((k_+_1)_+_1)_<=_(y,(y_\_x))_to_power_1
 ((0. X),(y \ x)) to_power 1 = (((0. X),y) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:18;
then  (0. X) \ (y \ x) = (((0. X),y) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:2;
then A3: (0. X) \ (y \ x) = ((0. X) \ y) \ (((0. X),x) to_power 1) by BCIALG_2:2;
let k be Element of NAT ; ::_thesis: ( ( k <= m implies (y,(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power 1 ) & k + 1 <= m implies (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 )
assume A4: ( k <= m implies (y,(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power 1 ) ; ::_thesis: ( k + 1 <= m implies (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 )
 (((0. X) \ y) \ ((0. X) \ x)) \ (x \ y) = 0. X by BCIALG_1:1;
then  ((0. X) \ y) \ ((0. X) \ x) = 0. X by A2, BCIALG_1:2;
then  (0. X) \ (y \ x) = 0. X by A3, BCIALG_2:2;
then  (y \ y) \ (y \ x) = 0. X by BCIALG_1:def_5;
then  (y \ (y \ x)) \ y = 0. X by BCIALG_1:7;
then  y \ (y \ x) <= y by BCIALG_1:def_11;
then  ((y \ (y \ x)),(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power (k + 1) by BCIALG_2:19;
then  (((y,(y \ x)) to_power 1),(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power (k + 1) by BCIALG_2:2;
then A5: (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power (k + 1) by BCIALG_2:10;
set m1 = k + 1;
assume  k + 1 <= m ; ::_thesis: (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1
hence  (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 by A4, A5, Th1, NAT_1:13; ::_thesis: verum
end;
then A6: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
 ((y,(y \ x)) to_power (0 + 1)) \ ((y,(y \ x)) to_power 1) = 0. X by BCIALG_1:def_5;
then A7: S1[ 0 ] by BCIALG_1:def_11;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A7, A6);
hence  (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 ; ::_thesis: verum
end;
assume A8: X is BCI-algebra of n, 0 ,m,m ; ::_thesis: X is BCI-commutative BCI-algebra
 for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume A9: x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
 Polynom (n,0,x,y) = Polynom (m,m,y,x) by A8, Def3;
then  (x,(y \ x)) to_power 0 = (((y,(y \ x)) to_power (m + 1)),(0. X)) to_power m by A9, BCIALG_2:5;
then  (x,(y \ x)) to_power 0 = ((((y,(y \ x)) to_power (m + 1)),(0. X)) to_power m) \ (0. X) by BCIALG_1:2;
then  (x,(y \ x)) to_power 0 = (((y,(y \ x)) to_power (m + 1)),(0. X)) to_power (m + 1) by BCIALG_2:4;
then  (x,(y \ x)) to_power 0 = (y,(y \ x)) to_power (m + 1) by BCIALG_2:5;
then  x = (y,(y \ x)) to_power (m + 1) by BCIALG_2:1;
then  x <= (y,(y \ x)) to_power 1 by A1, A9;
then A10: x <= y \ (y \ x) by BCIALG_2:2;
 (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7;
then  (y \ (y \ x)) \ x = 0. X by BCIALG_1:def_5;
then  y \ (y \ x) <= x by BCIALG_1:def_11;
hence  x = y \ (y \ x) by A10, Th2; ::_thesis: verum
end;
hence  X is BCI-commutative BCI-algebra by BCIALG_3:def_4; ::_thesis: verum
end;

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 & m > 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st j = 0 & m > 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
let X be BCK-algebra of i,j,m,n; ::_thesis: ( j = 0 & m > 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 )
assume that
A1: j = 0 and
A2: m > 0 ; ::_thesis: X is BCK-algebra of 0 , 0 , 0 , 0
 for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,n,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) = Polynom (0,n,y,x)
A3: Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
A4: i + 1 >= j + 1 by A1, XREAL_1:6;
 ( (x,(x \ y)) to_power (j + 1) = (x,(x \ y)) to_power (m + 1) & j + 1 < m + 1 ) by A1, A2, Th20, XREAL_1:6;
then  (x,(x \ y)) to_power (i + 1) = (x,(x \ y)) to_power (0 + 1) by A1, A4, Th6;
hence  Polynom (0,0,x,y) = Polynom (0,n,y,x) by A1, A3, Th20; ::_thesis: verum
end;
then reconsider X = X as BCK-algebra of 0 , 0 , 0 ,n by Def3;
A5: for x, y being Element of X holds Polynom (0,0,x,y) <= Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) <= Polynom (0,0,y,x)
 Polynom (0,0,x,y) = Polynom (0,n,y,x) by Def3;
hence  Polynom (0,0,x,y) <= Polynom (0,0,y,x) by Th5; ::_thesis: verum
end;
 for x, y being Element of X holds Polynom (0,0,y,x) = Polynom (0,0,x,y)
proof
let x, y be Element of X; ::_thesis: Polynom (0,0,y,x) = Polynom (0,0,x,y)
 Polynom (0,0,x,y) <= Polynom (0,0,y,x) by A5;
then A6: (Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X by BCIALG_1:def_11;
 Polynom (0,0,y,x) <= Polynom (0,0,x,y) by A5;
then  (Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X by BCIALG_1:def_11;
hence  Polynom (0,0,y,x) = Polynom (0,0,x,y) by A6, BCIALG_1:def_7; ::_thesis: verum
end;
hence  X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum
end;

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 & j > 0 holds
X is BCK-algebra of 0 ,1, 0 ,1
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st m = 0 & j > 0 holds
X is BCK-algebra of 0 ,1, 0 ,1
let X be BCK-algebra of i,j,m,n; ::_thesis: ( m = 0 & j > 0 implies X is BCK-algebra of 0 ,1, 0 ,1 )
reconsider X = X as BCK-algebra of i + 1,j,m,n + 1 by Th17;
assume that
A1: m = 0 and
A2: j > 0 ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x)
A3: (i + 1) + 1 > (m + 1) + 0 by A1, XREAL_1:8;
A4: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (m + 1) by Th20;
A5: j + 1 > m + 1 by A1, A2, XREAL_1:6;
 ( n + 1 >= m + 1 & (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (m + 1) ) by A1, Th20, XREAL_1:6;
then A6: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (0 + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by A1, A5, Th6;
 ( Polynom ((i + 1),j,x,y) = Polynom (m,(n + 1),y,x) & (x,(x \ y)) to_power (j + 1) = (x,(x \ y)) to_power (m + 1) ) by Def3, Th20;
then  (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power j = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by A1, A5, A3, Th6;
hence  Polynom (0,1,x,y) = Polynom (0,1,y,x) by A1, A5, A6, A4, Th6, NAT_1:14; ::_thesis: verum
end;
hence  X is BCK-algebra of 0 ,1, 0 ,1 by Def3; ::_thesis: verum
end;

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 & i <> 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st n = 0 & i <> 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
let X be BCK-algebra of i,j,m,n; ::_thesis: ( n = 0 & i <> 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 )
assume that
A1: n = 0 and
A2: i <> 0 ; ::_thesis: X is BCK-algebra of 0 , 0 , 0 , 0
 for x, y being Element of X holds Polynom (0,j,x,y) = Polynom (0,0,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,j,x,y) = Polynom (0,0,y,x)
A3: Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
A4: m + 1 >= n + 1 by A1, XREAL_1:6;
 ( (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (i + 1) & n + 1 < i + 1 ) by A1, A2, Th19, XREAL_1:6;
then  (y,(y \ x)) to_power (m + 1) = (y,(y \ x)) to_power (0 + 1) by A1, A4, Th6;
hence  Polynom (0,j,x,y) = Polynom (0,0,y,x) by A1, A3, Th19; ::_thesis: verum
end;
then reconsider X = X as BCK-algebra of 0 ,j, 0 , 0 by Def3;
A5: for x, y being Element of X holds Polynom (0,0,y,x) <= Polynom (0,0,x,y)
proof
let x, y be Element of X; ::_thesis: Polynom (0,0,y,x) <= Polynom (0,0,x,y)
 Polynom (0,j,x,y) = Polynom (0,0,y,x) by Def3;
hence  Polynom (0,0,y,x) <= Polynom (0,0,x,y) by Th5; ::_thesis: verum
end;
 for x, y being Element of X holds Polynom (0,0,y,x) = Polynom (0,0,x,y)
proof
let x, y be Element of X; ::_thesis: Polynom (0,0,y,x) = Polynom (0,0,x,y)
 Polynom (0,0,x,y) <= Polynom (0,0,y,x) by A5;
then A6: (Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X by BCIALG_1:def_11;
 Polynom (0,0,y,x) <= Polynom (0,0,x,y) by A5;
then  (Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X by BCIALG_1:def_11;
hence  Polynom (0,0,y,x) = Polynom (0,0,x,y) by A6, BCIALG_1:def_7; ::_thesis: verum
end;
hence  X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum
end;

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 & n <> 0 holds
X is BCK-algebra of 0 ,1, 0 ,1
proof
let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = 0 & n <> 0 holds
X is BCK-algebra of 0 ,1, 0 ,1
let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = 0 & n <> 0 implies X is BCK-algebra of 0 ,1, 0 ,1 )
reconsider X = X as BCK-algebra of i,j + 1,m + 1,n by Th18;
assume that
A1: i = 0 and
A2: n <> 0 ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1
 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x)
proof
let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x)
A3: (m + 1) + 1 > (i + 1) + 0 by A1, XREAL_1:8;
A4: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by Th19;
A5: n + 1 > i + 1 by A1, A2, XREAL_1:6;
 ( j + 1 >= i + 1 & (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (n + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (i + 1) ) by A1, Th19, XREAL_1:6;
then A6: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (0 + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) by A1, A5, Th6;
 ( Polynom (i,(j + 1),x,y) = Polynom ((m + 1),n,y,x) & (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (i + 1) ) by Def3, Th19;
then  (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power n by A1, A5, A3, Th6;
hence  Polynom (0,1,x,y) = Polynom (0,1,y,x) by A1, A5, A6, A4, Th6, NAT_1:14; ::_thesis: verum
end;
hence  X is BCK-algebra of 0 ,1, 0 ,1 by Def3; ::_thesis: verum
end;