begin
:: 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:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
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
theorem Th9:
theorem Th10:
theorem
theorem
definition
let X be
BCI-algebra;
attr X is
quasi-commutative means :
Def2:
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) );
definition
let i,
j,
m,
n be
Element of
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 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:
theorem Th14:
theorem
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
definition
let i,
j,
m,
n be
Element of
NAT ;
func min (
i,
j,
m,
n)
-> ext-real number equals
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
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
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 )
theorem
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 )
theorem Th25:
theorem Th26:
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 )
theorem Th27:
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
theorem
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
theorem
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
theorem
theorem
theorem
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
theorem
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
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem Th42:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th49:
theorem Th50:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem