:: General Theory of Quasi-Commutative BCI-algebras
:: by Tao Sun , Weibo Pan , Chenglong Wu and Xiquan Liang
::
:: Received May 13, 2008
:: Copyright (c) 2008-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, BCIALG_1, SUBSET_1, POLYEQ_1, XBOOLE_0, POWER, ARYTM_3,
FUNCT_1, STRUCT_0, XXREAL_0, SUPINF_2, CARD_1, ARYTM_1, NAT_1, BINOP_1,
TARSKI, CHORD, FILTER_0, BCIALG_3, BCIALG_5;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1, ORDINAL1, NUMBERS,
XXREAL_0, REAL_1, FUNCT_2, XCMPLX_0, NAT_1, BCIALG_2, BCIALG_3;
constructors REAL_1, NAT_1, BCIALG_2, BCIALG_3, XREAL_0, NUMBERS;
registrations BCIALG_1, STRUCT_0, ORDINAL1, XXREAL_0, XREAL_0, BCIALG_3,
NAT_1, BCIALG_2, XCMPLX_0;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
begin :: The Basics of General Theory of Quasi-Commutative BCI-algebra
definition
let X be BCI-algebra;
let x,y be Element of X;
let m,n be Nat;
func Polynom (m,n,x,y) -> Element of X equals
:: BCIALG_5:def 1
(((x,(x\y)) to_power (m+1)),(y
\x)) to_power n;
end;
reserve X for BCI-algebra;
reserve x,y,z for Element of X;
reserve i,j,k,l,m,n for Nat;
reserve f,g for sequence of the carrier of X;
theorem :: BCIALG_5:1
x <= y & y <= z implies x <= z;
theorem :: BCIALG_5:2
x <= y & y <= x implies x = y;
theorem :: BCIALG_5:3
for X being BCK-algebra,x,y being Element of X holds x\y <= x & (
x,y) to_power (n+1) <= (x,y) to_power n;
theorem :: BCIALG_5:4
for X being BCK-algebra,x being Element of X holds (0.X,x) to_power n = 0.X;
theorem :: BCIALG_5:5
for X being BCK-algebra,x,y being Element of X st m>=n
holds (x,y) to_power m <= (x,y) to_power n;
theorem :: BCIALG_5:6
for X being BCK-algebra, x,y being Element of X st m>n & (x,y)
to_power n = (x,y) to_power m holds for k being Nat st k >=n holds (
x,y) to_power n = (x,y) to_power k;
theorem :: BCIALG_5:7
Polynom (0,0,x,y) = x\(x\y);
theorem :: BCIALG_5:8
Polynom (m,n,x,y) = (((Polynom (0,0,x,y),(x\y)) to_power m),(y\x)) to_power n
;
theorem :: BCIALG_5:9
Polynom (m+1,n,x,y) = Polynom (m,n,x,y) \ (x\y);
theorem :: BCIALG_5:10
Polynom (m,n+1,x,y) = Polynom (m,n,x,y) \ (y\x);
theorem :: BCIALG_5:11
Polynom (n+1,n+1,y,x) <= Polynom (n,n+1,x,y);
theorem :: BCIALG_5:12
Polynom (n,n+1,x,y) <= Polynom (n,n,y,x);
definition
let X be BCI-algebra;
attr X is quasi-commutative means
:: BCIALG_5:def 2
ex i,j,m,n being Element of NAT st
for x,y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x);
end;
registration
cluster BCI-EXAMPLE -> quasi-commutative;
end;
registration
cluster quasi-commutative for BCI-algebra;
end;
definition
let i,j,m,n be Nat;
mode BCI-algebra of i,j,m,n -> BCI-algebra means
:: BCIALG_5:def 3
for x,y being Element of it holds Polynom (i,j,x,y) = Polynom (m,n,y,x);
end;
theorem :: BCIALG_5:13
X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j;
theorem :: BCIALG_5:14
for X being BCI-algebra of i,j,m,n holds for k being Element of
NAT holds X is BCI-algebra of i+k,j,m,n+k;
theorem :: BCIALG_5:15
for X being BCI-algebra of i,j,m,n holds for k being Element of NAT
holds X is BCI-algebra of i,j+k,m+k,n;
registration
cluster quasi-commutative for BCK-algebra;
end;
registration
let i,j,m,n be Nat;
cluster being_BCK-5 for BCI-algebra of i,j,m,n;
end;
definition
let i,j,m,n be Nat;
mode BCK-algebra of i,j,m,n is being_BCK-5 BCI-algebra of i,j,m,n;
end;
theorem :: BCIALG_5:16
X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j;
theorem :: BCIALG_5:17
for X being BCK-algebra of i,j,m,n holds for k being Element of
NAT holds X is BCK-algebra of i+k,j,m,n+k;
theorem :: BCIALG_5:18
for X being BCK-algebra of i,j,m,n holds for k being Element of
NAT holds X is BCK-algebra of i,j+k,m+k,n;
theorem :: BCIALG_5:19
for X being BCK-algebra of i,j,m,n holds for x,y being Element
of X holds (x,y) to_power (i+1) = (x,y) to_power (n+1);
theorem :: BCIALG_5:20
for X being BCK-algebra of i,j,m,n holds for x,y being Element
of X holds (x,y) to_power (j+1) = (x,y) to_power (m+1);
theorem :: BCIALG_5:21
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j ,j,n;
theorem :: BCIALG_5:22
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j ,m,n;
:: The Reduction of the Type of Quasi-Commutative BCK-algebra
definition
let i,j,m,n;
func min(i,j,m,n) -> ExtReal equals
:: BCIALG_5:def 4
min(min(i,j),min(m,n));
func max(i,j,m,n) -> ExtReal equals
:: BCIALG_5:def 5
max(max(i,j),max(m,n));
end;
theorem :: BCIALG_5:23
min(i,j,m,n) = i or min(i,j,m,n) = j or min(i,j,m,n) = m or min(i,j,m, n) = n
;
theorem :: BCIALG_5:24
max(i,j,m,n) = i or max(i,j,m,n) = j or max(i,j,m,n) = m or max(i,j,m, n) = n
;
theorem :: BCIALG_5:25
i = min(i,j,m,n) implies i<=j & i<=m & i<=n;
theorem :: BCIALG_5:26
max(i,j,m,n) >= i & max(i,j,m,n) >= j & max(i,j,m,n) >= m & max(
i,j,m,n) >= n;
theorem :: BCIALG_5:27
for X being BCK-algebra of i,j,m,n st i = min(i,j,m,n) holds ( i
= j implies X is BCK-algebra of i,i,i,i );
theorem :: BCIALG_5:28
for X being BCK-algebra of i,j,m,n st i = min(i,j,m,n) holds ( i < j &
i < n implies X is BCK-algebra of i,i+1,i,i+1 );
theorem :: BCIALG_5:29
for X being BCK-algebra of i,j,m,n st i = min(i,j,m,n) holds ( i = n &
i = m implies X is BCK-algebra of i,i,i,i );
theorem :: BCIALG_5:30
for X being BCK-algebra of i,j,m,n st i = n & m < j holds X is
BCK-algebra of i,m+1,m,i;
theorem :: BCIALG_5:31
for X being BCK-algebra of i,j,m,n st i = n holds X is BCK-algebra of i,j,j,i
;
theorem :: BCIALG_5:32
for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds X is
BCK-algebra of k,l,l,k;
theorem :: BCIALG_5:33
for X being BCK-algebra of i,j,m,n st k >= max(i,j,m,n) holds X is
BCK-algebra of k,k,k,k;
theorem :: BCIALG_5:34
for X being BCK-algebra of i,j,m,n st i <= m & j <= n holds X is
BCK-algebra of i,j,i,j;
theorem :: BCIALG_5:35
for X being BCK-algebra of i,j,m,n holds ( i <= m & i < n implies X is
BCK-algebra of i,j,i,i+1 );
theorem :: BCIALG_5:36
X is BCI-algebra of i,j,j+k,i+k implies X is BCK-algebra;
::Some Special Classes of Quasi-Commutative BCI-algebra
theorem :: BCIALG_5:37
X is BCI-algebra of 0,0,0,0 iff X is BCK-algebra of 0,0,0,0;
theorem :: BCIALG_5:38
X is commutative BCK-algebra iff X is BCI-algebra of 0,0,0,0;
notation
let X be BCI-algebra;
synonym p-Semisimple-part(X) for AtomSet(X);
end;
reserve B,P for non empty Subset of X;
theorem :: BCIALG_5:39
for X being BCI-algebra st B = BCK-part(X) & P = p-Semisimple-part(X)
holds B /\ P = {0.X};
theorem :: BCIALG_5:40
for X being BCI-algebra st P = p-Semisimple-part(X) holds (X is
BCK-algebra iff P = {0.X});
theorem :: BCIALG_5:41
for X being BCI-algebra st B = BCK-part(X) holds (X is p-Semisimple
BCI-algebra iff B = {0.X});
theorem :: BCIALG_5:42
X is p-Semisimple BCI-algebra implies X is BCI-algebra of 0,1,0, 0;
theorem :: BCIALG_5:43
X is p-Semisimple BCI-algebra implies X is BCI-algebra of n+j,n,m,m+j+ 1;
theorem :: BCIALG_5:44
X is associative BCI-algebra implies X is BCI-algebra of 0,1,0,0 & X
is BCI-algebra of 1,0,0,0;
theorem :: BCIALG_5:45
X is weakly-positive-implicative BCI-algebra implies X is BCI-algebra
of 0,1,1,1;
theorem :: BCIALG_5:46
X is positive-implicative BCI-algebra implies X is BCI-algebra of 0,1, 1,1;
theorem :: BCIALG_5:47
X is implicative BCI-algebra implies X is BCI-algebra of 0,1,0,0;
theorem :: BCIALG_5:48
X is alternative BCI-algebra implies X is BCI-algebra of 0,1,0,0;
theorem :: BCIALG_5:49
X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0,1,0,1;
theorem :: BCIALG_5:50
X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1,0,0,0;
registration
cluster BCK-implicative -> commutative for BCK-algebra;
cluster BCK-implicative -> BCK-positive-implicative for BCK-algebra;
end;
theorem :: BCIALG_5:51
X is BCK-algebra of 1,0,0,0 iff X is BCK-algebra of 0,0,0,0 & X is
BCK-algebra of 0,1,0,1;
theorem :: BCIALG_5:52
for X being quasi-commutative BCK-algebra holds (X is BCK-algebra of 0
,1,0,1 iff for x,y being Element of X holds x\y = (x\y)\y );
theorem :: BCIALG_5:53
for X being quasi-commutative BCK-algebra holds (X is BCK-algebra of n
,n+1,n,n+1 iff for x,y being Element of X holds (x,y) to_power (n+1) = (x,y)
to_power (n+2) );
theorem :: BCIALG_5:54
X is BCI-algebra of 0,1,0,0 implies X is BCI-commutative BCI-algebra;
theorem :: BCIALG_5:55
X is BCI-algebra of n,0,m,m implies X is BCI-commutative BCI-algebra;
theorem :: BCIALG_5:56
for X being BCK-algebra of i,j,m,n holds ( j = 0 & m > 0 implies X is
BCK-algebra of 0,0,0,0 );
theorem :: BCIALG_5:57
for X being BCK-algebra of i,j,m,n holds ( m = 0 & j > 0 implies X is
BCK-algebra of 0,1,0,1 );
theorem :: BCIALG_5:58
for X being BCK-algebra of i,j,m,n holds ( n = 0 & i <> 0 implies X is
BCK-algebra of 0,0,0,0 );
theorem :: BCIALG_5:59
for X being BCK-algebra of i,j,m,n holds ( i = 0 & n <> 0 implies X is
BCK-algebra of 0,1,0,1 );