let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

set I = {(0_ (n,L))};

set G = {(0_ (n,L))};

set R = PolyRedRel ({(0_ (n,L))},T);

A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

then {(0_ (n,L))} -Ideal = {(0_ (n,L))} by IDEAL_1:44;

hence {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T by A8; :: thesis: verum

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

set I = {(0_ (n,L))};

set G = {(0_ (n,L))};

set R = PolyRedRel ({(0_ (n,L))},T);

A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

now :: thesis: for a, b, c being object st [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) holds

b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

then A8:
PolyRedRel ({(0_ (n,L))},T) is locally-confluent
by REWRITE1:def 24;b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

let a, b, c be object ; :: thesis: ( [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) implies b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) )

assume that

A2: [a,b] in PolyRedRel ({(0_ (n,L))},T) and

[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis: b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

consider p, q being object such that

A3: p in NonZero (Polynom-Ring (n,L)) and

A4: q in the carrier of (Polynom-Ring (n,L)) and

A5: [a,b] = [p,q] by A2, ZFMISC_1:def 2;

reconsider q = q as Polynomial of n,L by A4, POLYNOM1:def 11;

not p in {(0_ (n,L))} by A1, A3, XBOOLE_0:def 5;

then p <> 0_ (n,L) by TARSKI:def 1;

then reconsider p = p as non-zero Polynomial of n,L by A3, POLYNOM1:def 11, POLYNOM7:def 1;

p reduces_to q,{(0_ (n,L))},T by A2, A5, POLYRED:def 13;

then consider g being Polynomial of n,L such that

A6: g in {(0_ (n,L))} and

A7: p reduces_to q,g,T by POLYRED:def 7;

g = 0_ (n,L) by A6, TARSKI:def 1;

then p is_reducible_wrt 0_ (n,L),T by A7, POLYRED:def 8;

hence b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) by Lm3; :: thesis: verum

end;assume that

A2: [a,b] in PolyRedRel ({(0_ (n,L))},T) and

[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis: b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

consider p, q being object such that

A3: p in NonZero (Polynom-Ring (n,L)) and

A4: q in the carrier of (Polynom-Ring (n,L)) and

A5: [a,b] = [p,q] by A2, ZFMISC_1:def 2;

reconsider q = q as Polynomial of n,L by A4, POLYNOM1:def 11;

not p in {(0_ (n,L))} by A1, A3, XBOOLE_0:def 5;

then p <> 0_ (n,L) by TARSKI:def 1;

then reconsider p = p as non-zero Polynomial of n,L by A3, POLYNOM1:def 11, POLYNOM7:def 1;

p reduces_to q,{(0_ (n,L))},T by A2, A5, POLYRED:def 13;

then consider g being Polynomial of n,L such that

A6: g in {(0_ (n,L))} and

A7: p reduces_to q,g,T by POLYRED:def 7;

g = 0_ (n,L) by A6, TARSKI:def 1;

then p is_reducible_wrt 0_ (n,L),T by A7, POLYRED:def 8;

hence b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) by Lm3; :: thesis: verum

0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

then {(0_ (n,L))} -Ideal = {(0_ (n,L))} by IDEAL_1:44;

hence {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T by A8; :: thesis: verum