let n be Element of NAT ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: for f being Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L)

PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: verum

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; :: thesis: 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 ; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: for f being Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L)

now :: thesis: for f being Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L)

hence
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; :: thesis: ( f in P -Ideal implies PolyRedRel (P,T) reduces f, 0_ (n,L) )

assume A2: f in P -Ideal ; :: thesis: 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;

end;let f be Polynomial of n,L; :: thesis: ( f in P -Ideal implies PolyRedRel (P,T) reduces f, 0_ (n,L) )

assume A2: f in P -Ideal ; :: thesis: 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 :: thesis: not c9 <> 0_ (n,L)

hence
PolyRedRel (P,T) reduces f, 0_ (n,L)
by A3; :: thesis: verumassume
c9 <> 0_ (n,L)
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: verum