:: POLYRED semantic presentation

registration

let n be Ordinal;
let R be non trivial ZeroStr ;
cluster non-zero Relation of Bags n,the carrier of R;
existence

proof end;

end;

registration

cluster non trivial doubleLoopStr ;
existence

proof end;

end;

Lm1: for X being set
for S being Subset of X
for R being Order of X st R is_linear-order holds
R linearly_orders S

proof end;

Lm2: for n being Ordinal
for b1, b2, b3 being bag of n st b1 <=' b2 holds
b1 + b3 <=' b2 + b3

proof end;

Lm3: for n being Ordinal
for b1, b2 being bag of n st b1 <=' b2 & b2 <=' b1 holds
b1 = b2

proof end;

Lm4: for n being Ordinal
for b1, b2 being bag of n holds
( not b1 < b2 iff b2 <=' b1 )

proof end;

Lm5: for n being Ordinal
for L being non trivial ZeroStr
for p being finite-Support non-zero 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 ) )

proof end;

Lm6: for L being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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))

proof end;

registration

let n be Ordinal;
let L be unital add-associative right_zeroed right_complementable distributive domRing-like left_zeroed non trivial doubleLoopStr ;
let p, q be finite-Support non-zero Series of n,L;
cluster p *' q -> non-zero ;
coherence

proof end;

end;

theorem Th1: :: POLYRED:1

for X being set
for L being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for p, q being Series of X,L holds - (p + q) = (- p) + (- q)

proof end;

theorem Th2: :: POLYRED:2

for X being set
for L being non empty left_zeroed LoopStr
for p being Series of X,L holds (0_ X,L) + p = p

proof end;

theorem Th3: :: POLYRED:3

for X being set
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being Series of X,L holds
( (- p) + p = 0_ X,L & p + (- p) = 0_ X,L )

proof end;

theorem Th4: :: POLYRED:4

for n being set
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being Series of n,L holds p - (0_ n,L) = p

proof end;

theorem Th5: :: POLYRED:5

for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable left-distributive add-left-cancelable doubleLoopStr
for p being Series of n,L holds (0_ n,L) *' p = 0_ n,L

proof end;

Lm7: for n being Ordinal
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for p being Polynomial of n,L
for q being Element of (Polynom-Ring n,L) st p = q holds
- p = - q

proof end;

theorem Th6: :: POLYRED:6

for n being Ordinal
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for p, q being Polynomial of n,L holds
( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )

proof end;

Lm8: for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable LoopStr
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

proof end;

theorem Th7: :: POLYRED:7

for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)

proof end;

theorem Th8: :: POLYRED:8

for X being set
for L being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for p being Series of X,L holds (0. L) * p = 0_ X,L

proof end;

theorem Th9: :: POLYRED:9

for X being set
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for p being Series of X,L
for a being Element of L holds
( - (a * p) = (- a) * p & - (a * p) = a * (- p) )

proof end;

theorem Th10: :: POLYRED:10

for X being set
for L being non empty left-distributive doubleLoopStr
for p being Series of X,L
for a, a' being Element of L holds (a * p) + (a' * p) = (a + a') * p

proof end;

theorem Th11: :: POLYRED:11

for X being set
for L being non empty associative multLoopStr_0
for p being Series of X,L
for a, a' being Element of L holds (a * a') * p = a * (a' * p)

proof end;

theorem Th12: :: POLYRED:12

for n being Ordinal
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive doubleLoopStr
for p, p' being Series of n,L
for a being Element of L holds a * (p *' p') = p *' (a * p')

proof end;

definition

let n be Ordinal;
let b be bag of n;
let L be non empty ZeroStr ;
let p be Series of n,L;
func b *' p -> Series of n,L means :Def1: :: POLYRED:def 1
for b' being bag of n st b divides b' holds
( it . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
it . b' = 0. L ) );
existence

proof end;

uniqueness

proof end;

end;

:: 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'

proof end;

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 }

proof end;

