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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) implies for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) )

set R = PolyRedRel (G,T);

assume A1: for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ; :: thesis: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) implies for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) )

set R = PolyRedRel (G,T);

assume A1: for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ; :: thesis: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

now :: thesis: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

hence
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

let g1, g2 be Polynomial of n,L; :: thesis: ( g1 in G & g2 in G implies PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) )

A2: q is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) by REWRITE1:def 11;

PolyRedRel (G,T) reduces S-Poly (g1,g2,T),q by A2, REWRITE1:def 6;

then reconsider q = q as Polynomial of n,L by Lm1;

assume ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

then q = 0_ (n,L) by A1, A2;

hence PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by A2, REWRITE1:def 6; :: thesis: verum

end;now :: thesis: ( ( S-Poly (g1,g2,T) in field (PolyRedRel (G,T)) & S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T) ) or ( not S-Poly (g1,g2,T) in field (PolyRedRel (G,T)) & S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T) ) )end;

then consider q being object such that per cases
( S-Poly (g1,g2,T) in field (PolyRedRel (G,T)) or not S-Poly (g1,g2,T) in field (PolyRedRel (G,T)) )
;

end;

case
S-Poly (g1,g2,T) in field (PolyRedRel (G,T))
; :: thesis: S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T)

end;

end;

case
not S-Poly (g1,g2,T) in field (PolyRedRel (G,T))
; :: thesis: S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T)

end;

end;

A2: q is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) by REWRITE1:def 11;

PolyRedRel (G,T) reduces S-Poly (g1,g2,T),q by A2, REWRITE1:def 6;

then reconsider q = q as Polynomial of n,L by Lm1;

assume ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

then q = 0_ (n,L) by A1, A2;

hence PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by A2, REWRITE1:def 6; :: thesis: verum

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ; :: thesis: verum