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 )

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

hence
PolyRedRel (G,T) is Completion of PolyRedRel (P,T)
by REWRITE1:def 28; :: thesis: verum
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;

end;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

end;now :: thesis: ( ( a = b & a,b are_convergent_wrt RG ) or ( a <> b & a,b are_convergent_wrt RG ) )end;

hence
a,b are_convergent_wrt RG
; :: thesis: verumper cases
( a = b or a <> b )
;

end;

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 and

A7: p . (len p) = b by REWRITE1:def 3;

reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;

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;

reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;

G -Ideal = P -Ideal by A2, IDEAL_1:44;

then a9,b9 are_congruent_mod G -Ideal by A4, POLYRED:57;

then a9,b9 are_convertible_wrt RG by POLYRED:58;

hence a,b are_convergent_wrt RG by REWRITE1:def 23; :: thesis: verum

end;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 INT_1:5, NAT_1:14;

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 ) )end;

then reconsider a9 = a, b9 = b as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;per cases
( len p = 1 or len p <> 1 )
;

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 A8, XXREAL_0:1;

then A11: 1 <= l by NAT_1:13;

l <= l + 1 by NAT_1:13;

then l in Seg (len p) by A11, FINSEQ_1:1;

then l in dom p by FINSEQ_1:def 3;

then A12: [(p . l),b] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A7, A9, REWRITE1:def 2;

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 A8, FINSEQ_1:1;

then 1 in dom p by FINSEQ_1:def 3;

then A19: [a,(p . (1 + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A6, A18, REWRITE1:def 2;

end;then A11: 1 <= l by NAT_1:13;

l <= l + 1 by NAT_1:13;

then l in Seg (len p) by A11, FINSEQ_1:1;

then l in dom p by FINSEQ_1:def 3;

then A12: [(p . l),b] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A7, A9, REWRITE1:def 2;

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 ) )end;

1 < len p
by A8, A10, XXREAL_0:1;per cases
( [(p . l),b] in PolyRedRel (P,T) or [(p . l),b] in (PolyRedRel (P,T)) ~ )
by A12, XBOOLE_0:def 3;

end;

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 A14, XTUPLE_0:1;

hence b is Polynomial of n,L by A15, POLYNOM1:def 11; :: thesis: verum

end;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 A14, XTUPLE_0:1;

hence b is Polynomial of n,L by A15, POLYNOM1:def 11; :: thesis: verum

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 A16, XTUPLE_0:1;

hence b is Polynomial of n,L by A17, POLYNOM1:def 11; :: thesis: verum

end;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 A16, XTUPLE_0:1;

hence b is Polynomial of n,L by A17, POLYNOM1:def 11; :: thesis: verum

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 A8, FINSEQ_1:1;

then 1 in dom p by FINSEQ_1:def 3;

then A19: [a,(p . (1 + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A6, A18, REWRITE1:def 2;

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 ) )end;

hence
( a is Polynomial of n,L & b is Polynomial of n,L )
by A13; :: thesis: verumper cases
( [a,(p . (1 + 1))] in PolyRedRel (P,T) or [a,(p . (1 + 1))] in (PolyRedRel (P,T)) ~ )
by A19, XBOOLE_0:def 3;

end;

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 A20, XTUPLE_0:1;

hence a is Polynomial of n,L by A21, POLYNOM1:def 11; :: thesis: verum

end;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 A20, XTUPLE_0:1;

hence a is Polynomial of n,L by A21, POLYNOM1:def 11; :: thesis: verum

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 A22, XTUPLE_0:1;

hence a is Polynomial of n,L by A23, POLYNOM1:def 11; :: thesis: verum

end;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 A22, XTUPLE_0:1;

hence a is Polynomial of n,L by A23, POLYNOM1:def 11; :: thesis: verum

reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;

G -Ideal = P -Ideal by A2, IDEAL_1:44;

then a9,b9 are_congruent_mod G -Ideal by A4, POLYRED:57;

then a9,b9 are_convertible_wrt RG by POLYRED:58;

hence a,b are_convergent_wrt RG by REWRITE1:def 23; :: thesis: verum

now :: thesis: ( a,b are_convergent_wrt RG implies a,b are_convertible_wrt PolyRedRel (P,T) )

hence
( a,b are_convertible_wrt PolyRedRel (P,T) iff a,b are_convergent_wrt RG )
by A3; :: thesis: verumassume A24:
a,b are_convergent_wrt RG
; :: thesis: a,b are_convertible_wrt PolyRedRel (P,T)

end;now :: thesis: ( ( a = b & a,b are_convertible_wrt PolyRedRel (P,T) ) or ( a <> b & a,b are_convertible_wrt PolyRedRel (P,T) ) )end;

hence
a,b are_convertible_wrt PolyRedRel (P,T)
; :: thesis: verumper cases
( a = b or a <> b )
;

end;

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 A24, REWRITE1:def 7;

( a is Polynomial of n,L & b is Polynomial of n,L )

reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;

( G -Ideal = P -Ideal & a9,b9 are_convertible_wrt RG ) by A2, A24, IDEAL_1:44, REWRITE1:37;

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;A26: RG reduces a,c and

A27: RG reduces b,c by A24, REWRITE1:def 7;

( a is Polynomial of n,L & b is Polynomial of n,L )

proof

end;

then reconsider a9 = a, b9 = b as Element of the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11;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 ) )end;

hence
( a is Polynomial of n,L & b is Polynomial of n,L )
; :: thesis: verumper cases
( a = c or a <> c )
;

end;

case A28:
a <> c
; :: thesis: ( a is Polynomial of n,L & b is Polynomial of n,L )

end;

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 ) )end;

hence
( a is Polynomial of n,L & b is Polynomial of n,L )
by A26, A28, Lm6; :: thesis: verumper cases
( b = c or b <> c )
;

end;

reconsider a9 = a9, b9 = b9 as Element of (Polynom-Ring (n,L)) ;

( G -Ideal = P -Ideal & a9,b9 are_convertible_wrt RG ) by A2, A24, IDEAL_1:44, REWRITE1:37;

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