environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, XBOOLE_0, BCIALG_1;
theorems TARSKI, STRUCT_0, BCIALG_1, XREAL_1, XXREAL_0, XBOOLE_0, BCIALG_3, NAT_1, BCIALG_2;
schemes NAT_1;
registrations BCIALG_1, STRUCT_0, ORDINAL1, XXREAL_0, XREAL_0, BCIALG_3, NAT_1, BCIALG_2, XCMPLX_0;
constructors HIDDEN, REAL_1, NAT_1, BCIALG_2, BCIALG_3, XREAL_0, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
equalities BCIALG_1;
expansions TARSKI, BCIALG_1;
theorem
for
X being
BCI-algebra for
x,
y being
Element of
X for
m,
n being
Nat holds
Polynom (
m,
n,
x,
y)
= (
(((Polynom (0,0,x,y)),(x \ y)) to_power m),
(y \ x))
to_power n
definition
let X be
BCI-algebra;
attr X is
quasi-commutative means
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 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) );
definition
let i,
j,
m,
n be
Nat;
mode BCI-algebra of
i,
j,
m,
n -> BCI-algebra means :
Def3:
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)
end;
::
deftheorem Def3 defines
BCI-algebra BCIALG_5:def 3 :
for i, j, m, n being 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
for
i,
j,
m,
n being
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 )
theorem
for
i,
j,
m,
n being
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 )
theorem Th25:
for
i,
j,
m,
n being
Nat st
i = min (
i,
j,
m,
n) holds
(
i <= j &
i <= m &
i <= n )
theorem Th26:
for
i,
j,
m,
n being
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 )
theorem Th27:
for
i,
j,
m,
n being
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
theorem
for
i,
j,
m,
n being
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
theorem
for
i,
j,
m,
n being
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
theorem
for
i,
j,
k,
l,
m,
n being
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
theorem
for
i,
j,
k,
m,
n being
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