let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L st HT p1,T, HT p2,T are_disjoint holds
PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L st HT p1,T, HT p2,T are_disjoint holds
PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of n,L st HT p1,T, HT p2,T are_disjoint holds
PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L
let p1, p2 be Polynomial of n,L; :: thesis: ( HT p1,T, HT p2,T are_disjoint implies PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L )
assume A1: HT p1,T, HT p2,T are_disjoint ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L
then A2: S-Poly p1,p2,T = ((Red p1,T) *' p2) - ((Red p2,T) *' p1) by Th54;

now

per cases ( p1 = 0_ n,L or p1 <> 0_ n,L ) ;

case A3: p1 = 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then A4: (Red p2,T) *' p1 = 0_ n,L by POLYNOM1:87;
Red p1,T = 0_ n,L by A3, Th11;
then S-Poly p1,p2,T = (0_ n,L) - (0_ n,L) by A2, A4, POLYNOM1:87
.= 0_ n,L by POLYRED:4 ;
hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L by REWRITE1:13; :: thesis: verum

end;

case p1 <> 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then reconsider p1a = p1 as non-zero Polynomial of n,L by POLYNOM7:def 2;

now

let u be set ; :: thesis: ( u in {p1} implies u in {p1,p2} )
assume u in {p1} ; :: thesis: u in {p1,p2}
then u = p1 by TARSKI:def 1;
hence u in {p1,p2} by TARSKI:def 2; :: thesis: verum

end;

then A5: {p1} c= {p1,p2} by TARSKI:def 3;
then A6: PolyRedRel {p1},T c= PolyRedRel {p1,p2},T by GROEB_1:4;

now

let u be set ; :: thesis: ( u in {p2} implies u in {p1,p2} )
assume u in {p2} ; :: thesis: u in {p1,p2}
then u = p2 by TARSKI:def 1;
hence u in {p1,p2} by TARSKI:def 2; :: thesis: verum

end;

then A7: {p2} c= {p1,p2} by TARSKI:def 3;
then A8: PolyRedRel {p2},T c= PolyRedRel {p1,p2},T by GROEB_1:4;

now

per cases ( p2 = 0_ n,L or p2 <> 0_ n,L ) ;

case A9: p2 = 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then A10: (Red p1,T) *' p2 = 0_ n,L by POLYNOM1:87;
Red p2,T = 0_ n,L by A9, Th11;
then S-Poly p1,p2,T = (0_ n,L) - (0_ n,L) by A2, A10, POLYNOM1:87
.= 0_ n,L by POLYRED:4 ;
hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L by REWRITE1:13; :: thesis: verum

end;

case p2 <> 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then reconsider p2a = p2 as non-zero Polynomial of n,L by POLYNOM7:def 2;

now

per cases ( Red p1,T = 0_ n,L or Red p1,T <> 0_ n,L ) ;

case Red p1,T = 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then A11: S-Poly p1,p2,T = (0_ n,L) - ((Red p2,T) *' p1) by A2, POLYNOM1:87;

now

per cases ( Red p2,T = 0_ n,L or Red p2,T <> 0_ n,L ) ;

case Red p2,T = 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then S-Poly p1,p2,T = (0_ n,L) - (0_ n,L) by A11, POLYNOM1:87
.= 0_ n,L by POLYRED:4 ;
hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L by REWRITE1:13; :: thesis: verum

end;

case Red p2,T <> 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then reconsider rp2 = Red p2,T as non-zero Polynomial of n,L by POLYNOM7:def 2;
PolyRedRel {p1a},T reduces - (rp2 *' p1a), - (0_ n,L) by Th49, Th51;
then PolyRedRel {p1a},T reduces - (rp2 *' p1a), 0_ n,L by Th13;
then PolyRedRel {p1},T reduces S-Poly p1,p2,T, 0_ n,L by A11, Th14;
hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L by A5, GROEB_1:4, REWRITE1:23; :: thesis: verum

end;

end;

end;

hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L ; :: thesis: verum

end;

case Red p1,T <> 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then reconsider rp1 = Red p1,T as non-zero Polynomial of n,L by POLYNOM7:def 2;

now

per cases ( Red p2,T = 0_ n,L or Red p2,T <> 0_ n,L ) ;

case Red p2,T = 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then (Red p2,T) *' p1 = 0_ n,L by POLYNOM1:87;
then A12: S-Poly p1,p2,T = ((Red p1,T) *' p2) - (0_ n,L) by A1, Th54
.= (Red p1,T) *' p2 by POLYRED:4 ;
PolyRedRel {p2a},T reduces rp1 *' p2a, 0_ n,L by Th51;
hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L by A7, A12, GROEB_1:4, REWRITE1:23; :: thesis: verum

end;

case Red p2,T <> 0_ n,L ; :: thesis: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L

then reconsider rp2 = Red p2,T as non-zero Polynomial of n,L by POLYNOM7:def 2;
S-Poly p1,p2,T = ((HM p2a,T) *' rp1) - ((HM p1a,T) *' rp2) by A1, Th53;
then A13: PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T,p2 *' (Red p1,T) by A1, A6, Th55, REWRITE1:23;
PolyRedRel {p1,p2},T reduces rp1 *' p2a, 0_ n,L by A8, Th51, REWRITE1:23;
hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L by A13, REWRITE1:17; :: thesis: verum

end;

end;

end;

hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L ; :: thesis: verum

end;

end;

end;

hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L ; :: thesis: verum

end;

end;

end;

hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L ; :: thesis: verum

end;

end;

end;

hence PolyRedRel {p1,p2},T reduces S-Poly p1,p2,T, 0_ n,L ; :: thesis: verum