begin
:: deftheorem defines Polynom BCIALG_5:def 1 :
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 :
:: deftheorem defines max BCIALG_5:def 5 :
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