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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 by Def4;
then PolyRedRel G,T is confluent ;
then reconsider RG = PolyRedRel G,T as complete Relation ;
for a, b being set holds
( a,b are_convertible_wrt PolyRedRel P,T iff a,b are_convergent_wrt RG )
proof
let a, b be set ; :: thesis: ( a,b are_convertible_wrt PolyRedRel P,T iff a,b are_convergent_wrt RG )
A2: G -Ideal = P by A1, Def4;
A3: now
assume A4: a,b are_convertible_wrt PolyRedRel P,T ; :: thesis: a,b are_convergent_wrt RG
now
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 A4, REWRITE1:def 4;
then consider p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) such that
A6: ( p . 1 = a & p . (len p) = b ) by REWRITE1:def 3;
A8: 1 <= len p by NAT_1:14;
reconsider l = (len p) - 1 as Element of NAT by INT_1:18, NAT_1:14;
( 1 <= l + 1 & l + 1 <= len p ) by NAT_1:12;
then l + 1 in Seg (len p) by FINSEQ_1:3;
then A9: l + 1 in dom p by FINSEQ_1:def 3;
set h = p . l;
set g = p . (1 + 1);
now
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; :: thesis: verum
end;
case A10: len p <> 1 ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
then A11: 1 < len p by A8, XXREAL_0:1;
0 + 1 < l + 1 by A8, A10, XXREAL_0:1;
then ( 1 <= l & l <= l + 1 ) by NAT_1:13;
then l in Seg (len p) by FINSEQ_1:3;
then l in dom p by FINSEQ_1:def 3;
then A12: [(p . l),b] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A6, A9, REWRITE1:def 2;
A13: now
per cases ( [(p . l),b] in PolyRedRel P,T or [(p . l),b] in (PolyRedRel P,T) ~ ) by A12, XBOOLE_0:def 3;
case [(p . l),b] in PolyRedRel P,T ; :: thesis: b is Polynomial of n,L
then consider h', b' being set such that
A14: ( [(p . l),b] = [h',b'] & h' in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & b' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
b = [h',b'] `2 by A14, MCART_1:def 2
.= b' by MCART_1:def 2 ;
hence b is Polynomial of n,L by A14, POLYNOM1:def 27; :: 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 h', b' being set such that
A15: ( [b,(p . l)] = [h',b'] & h' in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & b' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
b = [h',b'] `1 by A15, MCART_1:def 1
.= h' by MCART_1:def 1 ;
hence b is Polynomial of n,L by A15, POLYNOM1:def 27; :: thesis: verum
end;
end;
end;
1 in Seg (len p) by A8, FINSEQ_1:3;
then A16: 1 in dom p by FINSEQ_1:def 3;
( 1 <= 1 + 1 & 1 + 1 <= len p ) by A11, NAT_1:13;
then 1 + 1 in Seg (len p) by FINSEQ_1:3;
then 1 + 1 in dom p by FINSEQ_1:def 3;
then A17: [a,(p . (1 + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A6, A16, REWRITE1:def 2;
now
per cases ( [a,(p . (1 + 1))] in PolyRedRel P,T or [a,(p . (1 + 1))] in (PolyRedRel P,T) ~ ) by A17, XBOOLE_0:def 3;
case [a,(p . (1 + 1))] in PolyRedRel P,T ; :: thesis: a is Polynomial of n,L
then consider h', b' being set such that
A18: ( [a,(p . (1 + 1))] = [h',b'] & h' in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & b' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
a = [h',b'] `1 by A18, MCART_1:def 1
.= h' by MCART_1:def 1 ;
hence a is Polynomial of n,L by A18, POLYNOM1:def 27; :: 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 h', b' being set such that
A19: ( [(p . (1 + 1)),a] = [h',b'] & h' in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & b' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
a = [h',b'] `2 by A19, MCART_1:def 2
.= b' by MCART_1:def 2 ;
hence a is Polynomial of n,L by A19, POLYNOM1:def 27; :: 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 a' = a, b' = b as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider a' = a', b' = b' as Element of (Polynom-Ring n,L) ;
G -Ideal = P -Ideal by A2, IDEAL_1:44;
then a',b' are_congruent_mod G -Ideal by A4, POLYRED:57;
then a',b' 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
assume A20: a,b are_convergent_wrt RG ; :: thesis: a,b are_convertible_wrt PolyRedRel P,T
now
per cases ( a = b or a <> b ) ;
case A21: a <> b ; :: thesis: a,b are_convertible_wrt PolyRedRel P,T
consider c being set such that
A22: ( RG reduces a,c & RG reduces b,c ) by A20, REWRITE1:def 7;
( a is Polynomial of n,L & b is Polynomial of n,L )
proof
now
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 A21, A22, Lm6; :: thesis: verum
end;
case A23: a <> c ; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )
now
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 A21, A22, Lm6; :: thesis: verum
end;
case b <> c ; :: thesis: b is Polynomial of n,L
hence b is Polynomial of n,L by A22, Lm6; :: thesis: verum
end;
end;
end;
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) by A22, A23, Lm6; :: thesis: verum
end;
end;
end;
hence ( a is Polynomial of n,L & b is Polynomial of n,L ) ; :: thesis: verum
end;
then reconsider a' = a, b' = b as Element of the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider a' = a', b' = b' as Element of (Polynom-Ring n,L) ;
A24: G -Ideal = P -Ideal by A2, IDEAL_1:44;
a',b' are_convertible_wrt RG by A20, REWRITE1:38;
then a',b' are_congruent_mod P -Ideal by A24, 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