registration

let n be Ordinal;
let b be bag of n;
let L be non empty ZeroStr ;
let p be finite-Support Series of n,L;
cluster b *' p -> finite-Support ;
coherence

proof end;

end;

theorem :: POLYRED:13

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' by Lm9;

theorem :: POLYRED:14

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 } by Lm10;

theorem Th15: :: POLYRED:15

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L
for b being bag of n holds HT (b *' p),T = b + (HT p,T)

proof end;

theorem Th16: :: POLYRED:16

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b, b' being bag of n st b' in Support (b *' p) holds
b' <= b + (HT p,T),T

proof end;

theorem :: POLYRED:17

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L holds (EmptyBag n) *' p = p

proof end;

theorem Th18: :: POLYRED:18

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L
for b1, b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p)

proof end;

theorem Th19: :: POLYRED:19

for n being Ordinal
for L being add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L holds Support (a * p) c= Support p

proof end;

theorem :: POLYRED:20

for n being Ordinal
for L being domRing-like non trivial doubleLoopStr
for p being Polynomial of n,L
for a being non-zero Element of L holds Support p c= Support (a * p)

proof end;

theorem Th21: :: POLYRED:21

for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr
for p being Polynomial of n,L
for a being non-zero Element of L holds HT (a * p),T = HT p,T

proof end;

theorem Th22: :: POLYRED:22

for n being Ordinal
for L being add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom a,b) *' p

proof end;

theorem :: POLYRED:23

for n being Ordinal
for T being connected admissible TermOrder of n
for L being unital add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr
for p being non-zero Polynomial of n,L
for q being Polynomial of n,L
for m being non-zero Monomial of n,L st HT p,T in Support q holds
HT (m *' p),T in Support (m *' q)

proof end;

registration

