:: POLYRED semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let n be Ordinal;
let R be non trivial ZeroStr ;
cluster non-zero Relation of Bags n,the carrier of R;
existence
ex b1 being Monomial of n,R st b1 is non-zero
proof end;
end;

registration
cluster non trivial doubleLoopStr ;
existence
not for b1 being Field holds b1 is trivial
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
p *' q is non-zero
proof end;
end;

theorem Th1: :: POLYRED:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Series of n,L st
for b' being bag of n st b divides b' holds
( b1 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
b1 . b' = 0. L ) )
proof end;
uniqueness
for b1, b2 being Series of n,L st ( for b' being bag of n st b divides b' holds
( b1 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
b1 . b' = 0. L ) ) ) & ( for b' being bag of n st b divides b' holds
( b2 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
b2 . b' = 0. L ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines *' POLYRED:def 1 :
for n being Ordinal
for b being bag of n
for L being non empty ZeroStr
for p, b5 being Series of n,L holds
( b5 = b *' p iff for b' being bag of n st b divides b' holds
( b5 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
b5 . b' = 0. L ) ) );

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
b *' p is finite-Support
proof end;
end;

theorem :: POLYRED:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
RelStr(# (Bags n),T #) is connected
proof end;
end;

registration
let n be Nat;
let T be admissible TermOrder of n;
cluster RelStr(# (Bags n),T #) -> well_founded ;
coherence
RelStr(# (Bags n),T #) is well_founded
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 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p, q being Polynomial of n,L holds
( p <= q,T iff [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) );

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 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( p <= q,T & Support p <> Support q ) );

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
Support p is Element of Fin the carrier of RelStr(# (Bags n),T #)
by Lm11;
end;

:: deftheorem defines Support POLYRED:def 4 :
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,T = Support p;

theorem Th24: :: POLYRED:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 < p,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 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 :
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 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)) ) ) );

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 :
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 holds
( f reduces_to g,p,T iff ex b being bag of n st f reduces_to g,p,b,T );

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 :
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 being Polynomial of n,L
for P being Subset of (Polynom-Ring n,L) holds
( f reduces_to g,P,T iff ex p being Polynomial of n,L st
( p in P & f reduces_to g,p,T ) );

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 :
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 being Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex g being Polynomial of n,L st f reduces_to g,p,T );

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 :
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 Subset of (Polynom-Ring n,L) holds
( f is_reducible_wrt P,T iff ex g being Polynomial of n,L st f reduces_to g,P,T );

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 :
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 holds
( f top_reduces_to g,p,T iff f reduces_to g,p, HT f,T,T );

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 :
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 being Polynomial of n,L holds
( f is_top_reducible_wrt p,T iff ex g being Polynomial of n,L st f top_reduces_to g,p,T );

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 :
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 Subset of (Polynom-Ring n,L) holds
( f is_top_reducible_wrt P,T iff ex p being Polynomial of n,L st
( p in P & f is_top_reducible_wrt p,T ) );

theorem :: POLYRED:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
f . b' = g . b'
proof end;

theorem Th42: :: POLYRED:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Relation of the carrier of (Polynom-Ring n,L) \ {(0_ n,L)},the carrier of (Polynom-Ring n,L) st
for p, q being Polynomial of n,L holds
( [p,q] in b1 iff p reduces_to q,P,T )
proof end;
uniqueness
for b1, b2 being Relation of the carrier of (Polynom-Ring n,L) \ {(0_ n,L)},the carrier of (Polynom-Ring n,L) 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
proof end;
end;

:: deftheorem Def13 defines PolyRedRel POLYRED:def 13 :
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 Subset of (Polynom-Ring n,L)
for b5 being Relation of the carrier of (Polynom-Ring n,L) \ {(0_ n,L)},the carrier of (Polynom-Ring n,L) holds
( b5 = PolyRedRel P,T iff for p, q being Polynomial of n,L holds
( [p,q] in b5 iff p reduces_to q,P,T ) );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
PolyRedRel P,T is strongly-normalizing
proof end;
end;

theorem Th45: :: POLYRED:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for R being non empty LoopStr
for I being Subset of R
for a, b being Element of R holds
( a,b are_congruent_mod I iff a - b in I );

theorem :: POLYRED:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;