begin
Lm1:
for X being set
for S being Subset of
for R being Order of st R is being_linear-order holds
R linearly_orders S
Lm2:
for n being Ordinal
for b1, b2, b3 being bag of n st b1 <=' b2 holds
b1 + b3 <=' b2 + b3
Lm3:
for n being Ordinal
for b1, b2 being bag of n st b1 <=' b2 & b2 <=' b1 holds
b1 = b2
Lm4:
for n being Ordinal
for b1, b2 being bag of n holds
( not b1 < b2 iff b2 <=' b1 )
Lm5:
for n being Ordinal
for L being non trivial ZeroStr
for p being non-zero finite-Support Series of n,L ex b being bag of n st
( p . b <> 0. L & ( for b' being bag of n st b < b' holds
p . b' = 0. L ) )
Lm6:
for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for f, g being FinSequence of the carrier of L
for n being Nat st len f = n + 1 & g = f | (Seg n) holds
Sum f = (Sum g) + (f /. (len f))
begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
Lm7:
for n being Ordinal
for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for q being Element of st p = q holds
- p = - q
theorem Th6:
Lm8:
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of n st b <> term m holds
m . b = 0. L
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
begin
:: deftheorem Def1 defines *' POLYRED:def 1 :
Lm9:
for n being Ordinal
for b, b' being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds (b *' p) . (b' + b) = p . b'
Lm10:
for n being Ordinal
for L being non empty ZeroStr
for p being Polynomial of n,L
for b being bag of n holds Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p }
theorem
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
begin
Lm11:
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds Support p in Fin the carrier of RelStr(# (Bags n),T #)
:: deftheorem Def2 defines <= POLYRED:def 2 :
:: deftheorem Def3 defines < POLYRED:def 3 :
:: deftheorem defines Support POLYRED:def 4 :
theorem Th24:
theorem Th25:
Lm12:
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds 0_ n,L <= p,T
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
Lm13:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st [(HT p,T),b] in T & b <> HT p,T holds
p . b = 0. L
Lm14:
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L st HT p,T = EmptyBag n holds
Red p,T = 0_ n,L
Lm15:
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) )
theorem
Lm16:
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L st q <> 0_ n,L & HT p,T = HT q,T & Red p,T <= Red q,T,T holds
p <= q,T
theorem Th31:
theorem
for
n being
Ordinal for
T being
connected admissible TermOrder of
n for
L being non
trivial right_complementable add-associative right_zeroed addLoopStr for
p,
q being
Polynomial of
n,
L holds
(
p < q,
T iff ( (
p = 0_ n,
L &
q <> 0_ n,
L ) or
HT p,
T < HT q,
T,
T or (
HT p,
T = HT q,
T &
Red p,
T < Red q,
T,
T ) ) )
by Lm15;
theorem Th33:
theorem Th34:
theorem Th35:
begin
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f,
p,
g be
Polynomial of
n,
L;
let b be
bag of
n;
pred f reduces_to g,
p,
b,
T means :
Def5:
(
f <> 0_ n,
L &
p <> 0_ n,
L &
b in Support f & ex
s being
bag of
n st
(
s + (HT p,T) = b &
g = f - (((f . b) / (HC p,T)) * (s *' p)) ) );
end;
:: deftheorem Def5 defines reduces_to POLYRED:def 5 :
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for
f,
p,
g being
Polynomial of
n,
L for
b being
bag of
n holds
(
f reduces_to g,
p,
b,
T iff (
f <> 0_ n,
L &
p <> 0_ n,
L &
b in Support f & ex
s being
bag of
n st
(
s + (HT p,T) = b &
g = f - (((f . b) / (HC p,T)) * (s *' p)) ) ) );
:: deftheorem Def6 defines reduces_to POLYRED:def 6 :
:: deftheorem Def7 defines reduces_to POLYRED:def 7 :
:: deftheorem Def8 defines is_reducible_wrt POLYRED:def 8 :
:: deftheorem defines is_reducible_wrt POLYRED:def 9 :
:: deftheorem defines top_reduces_to POLYRED:def 10 :
:: deftheorem defines is_top_reducible_wrt POLYRED:def 11 :
:: deftheorem defines is_top_reducible_wrt POLYRED:def 12 :
theorem
Lm17:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g
theorem Th37:
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
begin
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be
Subset of ;
func PolyRedRel P,
T -> Relation of ,
means :
Def13:
for
p,
q being
Polynomial of
n,
L holds
(
[p,q] in it iff
p reduces_to q,
P,
T );
existence
ex b1 being Relation of , st
for p, q being Polynomial of n,L holds
( [p,q] in b1 iff p reduces_to q,P,T )
uniqueness
for b1, b2 being Relation of , st ( for p, q being Polynomial of n,L holds
( [p,q] in b1 iff p reduces_to q,P,T ) ) & ( for p, q being Polynomial of n,L holds
( [p,q] in b2 iff p reduces_to q,P,T ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines PolyRedRel POLYRED:def 13 :
Lm18:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds
( f <> 0_ n,L & p <> 0_ n,L )
theorem
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem Th49:
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
P being
Subset of
for
f,
g,
h,
h1 being
Polynomial of
n,
L st
f - g = h &
PolyRedRel P,
T reduces h,
h1 holds
ex
f1,
g1 being
Polynomial of
n,
L st
(
f1 - g1 = h1 &
PolyRedRel P,
T reduces f,
f1 &
PolyRedRel P,
T reduces g,
g1 )
theorem Th50:
theorem Th51:
:: deftheorem Def14 defines are_congruent_mod POLYRED:def 14 :
theorem
theorem Th53:
theorem Th54:
theorem
theorem
Lm19:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of
for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f', g' being Element of st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal
theorem Th57:
Lm20:
for n being Nat
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being non empty Subset of
for f, p, h being Element of st p in P & p <> 0_ n,L & h <> 0_ n,L holds
f,f + (h * p) are_convertible_wrt PolyRedRel P,T
theorem
theorem Th59:
theorem