let n be Ordinal;
let T be connected TermOrder of n;
cluster RelStr(# (Bags n),T #) -> connected ;
coherence

proof end;

end;

registration

let n be Nat;
let T be admissible TermOrder of n;
cluster RelStr(# (Bags n),T #) -> well_founded ;
coherence

proof end;

end;

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 #)

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p, q be Polynomial of n,L;
pred p <= q,T means :Def2: :: POLYRED:def 2
[(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #);

end;

:: deftheorem Def2 defines <= POLYRED:def 2 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p, q be Polynomial of n,L;
pred p < q,T means :Def3: :: POLYRED:def 3
( p <= q,T & Support p <> Support q );

end;

:: deftheorem Def3 defines < POLYRED:def 3 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func Support p,T -> Element of Fin the carrier of RelStr(# (Bags n),T #) equals :: POLYRED:def 4
Support p;
coherence by Lm11;

end;

:: deftheorem defines Support POLYRED:def 4 :

theorem Th24: :: POLYRED:24

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L holds PosetMax (Support p,T) = HT p,T

proof end;

theorem Th25: :: POLYRED:25

for n being Ordinal
for T being connected TermOrder of n
for L being non empty LoopStr
for p being Polynomial of n,L holds p <= p,T

proof end;

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

proof end;

theorem Th26: :: POLYRED:26

for n being Ordinal
for T being connected TermOrder of n
for L being non empty LoopStr
for p, q being Polynomial of n,L holds
( ( p <= q,T & q <= p,T ) iff Support p = Support q )

proof end;

theorem Th27: :: POLYRED:27

for n being Ordinal
for T being connected TermOrder of n
for L being non empty LoopStr
for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds
p <= r,T

proof end;

theorem Th28: :: POLYRED:28

for n being Ordinal
for T being connected TermOrder of n
for L being non empty LoopStr
for p, q being Polynomial of n,L holds
( p <= q,T or q <= p,T )

proof end;

theorem Th29: :: POLYRED:29

for n being Ordinal
for T being connected TermOrder of n
for L being non empty LoopStr
for p, q being Polynomial of n,L holds
( p <= q,T iff not q < p,T )

proof end;

Lm13: for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
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

proof end;

Lm14: for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L st HT p,T = EmptyBag n holds
Red p,T = 0_ n,L

proof end;

Lm15: for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
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 ) ) )

proof end;

theorem :: POLYRED:30

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 by Lm12;

Lm16: for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
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

proof end;

theorem Th31: :: POLYRED:31

for n being Nat
for T being connected admissible TermOrder of n
for L being unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for P being non empty Subset of (Polynom-Ring n,L) ex p being Polynomial of n,L st
( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )

proof end;

theorem :: POLYRED:32

for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
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: :: POLYRED:33

for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being non-zero Polynomial of n,L holds Red p,T < HM p,T,T

proof end;

theorem Th34: :: POLYRED:34

for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds HM p,T <= p,T

proof end;

theorem Th35: :: POLYRED:35

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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: :: POLYRED:def 5
( 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 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f, p, g be Polynomial of n,L;
pred f reduces_to g,p,T means :Def6: :: POLYRED:def 6
ex b being bag of n st f reduces_to g,p,b,T;

end;

:: deftheorem Def6 defines reduces_to POLYRED:def 6 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f, g be Polynomial of n,L;
let P be Subset of (Polynom-Ring n,L);
pred f reduces_to g,P,T means :Def7: :: POLYRED:def 7
ex p being Polynomial of n,L st
( p in P & f reduces_to g,p,T );

end;

:: deftheorem Def7 defines reduces_to POLYRED:def 7 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f, p be Polynomial of n,L;
pred f is_reducible_wrt p,T means :Def8: :: POLYRED:def 8
ex g being Polynomial of n,L st f reduces_to g,p,T;

end;

:: deftheorem Def8 defines is_reducible_wrt POLYRED:def 8 :

notation

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f, p be Polynomial of n,L;
antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T;
antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T;

end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be Subset of (Polynom-Ring n,L);
pred f is_reducible_wrt P,T means :: POLYRED:def 9
ex g being Polynomial of n,L st f reduces_to g,P,T;

end;

:: deftheorem defines is_reducible_wrt POLYRED:def 9 :

notation

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be Subset of (Polynom-Ring n,L);
antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T;
antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T;

end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f, p, g be Polynomial of n,L;
pred f top_reduces_to g,p,T means :: POLYRED:def 10
f reduces_to g,p, HT f,T,T;

end;

:: deftheorem defines top_reduces_to POLYRED:def 10 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f, p be Polynomial of n,L;
pred f is_top_reducible_wrt p,T means :: POLYRED:def 11
ex g being Polynomial of n,L st f top_reduces_to g,p,T;

end;

:: deftheorem defines is_top_reducible_wrt POLYRED:def 11 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be Subset of (Polynom-Ring n,L);
pred f is_top_reducible_wrt P,T means :: POLYRED:def 12
ex p being Polynomial of n,L st
( p in P & f is_top_reducible_wrt p,T );

end;

:: deftheorem defines is_top_reducible_wrt POLYRED:def 12 :

theorem :: POLYRED:36

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT p,T divides b ) )

proof end;

Lm17: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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

proof end;

theorem Th37: :: POLYRED:37

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p being Polynomial of n,L holds 0_ n,L is_irreducible_wrt p,T

proof end;

theorem :: POLYRED:38

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, p being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds
HT (m *' p),T in Support f

proof end;

theorem :: POLYRED:39

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 by Lm17;

theorem Th40: :: POLYRED:40

for n being Ordinal
for T being connected admissible TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b' being bag of n st b < b',T & f reduces_to g,p,b,T holds
( b' in Support g iff b' in Support f )

proof end;

theorem Th41: :: POLYRED:41

proof end;

theorem Th42: :: POLYRED:42

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT f,T,T

proof end;

theorem Th43: :: POLYRED:43

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
func PolyRedRel P,T -> Relation of the carrier of (Polynom-Ring n,L) \ {(0_ n,L)},the carrier of (Polynom-Ring n,L) means :Def13: :: POLYRED:def 13
for p, q being Polynomial of n,L holds
( [p,q] in it iff p reduces_to q,P,T );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines PolyRedRel POLYRED:def 13 :

Lm18: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 )

proof end;

theorem :: POLYRED:44

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
( g <= f,T & ( g = 0_ n,L or HT g,T <= HT f,T,T ) )

proof end;

registration

let n be Nat;
let T be connected admissible TermOrder of n;
let L be non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
cluster PolyRedRel P,T -> strongly-normalizing ;
coherence

proof end;

end;

theorem Th45: :: POLYRED:45

for n being Nat
for T being connected admissible TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like left_zeroed non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, h being Polynomial of n,L st f in P holds
PolyRedRel P,T reduces h *' f, 0_ n,L

proof end;

theorem Th46: :: POLYRED:46

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T

proof end;

theorem Th47: :: POLYRED:47

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel P,T reduces f,g holds
PolyRedRel P,T reduces m *' f,m *' g

proof end;

theorem :: POLYRED:48

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel P,T reduces f, 0_ n,L holds
PolyRedRel P,T reduces m *' f, 0_ n,L

proof end;

theorem Th49: :: POLYRED:49

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
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 )

