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, P being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of P,T holds
PolyRedRel (G,T) is Completion of PolyRedRel (P,T)

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, P being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of P,T holds
PolyRedRel (G,T) is Completion of PolyRedRel (P,T)

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, P being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of P,T holds
PolyRedRel (G,T) is Completion of PolyRedRel (P,T)

let G, P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_of P,T implies PolyRedRel (G,T) is Completion of PolyRedRel (P,T) )
set R = PolyRedRel (P,T);
assume A1: G is_Groebner_basis_of P,T ; :: thesis: PolyRedRel (G,T) is Completion of PolyRedRel (P,T)
then PolyRedRel (G,T) is locally-confluent ;
then reconsider RG = PolyRedRel (G,T) as complete Relation ;
for a, b being object holds
( a,b are_convertible_wrt PolyRedRel (P,T) iff a,b are_convergent_wrt RG )
proof
let a, b be object ; :: thesis: ( a,b are_convertible_wrt PolyRedRel (P,T) iff a,b are_convergent_wrt RG )
A2: G -Ideal = P by A1;
A3: now :: thesis: ( a,b are_convertible_wrt PolyRedRel (P,T) implies a,b are_convergent_wrt RG )
assume A4: a,b are_convertible_wrt PolyRedRel (P,T) ; :: thesis: a,b are_convergent_wrt RG
now :: thesis: ( ( a = b & a,b are_convergent_wrt RG ) or ( a <> b & a,b are_convergent_wrt RG ) )
per cases ( a = b or a <> b ) ;
case A5: a <> b ; :: thesis: a,b are_convergent_wrt RG
(PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces a,b by ;
then consider p being RedSequence of (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) such that
A6: p . 1 = a and
A7: p . (len p) = b by REWRITE1:def 3;
reconsider l = (len p) - 1 as Element of NAT by ;
A8: 1 <= len p by NAT_1:14;
set h = p . l;
set g = p . (1 + 1);
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg (len p) by FINSEQ_1:1;
then A9: l + 1 in dom p by FINSEQ_1:def 3;
now :: thesis: ( ( len p = 1 & a is Polynomial of n,L & b is Polynomial of n,L ) or ( len p <> 1 & a is Polynomial of n,L & b is Polynomial of n,L ) )
per cases ( len p = 1 or len p <> 1 ) ;
case len p = 1 ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A5, A6, A7; :: thesis: verum
end;
case A10: len p <> 1 ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
then 0 + 1 < l + 1 by ;
then A11: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg (len p) by ;
then l in dom p by FINSEQ_1:def 3;
then A12: [(p . l),b] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by ;
A13: now :: thesis: ( ( [(p . l),b] in PolyRedRel (P,T) & b is Polynomial of n,L ) or ( [(p . l),b] in (PolyRedRel (P,T)) ~ & b is Polynomial of n,L ) )
per cases ( [(p . l),b] in PolyRedRel (P,T) or [(p . l),b] in (PolyRedRel (P,T)) ~ ) by ;
case [(p . l),b] in PolyRedRel (P,T) ; :: thesis: b is Polynomial of n,L
then consider h9, b9 being object such that
A14: [(p . l),b] = [h9,b9] and
h9 in NonZero (Polynom-Ring (n,L)) and
A15: b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
b = b9 by ;
hence b is Polynomial of n,L by ; :: thesis: verum
end;
case [(p . l),b] in (PolyRedRel (P,T)) ~ ; :: thesis: b is Polynomial of n,L
then [b,(p . l)] in PolyRedRel (P,T) by RELAT_1:def 7;
then consider h9, b9 being object such that
A16: [b,(p . l)] = [h9,b9] and
A17: h9 in NonZero (Polynom-Ring (n,L)) and
b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
b = h9 by ;
hence b is Polynomial of n,L by ; :: thesis: verum
end;
end;
end;
1 < len p by ;
then 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg (len p) by FINSEQ_1:1;
then A18: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg (len p) by ;
then 1 in dom p by FINSEQ_1:def 3;
then A19: [a,(p . (1 + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by ;
now :: thesis: ( ( [a,(p . (1 + 1))] in PolyRedRel (P,T) & a is Polynomial of n,L ) or ( [a,(p . (1 + 1))] in (PolyRedRel (P,T)) ~ & a is Polynomial of n,L ) )
per cases ( [a,(p . (1 + 1))] in PolyRedRel (P,T) or [a,(p . (1 + 1))] in (PolyRedRel (P,T)) ~ ) by ;
case [a,(p . (1 + 1))] in PolyRedRel (P,T) ; :: thesis: a is Polynomial of n,L
then consider h9, b9 being object such that
A20: [a,(p . (1 + 1))] = [h9,b9] and
A21: h9 in NonZero (Polynom-Ring (n,L)) and
b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
a = h9 by ;
hence a is Polynomial of n,L by ; :: thesis: verum
end;
case [a,(p . (1 + 1))] in (PolyRedRel (P,T)) ~ ; :: thesis: a is Polynomial of n,L
then [(p . (1 + 1)),a] in PolyRedRel (P,T) by RELAT_1:def 7;
then consider h9, b9 being object such that
A22: [(p . (1 + 1)),a] = [h9,b9] and
h9 in NonZero (Polynom-Ring (n,L)) and
A23: b9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
a = b9 by ;
hence a is Polynomial of n,L by ; :: thesis: verum
end;
end;
end;
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A13; :: thesis: verum
end;
end;
end;
then reconsider a9 = a, b9 = b as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;
G -Ideal = P -Ideal by ;
then a9,b9 are_congruent_mod G -Ideal by ;
then a9,b9 are_convertible_wrt RG by POLYRED:58;
hence a,b are_convergent_wrt RG by REWRITE1:def 23; :: thesis: verum
end;
end;
end;
hence a,b are_convergent_wrt RG ; :: thesis: verum
end;
now :: thesis: ( a,b are_convergent_wrt RG implies a,b are_convertible_wrt PolyRedRel (P,T) )
assume A24: a,b are_convergent_wrt RG ; :: thesis: a,b are_convertible_wrt PolyRedRel (P,T)
now :: thesis: ( ( a = b & a,b are_convertible_wrt PolyRedRel (P,T) ) or ( a <> b & a,b are_convertible_wrt PolyRedRel (P,T) ) )
per cases ( a = b or a <> b ) ;
case A25: a <> b ; :: thesis: a,b are_convertible_wrt PolyRedRel (P,T)
consider c being object such that
A26: RG reduces a,c and
A27: RG reduces b,c by ;
( a is Polynomial of n,L & b is Polynomial of n,L )
proof
now :: thesis: ( ( a = c & a is Polynomial of n,L & b is Polynomial of n,L ) or ( a <> c & a is Polynomial of n,L & b is Polynomial of n,L ) )
per cases ( a = c or a <> c ) ;
case a = c ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by ; :: thesis: verum
end;
case A28: a <> c ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
now :: thesis: ( ( b = c & a is Polynomial of n,L & b is Polynomial of n,L ) or ( b <> c & b is Polynomial of n,L ) )
per cases ( b = c or b <> c ) ;
case b = c ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by ; :: thesis: verum
end;
case b <> c ; :: thesis: b is Polynomial of n,L
hence b is Polynomial of n,L by ; :: thesis: verum
end;
end;
end;
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by ; :: thesis: verum
end;
end;
end;
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) ; :: thesis: verum
end;
then reconsider a9 = a, b9 = b as Element of the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;
( G -Ideal = P -Ideal & a9,b9 are_convertible_wrt RG ) by ;
then a9,b9 are_congruent_mod P -Ideal by POLYRED:57;
hence a,b are_convertible_wrt PolyRedRel (P,T) by POLYRED:58; :: thesis: verum
end;
end;
end;
hence a,b are_convertible_wrt PolyRedRel (P,T) ; :: thesis: verum
end;
hence ( a,b are_convertible_wrt PolyRedRel (P,T) iff a,b are_convergent_wrt RG ) by A3; :: thesis: verum
end;
hence PolyRedRel (G,T) is Completion of PolyRedRel (P,T) by REWRITE1:def 28; :: thesis: verum