let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
let P be non empty Subset of (Polynom-Ring (n,L)); ( PolyRedRel (P,T) is with_Church-Rosser_property implies for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) )
set R = PolyRedRel (P,T);
assume A1:
PolyRedRel (P,T) is with_Church-Rosser_property
; for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
now for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)reconsider e =
0_ (
n,
L) as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
let f be
Polynomial of
n,
L;
( f in P -Ideal implies PolyRedRel (P,T) reduces f, 0_ (n,L) )assume A2:
f in P -Ideal
;
PolyRedRel (P,T) reduces f, 0_ (n,L)reconsider e =
e as
Element of
(Polynom-Ring (n,L)) ;
reconsider f9 =
f as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider f9 =
f9 as
Element of
(Polynom-Ring (n,L)) ;
f - (0_ (n,L)) = f9 - e
by Lm2;
then
f9 - e in P -Ideal
by A2, POLYRED:4;
then
f9,
e are_congruent_mod P -Ideal
by POLYRED:def 14;
then
f9,
e are_convertible_wrt PolyRedRel (
P,
T)
by POLYRED:58;
then
f9,
e are_convergent_wrt PolyRedRel (
P,
T)
by A1, REWRITE1:def 23;
then consider c being
object such that A3:
PolyRedRel (
P,
T)
reduces f,
c
and A4:
PolyRedRel (
P,
T)
reduces 0_ (
n,
L),
c
by REWRITE1:def 7;
reconsider c9 =
c as
Polynomial of
n,
L by A3, Lm4;
now not c9 <> 0_ (n,L)assume
c9 <> 0_ (
n,
L)
;
contradictionthen consider h being
Polynomial of
n,
L such that A5:
0_ (
n,
L)
reduces_to h,
P,
T
and
PolyRedRel (
P,
T)
reduces h,
c9
by A4, Lm5;
consider pp being
Polynomial of
n,
L such that
pp in P
and A6:
0_ (
n,
L)
reduces_to h,
pp,
T
by A5, POLYRED:def 7;
0_ (
n,
L)
is_reducible_wrt pp,
T
by A6, POLYRED:def 8;
hence
contradiction
by POLYRED:37;
verum end; hence
PolyRedRel (
P,
T)
reduces f,
0_ (
n,
L)
by A3;
verum end;
hence
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
; verum