let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convertible_wrt PolyRedRel (P,T)
let T be connected 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
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convertible_wrt PolyRedRel (P,T)
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convertible_wrt PolyRedRel (P,T)
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convertible_wrt PolyRedRel (P,T)
let f, g be Polynomial of n,L; :: thesis: ( PolyRedRel (P,T) reduces f - g, 0_ (n,L) implies f,g are_convertible_wrt PolyRedRel (P,T) )
set R = PolyRedRel (P,T);
assume PolyRedRel (P,T) reduces f - g, 0_ (n,L) ; :: thesis: f,g are_convertible_wrt PolyRedRel (P,T)
then f,g are_convergent_wrt PolyRedRel (P,T) by Th50;
then consider h being object such that
A1: PolyRedRel (P,T) reduces f,h and
A2: PolyRedRel (P,T) reduces g,h by REWRITE1:def 7;
(PolyRedRel (P,T)) ~ reduces h,g by A2, REWRITE1:24;
then A3: (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces h,g by REWRITE1:22, XBOOLE_1:7;
(PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces f,h by A1, REWRITE1:22, XBOOLE_1:7;
then (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces f,g by A3, REWRITE1:16;
hence f,g are_convertible_wrt PolyRedRel (P,T) by REWRITE1:def 4; :: thesis: verum