proof end;

theorem Th50: :: POLYRED:50

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g being Polynomial of n,L st PolyRedRel P,T reduces f - g, 0_ n,L holds
f,g are_convergent_wrt PolyRedRel P,T

proof end;

theorem Th51: :: POLYRED:51

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g being Polynomial of n,L st PolyRedRel P,T reduces f - g, 0_ n,L holds
f,g are_convertible_wrt PolyRedRel P,T

proof end;

definition

let R be non empty LoopStr ;
let I be Subset of R;
let a, b be Element of R;
pred a,b are_congruent_mod I means :Def14: :: POLYRED:def 14
a - b in I;

end;

:: deftheorem Def14 defines are_congruent_mod POLYRED:def 14 :

theorem :: POLYRED:52

for R being non empty add-associative right_zeroed right_complementable right-distributive left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a being Element of R holds a,a are_congruent_mod I

proof end;

theorem Th53: :: POLYRED:53

for R being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for I being non empty right-ideal Subset of R
for a, b being Element of R st a,b are_congruent_mod I holds
b,a are_congruent_mod I

proof end;

theorem Th54: :: POLYRED:54

for R being non empty add-associative right_zeroed right_complementable LoopStr
for I being non empty add-closed Subset of R
for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds
a,c are_congruent_mod I

proof end;

theorem :: POLYRED:55

for R being unital associative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for I being non empty add-closed Subset of R
for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds
a + c,b + d are_congruent_mod I

proof end;

theorem :: POLYRED:56

for R being non empty commutative add-associative right_zeroed right_complementable distributive doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds
a * c,b * d are_congruent_mod I

proof end;

Lm19: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal

proof end;

theorem Th57: :: POLYRED:57

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g being Element of (Polynom-Ring n,L) st f,g are_convertible_wrt PolyRedRel P,T holds
f,g are_congruent_mod P -Ideal

proof end;

Lm20: for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being non empty Subset of (Polynom-Ring n,L)
for f, p, h being Element of (Polynom-Ring n,L) st p in P & p <> 0_ n,L & h <> 0_ n,L holds
f,f + (h * p) are_convertible_wrt PolyRedRel P,T

proof end;

theorem :: POLYRED:58

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being non empty Subset of (Polynom-Ring n,L)
for f, g being Element of (Polynom-Ring n,L) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel P,T

proof end;

theorem Th59: :: POLYRED:59

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g being Polynomial of n,L st PolyRedRel P,T reduces f,g holds
f - g in P -Ideal

proof end;

theorem :: POLYRED:60

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f being Polynomial of n,L st PolyRedRel P,T reduces f, 0_ n,L holds
f in P -Ideal

proof end;