:: Polynomial Reduction
:: by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, ZFMISC_1, STRUCT_0, VALUED_0, POLYNOM7,
SUBSET_1, RELAT_1, SUPINF_2, POLYNOM1, VECTSP_1, ORDERS_1, TARSKI,
PRE_POLY, ARYTM_3, FUNCT_1, ALGSEQ_1, NAT_1, FINSET_1, CARD_1, XXREAL_0,
XBOOLE_0, RLVECT_1, ALGSTR_0, FINSEQ_1, CARD_3, PARTFUN1, ORDINAL4,
ARYTM_1, ALGSTR_1, LATTICES, VECTSP_2, BINOP_1, CAT_3, RELAT_2, BAGORDER,
TERMORD, XCMPLX_0, BROUWER, ORDERS_2, WELLORD1, FINSUB_1, WAYBEL_4,
MESFUNC1, REWRITE1, INT_1, IDEAL_1, POLYRED;
notations CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1,
ZFMISC_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSET_1, XXREAL_0, STRUCT_0, ALGSTR_0, ALGSTR_1, WAYBEL_0, FINSUB_1,
WAYBEL_4, REWRITE1, RLVECT_1, FINSEQ_1, XTUPLE_0, MCART_1, ORDERS_1,
VFUNCT_1, GROUP_1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1,
IDEAL_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD, PRE_POLY;
constructors REWRITE1, VECTSP_2, TRIANG_1, WAYBEL_4, WELLFND1, IDEAL_1,
BAGORDER, TERMORD, DOMAIN_1, RELSET_1, BINOP_2, FVSUM_1, VFUNCT_1,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, FINSUB_1, XREAL_0, NAT_1,
CARD_1, FINSEQ_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1,
GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, BAGORDER,
TERMORD, VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1,
RELSET_1;
requirements NUMERALS, REAL, SUBSET, BOOLE;
begin :: Preliminaries
registration
let n be Ordinal, R be non trivial ZeroStr;
cluster non-zero for Monomial of n,R;
end;
registration
cluster non trivial for Field;
end;
registration
let n be Ordinal, L be add-associative right_complementable left_zeroed
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p,q be non-zero finite-Support Series of n,L;
cluster p *' q -> non-zero;
end;
begin :: More on Polynomials and Monomials
theorem :: POLYRED:1
for X being set, L being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, p,q being Series of X, L holds -(p
+ q) = (-p) + (-q);
theorem :: POLYRED:2
for X being set, L being left_zeroed non empty addLoopStr, p
being Series of X, L holds 0_(X,L) + p = p;
theorem :: POLYRED:3
for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p being Series of X, L holds -p +
p = 0_(X,L) & p + -p = 0_(X,L);
theorem :: POLYRED:4
for n being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p be Series of n, L holds p - 0_(n
,L) = p;
theorem :: POLYRED:5
for n being Ordinal, L being add-associative right_complementable
right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p
being Series of n,L holds 0_(n,L) *' p = 0_(n,L);
theorem :: POLYRED:6
for n being Ordinal, L being Abelian right_zeroed add-associative
right_complementable well-unital distributive associative commutative non
trivial doubleLoopStr, p,q being Polynomial of n,L holds -(p *' q) = (-p) *' q
& -(p *' q) = p *' (-q);
theorem :: POLYRED:7
for n being Ordinal, L being add-associative right_complementable
right_zeroed distributive non empty doubleLoopStr, p being Polynomial of n,L,
m being Monomial of n,L, b being bag of n holds (m*'p).(term(m)+b) = m.term(m)
* p.b;
theorem :: POLYRED:8
for X being set, L being right_zeroed left_add-cancelable
left-distributive non empty doubleLoopStr, p being Series of X,L holds 0.L *
p = 0_(X,L);
theorem :: POLYRED:9
for X being set, L being add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr, p being Series of
X,L, a being Element of L holds -(a * p) = (-a) * p & -(a * p) = a * (-p);
theorem :: POLYRED:10
for X being set, L being left-distributive non empty
doubleLoopStr, p being Series of X,L, a,a9 being Element of L holds
a * p + a9 * p = (a + a9) * p;
theorem :: POLYRED:11
for X being set, L being associative non empty multLoopStr_0,
p being Series of X,L, a,a9 being Element of L holds (a * a9) * p = a * (a9 * p
);
theorem :: POLYRED:12
for n being Ordinal, L being add-associative right_zeroed
right_complementable well-unital associative commutative distributive non
empty doubleLoopStr, p,p9 being Series of n,L, a being Element of L holds a *
(p *' p9) = p *' (a * p9);
begin :: Multiplication of polynomials with bags
definition
let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be Series of n,L;
func b *' p -> Series of n,L means
:: POLYRED:def 1
for b9 being bag of n st b divides
b9 holds it.b9 = p.(b9 -' b) & for b9 being bag of n st not b divides b9 holds
it.b9 = 0.L;
end;
registration
let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be finite-Support
Series of n,L;
cluster b *' p -> finite-Support;
end;
theorem :: POLYRED:13
for n being Ordinal, b,b9 being bag of n, L being non empty ZeroStr, p
being Series of n,L holds (b*'p).(b9+b) = p.b9;
theorem :: POLYRED:14
for n being Ordinal, L being non empty ZeroStr, p being Polynomial of
n,L, b being bag of n holds Support(b*'p) c= {b + b9 where b9 is Element of
Bags n : b9 in Support p};
theorem :: POLYRED:15
for n being Ordinal, T being connected admissible TermOrder of n
, L being non trivial ZeroStr, p being non-zero Polynomial of n,L, b being bag
of n holds HT(b*'p,T) = b + HT(p,T);
theorem :: POLYRED:16
for n being Ordinal, T being connected admissible TermOrder of n
, L being non empty ZeroStr, p being Polynomial of n,L, b,b9 being bag of n
holds b9 in Support(b*'p) implies b9 <= b+HT(p,T),T;
theorem :: POLYRED:17
for n being Ordinal, T being connected TermOrder of n, L being non
empty ZeroStr, p being Series of n,L holds (EmptyBag n) *' p = p;
theorem :: POLYRED:18
for n being Ordinal, T being connected TermOrder of n, L being
non empty ZeroStr, p being Series of n,L, b1,b2 being bag of n holds (b1 + b2)
*' p = b1 *' (b2 *' p);
theorem :: POLYRED:19
for n being Ordinal, L being add-associative right_zeroed
right_complementable distributive non trivial doubleLoopStr, p being
Polynomial of n,L, a being Element of L holds Support(a*p) c= Support(p);
theorem :: POLYRED:20
for n being Ordinal, L being domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, a being non zero Element of L holds Support(p) c=
Support(a*p);
theorem :: POLYRED:21
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable distributive domRing-like
non trivial doubleLoopStr, p being Polynomial of n,L, a being non zero Element
of L holds HT(a*p,T) = HT(p,T);
theorem :: POLYRED:22
for n being Ordinal, L being add-associative
right_complementable right_zeroed distributive non trivial doubleLoopStr, p
being Series of n,L, b being bag of n, a being Element of L holds a * (b *' p)
= Monom(a,b) *' p;
theorem :: POLYRED:23
for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed well-unital
distributive domRing-like non trivial doubleLoopStr, p being non-zero
Polynomial of n,L, q being Polynomial of n,L, m being non-zero Monomial of n,L
holds HT(p,T) in Support q implies HT(m*'p,T) in Support(m*'q);
begin :: Orders on Polynomials
registration
let n be Ordinal, T be connected TermOrder of n;
cluster RelStr(#Bags n, T#) -> connected;
end;
registration
let n be Nat, T be admissible TermOrder of n;
cluster RelStr (#Bags n, T#) -> well_founded;
end;
definition :: according to p. 193
let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q
be Polynomial of n,L;
pred p <= q,T means
:: POLYRED:def 2
[Support p, Support q] in FinOrd RelStr(# Bags n, T#);
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q
be Polynomial of n,L;
pred p < q,T means
:: POLYRED:def 3
p <= q,T & Support p <> Support q;
end;
definition
let n being Ordinal, T being connected TermOrder of n, L being non empty
ZeroStr, p being Polynomial of n,L;
func Support(p,T) -> Element of Fin the carrier of RelStr(#Bags n,T#) equals
:: POLYRED:def 4
Support(p);
end;
theorem :: POLYRED:24 :: according to definition 5.15, p. 194
for n being Ordinal, T being connected TermOrder of n, L being
non trivial ZeroStr, p being non-zero Polynomial of n,L holds PosetMax(Support(
p,T)) = HT(p,T);
theorem :: POLYRED:25
:: theorem 5.12, p. 193
for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p being Polynomial of n,L holds p <= p,T;
theorem :: POLYRED:26
:: theorem 5.12, p. 193
for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T & q <= p,T iff
Support p = Support q;
theorem :: POLYRED:27
:: theorem 5.12, p. 193
for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q,r being Polynomial of n,L holds p <= q,T & q <= r,T
implies p <= r,T;
theorem :: POLYRED:28
for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T or q <= p,T;
theorem :: POLYRED:29
for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T iff not q < p,
T;
theorem :: POLYRED:30
for n being Ordinal, T being connected TermOrder of n, L being non
empty ZeroStr, p being Polynomial of n,L holds 0_(n,L) <= p,T;
theorem :: POLYRED:31
:: according to p. 193
for n being Nat, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed well-unital
distributive non trivial doubleLoopStr, P being non empty Subset of
Polynom-Ring(n,L) holds 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;
theorem :: POLYRED:32
for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed non trivial addLoopStr
, 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 :: POLYRED:33 :: exercise 5.16, p. 194
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed non trivial
addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < HM(p,T),T;
theorem :: POLYRED:34 :: exercise 5.16, p. 194
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, p
being Polynomial of n,L holds HM(p,T) <= p,T;
theorem :: POLYRED:35
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed non trivial
addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < p,T;
begin :: Polynomial Reduction
definition :: definition 5.18 (i), p. 195
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be
Polynomial of n,L, b be bag of n;
pred f reduces_to g,p,b,T means
:: 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;
definition :: definition 5.18 (ii), p. 195
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be
Polynomial of n,L;
pred f reduces_to g,p,T means
:: POLYRED:def 6
ex b being bag of n st f reduces_to g,p ,b,T;
end;
definition :: definition 5.18 (iii), p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,g be
Polynomial of n,L, P be Subset of Polynom-Ring(n,L);
pred f reduces_to g,P,T means
:: POLYRED:def 7
ex p being Polynomial of n,L st p in P & f reduces_to g,p,T;
end;
definition :: definition 5.18 (iv), p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,p be
Polynomial of n,L;
pred f is_reducible_wrt p,T means
:: POLYRED:def 8
ex g being Polynomial of n,L st f reduces_to g,p,T;
end;
notation :: definition 5.18 (iv), p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, 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 :: definition 5.18 (v), p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f be
Polynomial of n,L, 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;
notation :: definition 5.18 (v), p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f be
Polynomial of n,L, 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 :: following definition 5.18, p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, 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;
definition :: following definition 5.18, p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, 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;
definition :: following definition 5.18, p. 196
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f be
Polynomial of n,L, 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;
theorem :: POLYRED:36 :: lemma 5.20 (i), p. 197
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f
being Polynomial of n,L, 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;
theorem :: POLYRED:37
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p
being Polynomial of n,L holds 0_(n,L) is_irreducible_wrt p,T;
theorem :: POLYRED:38 :: lemma 5.20 (ii), p. 197
for n being Ordinal, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, f,p being Polynomial of n,L, m being non-zero Monomial of
n,L holds f reduces_to f-m*'p,p,T implies HT(m*'p,T) in Support f;
theorem :: POLYRED:39 :: lemma 5.20 (iii), p. 197
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non degenerated non empty
doubleLoopStr, f,p,g being Polynomial of n,L, b being bag of n holds f
reduces_to g,p,b,T implies not(b in Support g);
theorem :: POLYRED:40 :: lemma 5.20 (iii), p. 197
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T
holds f reduces_to g,p,b,T implies (b9 in Support g iff b9 in Support f);
theorem :: POLYRED:41
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T
holds f reduces_to g,p,b,T implies f.b9 = g.b9;
theorem :: POLYRED:42
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p,
T implies for b being bag of n st b in Support g holds b <= HT(f,T),T;
theorem :: POLYRED:43 :: lemma 5.20 (iv), p. 197
for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p,
T implies g < f,T;
begin :: Polynomial Reduction Relation
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of
Polynom-Ring(n,L);
func PolyRedRel(P,T) -> Relation of NonZero Polynom-Ring(n,L), the carrier
of Polynom-Ring(n,L) means
:: POLYRED:def 13
for p,q being Polynomial of n,L holds [p,q] in it iff p reduces_to q,P,T;
end;
theorem :: POLYRED:44 :: lemma 5.20 (v), p. 197
for n being Ordinal, T being connected admissible TermOrder of n, L
being Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,g being Polynomial of n,L, P being Subset of
Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,g implies g <= f,T & (g = 0_(
n,L) or HT(g,T) <= HT(f,T),T);
registration :: theorem 5.21, p. 198
let n be Nat, T be connected admissible TermOrder of n, L be Abelian
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non degenerated non empty
doubleLoopStr, P be Subset of Polynom-Ring(n,L);
cluster PolyRedRel(P,T) -> strongly-normalizing;
end;
theorem :: POLYRED:45 :: lemma 5.24 (i), p. 200
for n being Nat, T being admissible connected TermOrder of n, L
being add-associative right_complementable left_zeroed right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,h being
Polynomial of n,L holds f in P implies PolyRedRel(P,T) reduces h*'f,0_(n,L);
theorem :: POLYRED:46 :: lemma 5.24 (ii), p. 200
for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being
Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to g,P,T
implies m*'f reduces_to m*'g,P,T;
theorem :: POLYRED:47 :: lemma 5.24 (iii), p. 200
for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being
Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,g
implies PolyRedRel(P,T) reduces m*'f,m*'g;
theorem :: POLYRED:48 :: lemma 5.24 (iii), p. 200
for n being Ordinal, T being connected admissible TermOrder of n, L
being Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being
Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,0_(n
,L) implies PolyRedRel(P,T) reduces m*'f,0_(n,L);
theorem :: POLYRED:49 :: lemma 5.25 (i), p. 200
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g,h,h1 being Polynomial
of n,L holds (f - g = h & PolyRedRel(P,T) reduces h,h1) implies 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 :: POLYRED:50 :: lemma 5.25 (ii), p. 200
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,
L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convergent_wrt
PolyRedRel(P,T);
theorem :: POLYRED:51 :: lemma 5.25 (ii), p. 200
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,
L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convertible_wrt
PolyRedRel(P,T);
definition
let R be non empty addLoopStr, I be Subset of R, a,b be Element of R;
pred a,b are_congruent_mod I means
:: POLYRED:def 14
a - b in I;
end;
theorem :: POLYRED:52
for R being add-associative left_zeroed right_zeroed
right_complementable right-distributive non empty doubleLoopStr, I being
right-ideal non empty Subset of R, a being Element of R holds a,a
are_congruent_mod I;
theorem :: POLYRED:53
for R being add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr, I being right-ideal
non empty Subset of R, a,b being Element of R holds a,b are_congruent_mod I
implies b,a are_congruent_mod I;
theorem :: POLYRED:54
for R being add-associative right_zeroed right_complementable
non empty addLoopStr, I being add-closed non empty Subset of R, a,b,c being
Element of R holds a,b are_congruent_mod I & b,c are_congruent_mod I implies a,
c are_congruent_mod I;
theorem :: POLYRED:55
for R being Abelian add-associative right_zeroed right_complementable
well-unital distributive associative non trivial doubleLoopStr, I being
add-closed non empty Subset of R, a,b,c,d being Element of R holds a,b
are_congruent_mod I & c,d are_congruent_mod I implies a+c,b+d are_congruent_mod
I;
theorem :: POLYRED:56
for R being add-associative right_zeroed right_complementable
commutative distributive non empty doubleLoopStr, I being add-closed
right-ideal non empty Subset of R, a,b,c,d being Element of R holds a,b
are_congruent_mod I & c,d are_congruent_mod I implies a*c,b*d are_congruent_mod
I;
theorem :: POLYRED:57 :: lemma 5.26, p. 202
for n being Ordinal, T being connected TermOrder of n, L being
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Element of
Polynom-Ring(n,L) holds f,g are_convertible_wrt PolyRedRel(P,T) implies f,g
are_congruent_mod P-Ideal;
theorem :: POLYRED:58 :: lemma 5.26, p. 202
for n being Nat, T being admissible connected TermOrder of n, L being
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,g
being Element of Polynom-Ring(n,L) holds f,g are_congruent_mod P-Ideal implies
f,g are_convertible_wrt PolyRedRel(P,T);
theorem :: POLYRED:59 :: lemma 5.26, p. 202
for n being Ordinal, T being connected TermOrder of n, L being
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,
L holds PolyRedRel(P,T) reduces f,g implies f-g in P-Ideal;
theorem :: POLYRED:60 :: lemma 5.26, p. 202
for n being Ordinal, T being connected TermOrder of n, L being Abelian
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, P
being Subset of Polynom-Ring(n,L), f being Polynomial of n,L holds PolyRedRel(P
,T) reduces f,0_(n,L) implies f in P-Ideal;