YES (ignored inputs)COMMENT the following rules are removed from the original TRS dbl ( x ) -> + ( x , x ) Rewrite Rules: [ +(?x,?y) -> +(?y,?x), +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?x,?y)), +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?x,?y)), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Apply Direct Methods... Inner CPs: [ +(+(?y,?x),?z_5) = +(?x,+(?y,?z_5)), +(?x_1,?z_5) = +(?x_1,+(0,?z_5)), +(s(+(?x_2,?y_2)),?z_5) = +(?x_2,+(s(?y_2),?z_5)), +(?y_3,?z_5) = +(0,+(?y_3,?z_5)), +(s(+(?x_4,?y_4)),?z_5) = +(s(?x_4),+(?y_4,?z_5)), +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ] Outer CPs: [ +(0,?x) = ?x, +(s(?y_2),?x) = s(+(?x,?y_2)), +(?y,0) = ?y, +(?y,s(?x_4)) = s(+(?x_4,?y)), +(?y,+(?x_5,?y_5)) = +(?x_5,+(?y_5,?y)), 0 = 0, s(?x_4) = s(+(?x_4,0)), +(?x_5,?y_5) = +(?x_5,+(?y_5,0)), s(+(0,?y_2)) = s(?y_2), s(+(s(?x_4),?y_2)) = s(+(?x_4,s(?y_2))), s(+(+(?x_5,?y_5),?y_2)) = +(?x_5,+(?y_5,s(?y_2))) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ ?x = +(0,?x), s(+(?x,?y_2)) = +(s(?y_2),?x), ?y = +(?y,0), s(+(?x_4,?y)) = +(?y,s(?x_4)), +(?x_5,+(?y_5,?y)) = +(?y,+(?x_5,?y_5)), +(?x,+(?y,?z_6)) = +(+(?y,?x),?z_6), +(0,?x) = ?x, 0 = 0, s(+(?x_4,0)) = s(?x_4), +(?x_5,+(?y_5,0)) = +(?x_5,?y_5), +(?x,+(0,?z_6)) = +(?x,?z_6), +(s(?y),?x) = s(+(?x,?y)), s(?y) = s(+(0,?y)), s(+(?x_4,s(?y))) = s(+(s(?x_4),?y)), +(?x_5,+(?y_5,s(?y))) = s(+(+(?x_5,?y_5),?y)), +(?x,+(s(?y),?z_6)) = +(s(+(?x,?y)),?z_6), +(?y,0) = ?y, s(+(0,?y_3)) = s(?y_3), +(0,+(?y,?z_6)) = +(?y,?z_6), +(?y,s(?x)) = s(+(?x,?y)), s(?x) = s(+(?x,0)), s(+(s(?x),?y_3)) = s(+(?x,s(?y_3))), +(s(?x),+(?y,?z_6)) = +(s(+(?x,?y)),?z_6), +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)), +(?z,+(?y,?x)) = +(?x,+(?y,?z)), +(?z,?x) = +(?x,+(0,?z)), +(?z,s(+(?x,?y_4))) = +(?x,+(s(?y_4),?z)), +(?z,?y) = +(0,+(?y,?z)), +(?z,s(+(?x_6,?y))) = +(s(?x_6),+(?y,?z)), +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)), +(?y,?x) = +(?x,+(?y,0)), ?x = +(?x,+(0,0)), s(+(?x,?y_4)) = +(?x,+(s(?y_4),0)), ?y = +(0,+(?y,0)), s(+(?x_6,?y)) = +(s(?x_6),+(?y,0)), s(+(+(?x_4,+(?y_4,?y)),?y_3)) = +(+(?x_4,?y_4),+(?y,s(?y_3))), s(+(+(?y,?x),?y_3)) = +(?x,+(?y,s(?y_3))), s(+(?x,?y_3)) = +(?x,+(0,s(?y_3))), s(+(s(+(?x,?y_7)),?y_3)) = +(?x,+(s(?y_7),s(?y_3))), s(+(?y,?y_3)) = +(0,+(?y,s(?y_3))), s(+(s(+(?x_9,?y)),?y_3)) = +(s(?x_9),+(?y,s(?y_3))), +(?z,+(?x,?y)) = +(?x,+(?y,?z)), +(?x,?y) = +(?x,+(?y,0)), s(+(+(?x,?y),?y_3)) = +(?x,+(?y,s(?y_3))), +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)), +(+(?y,?x),?z) = +(?x,+(?y,?z)), +(?x,?z) = +(?x,+(0,?z)), +(s(+(?x,?y_4)),?z) = +(?x,+(s(?y_4),?z)), +(?y,?z) = +(0,+(?y,?z)), +(s(+(?x_6,?y)),?z) = +(s(?x_6),+(?y,?z)), +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1), +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1), +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1), +(s(+(?x,?y_5)),+(?z,?z_1)) = +(+(?x,+(s(?y_5),?z)),?z_1), +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1), +(s(+(?x_7,?y)),+(?z,?z_1)) = +(+(s(?x_7),+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1) ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair <+(+(?y,?x),?z_5), +(?x,+(?y,?z_5))> by Rules <0, 5> preceded by [(+,1)] joinable by a reduction of rules <[([(+,1)],0),([],5)], []> joinable by a reduction of rules <[([],5),([(+,2)],0)], [([],0),([],5)]> Critical Pair <+(?x_1,?z_5), +(?x_1,+(0,?z_5))> by Rules <1, 5> preceded by [(+,1)] joinable by a reduction of rules <[], [([(+,2)],3)]> Critical Pair <+(s(+(?x_2,?y_2)),?z_5), +(?x_2,+(s(?y_2),?z_5))> by Rules <2, 5> preceded by [(+,1)] joinable by a reduction of rules <[([],4),([(s,1)],5)], [([(+,2)],4),([],2)]> Critical Pair <+(?y_3,?z_5), +(0,+(?y_3,?z_5))> by Rules <3, 5> preceded by [(+,1)] joinable by a reduction of rules <[], [([],3)]> Critical Pair <+(s(+(?x_4,?y_4)),?z_5), +(s(?x_4),+(?y_4,?z_5))> by Rules <4, 5> preceded by [(+,1)] joinable by a reduction of rules <[([],4),([(s,1)],5)], [([],4)]> Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <5, 5> preceded by [(+,1)] joinable by a reduction of rules <[([],5),([(+,2)],5)], [([],5)]> Critical Pair by Rules <1, 0> preceded by [] joinable by a reduction of rules <[], [([],3)]> Critical Pair by Rules <2, 0> preceded by [] joinable by a reduction of rules <[([(s,1)],0)], [([],4)]> Critical Pair by Rules <3, 0> preceded by [] joinable by a reduction of rules <[], [([],1)]> Critical Pair by Rules <4, 0> preceded by [] joinable by a reduction of rules <[([(s,1)],0)], [([],2)]> Critical Pair <+(?x_5,+(?y_5,?z_5)), +(?z_5,+(?x_5,?y_5))> by Rules <5, 0> preceded by [] joinable by a reduction of rules <[], [([],0),([],5)]> Critical Pair <0, 0> by Rules <3, 1> preceded by [] joinable by a reduction of rules <[], []> Critical Pair by Rules <4, 1> preceded by [] joinable by a reduction of rules <[([(s,1)],1)], []> Critical Pair <+(?x_5,+(?y_5,0)), +(?x_5,?y_5)> by Rules <5, 1> preceded by [] joinable by a reduction of rules <[([(+,2)],1)], []> Critical Pair by Rules <3, 2> preceded by [] joinable by a reduction of rules <[], [([(s,1)],3)]> Critical Pair by Rules <4, 2> preceded by [] joinable by a reduction of rules <[([(s,1)],2)], [([(s,1)],4)]> Critical Pair <+(?x_5,+(?y_5,s(?y_2))), s(+(+(?x_5,?y_5),?y_2))> by Rules <5, 2> preceded by [] joinable by a reduction of rules <[([(+,2)],2),([],2)], [([(s,1)],5)]> unknown Diagram Decreasing check Non-Confluence... obtain 8 rules by 3 steps unfolding obtain 100 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (failure) unknown Non-Confluence Check relative termination: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?x,?y)), +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?x,?y)) ] [ +(?x,?y) -> +(?y,?x), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Polynomial Interpretation: +:= (1)*x1+(1)*x2 0:= (4) s:= (1)*x1 retract +(?x,0) -> ?x retract +(0,?y) -> ?y Polynomial Interpretation: +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2 0:= (8) s:= (4)+(2)*x1 relatively terminating Huet (modulo AC) Direct Methods: CR Combined result: CR /tmp/fileLP0yXx.trs: Success(CR) (1408 msec.)