let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 set 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:25;
then A3: (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces h,g by REWRITE1:23, XBOOLE_1:7;
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,h by A1, REWRITE1:23, XBOOLE_1:7;
then (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g by A3, REWRITE1:17;
hence f,g are_convertible_wrt PolyRedRel P,T by REWRITE1:def 4; :: thesis: verum