MAYBE Rewrite Rules: [ +(0,?x) -> ?x, +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Apply Direct Methods... Inner CPs: [ +(?x_1,?x) = +(+(?x_1,0),?x), +(?x_1,+(?x_2,+(?y_2,?z_2))) = +(+(?x_1,+(?x_2,?y_2)),?z_2), +(?x,?z_2) = +(0,+(?x,?z_2)), +(+(+(?x_1,?y_1),?z_1),?z_2) = +(?x_1,+(+(?y_1,?z_1),?z_2)), +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)), +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ] Outer CPs: [ +(?y_1,?z_1) = +(+(0,?y_1),?z_1), +(+(+(?x_2,?y_2),?y_1),?z_1) = +(?x_2,+(?y_2,+(?y_1,?z_1))) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ +(+(0,?y_1),?z_1) = +(?y_1,?z_1), +(+(?x_2,0),?x) = +(?x_2,?x), +(0,+(?x,?z_3)) = +(?x,?z_3), +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)), ?z = +(+(0,0),?z), +(?x_3,+(?y_3,?z)) = +(+(0,+(?x_3,?y_3)),?z), +(?x_2,+(?y_2,+(+(?y,?y_3),?z_3))) = +(+(+(?x_2,?y_2),?y),+(?y_3,?z_3)), +(?x_2,+(?y_2,?z)) = +(+(+(?x_2,?y_2),0),?z), +(?x_2,+(?y_2,+(?x_5,+(?y_5,?z)))) = +(+(+(?x_2,?y_2),+(?x_5,?y_5)),?z), +(?y,?z) = +(+(0,?y),?z), +(?x_2,+(?y_2,+(?y,?z))) = +(+(+(?x_2,?y_2),?y),?z), +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)), +(?x,?z) = +(+(?x,0),?z), +(?x,+(?x_3,+(?y_3,?z))) = +(+(?x,+(?x_3,?y_3)),?z), +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))), +(+(?x_1,?x),?z) = +(?x_1,+(+(?x,0),?z)), +(+(?x_1,?x),+(?x_4,+(?y_4,?z))) = +(?x_1,+(+(?x,+(?x_4,?y_4)),?z)), +(?x,+(+(+(?y,?y_4),?z_4),?z_3)) = +(+(+(?x,?y),+(?y_4,?z_4)),?z_3), +(?x,+(?z,?z_3)) = +(+(+(?x,0),?z),?z_3), +(?x,+(+(?x_6,+(?y_6,?z)),?z_3)) = +(+(+(?x,+(?x_6,?y_6)),?z),?z_3), +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)), +(?x,+(+(?y,?z),?z_3)) = +(+(+(?x,?y),?z),?z_3), +(+(+(?x_3,+(?y_3,?y)),?y_2),?z_2) = +(+(?x_3,?y_3),+(?y,+(?y_2,?z_2))), +(+(?y,?y_2),?z_2) = +(0,+(?y,+(?y_2,?z_2))), +(+(+(+(?x,?y_5),?z_5),?y_2),?z_2) = +(?x,+(+(?y_5,?z_5),+(?y_2,?z_2))), +(+(+(?x,?y),?y_2),?z_2) = +(?x,+(?y,+(?y_2,?z_2))), +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)), +(?y,?z) = +(0,+(?y,?z)), +(+(+(?x,?y_3),?z_3),?z) = +(?x,+(+(?y_3,?z_3),?z)), +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1), +(+(+(?x,?y_4),?z_4),+(?z,?z_1)) = +(+(?x,+(+(?y_4,?z_4),?z)),?z_1), +(+(?x_3,+(?x_4,+(?y_4,?y))),?z) = +(?x_3,+(+(?x_4,?y_4),+(?y,?z))), +(+(?x_3,?y),?z) = +(?x_3,+(0,+(?y,?z))), +(+(?x_3,+(+(?x,?y_6),?z_6)),?z) = +(?x_3,+(?x,+(+(?y_6,?z_6),?z))), +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1), +(+(?x_3,+(?x,?y)),?z) = +(?x_3,+(?x,+(?y,?z))) ] 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 <+(?x_1,?x), +(+(?x_1,0),?x)> by Rules <0, 1> preceded by [(+,2)] joinable by a reduction of rules <[], [([],2),([(+,2)],0)]> Critical Pair <+(?x_1,+(?x_2,+(?y_2,?z_2))), +(+(?x_1,+(?x_2,?y_2)),?z_2)> by Rules <2, 1> preceded by [(+,2)] joinable by a reduction of rules <[([(+,2)],1)], [([],2)]> Critical Pair <+(?x,?z_2), +(0,+(?x,?z_2))> by Rules <0, 2> preceded by [(+,1)] joinable by a reduction of rules <[], [([],0)]> Critical Pair <+(+(+(?x_1,?y_1),?z_1),?z_2), +(?x_1,+(+(?y_1,?z_1),?z_2))> by Rules <1, 2> preceded by [(+,1)] joinable by a reduction of rules <[([(+,1)],2)], [([],1)]> Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <1, 1> preceded by [(+,2)] joinable by a reduction of rules <[([(+,2)],2)], [([],2)]> Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <2, 2> preceded by [(+,1)] joinable by a reduction of rules <[([(+,1)],1)], [([],1)]> Critical Pair <+(+(0,?y_1),?z_1), +(?y_1,?z_1)> by Rules <1, 0> preceded by [] joinable by a reduction of rules <[([(+,1)],0)], []> Critical Pair <+(?x_2,+(?y_2,+(?y_1,?z_1))), +(+(+(?x_2,?y_2),?y_1),?z_1)> by Rules <2, 1> preceded by [] joinable by a reduction of rules <[([],1)], [([],2)]> unknown Diagram Decreasing check Non-Confluence... obtain 13 rules by 3 steps unfolding strenghten +(0,?x) and ?x strenghten +(+(0,0),?x_11) and ?x_11 strenghten +(0,+(0,?x_4)) and ?x_4 strenghten +(+(?x_1,0),?x) and +(?x_1,?x) strenghten +(+(0,?y_1),?z_1) and +(?y_1,?z_1) strenghten +(0,+(?x,?z_2)) and +(?x,?z_2) strenghten +(+(?x_1,+(0,0)),?x_4) and +(?x_1,?x_4) strenghten +(+(?x_1,0),+(0,?x_11)) and +(?x_1,?x_11) strenghten +(+(+(0,0),?y_1),?z_1) and +(?y_1,?z_1) strenghten +(+(0,0),+(?x_4,?z_2)) and +(?x_4,?z_2) strenghten +(0,+(+(0,?x_11),?z_2)) and +(?x_11,?z_2) strenghten +(?x_1,+(+(?y_1,?z_1),?z_2)) and +(+(+(?x_1,?y_1),?z_1),?z_2) strenghten +(+(?x,?y),+(?z,?z_1)) and +(+(?x,+(?y,?z)),?z_1) strenghten +(+(?x_1,?x),+(?y,?z)) and +(?x_1,+(+(?x,?y),?z)) strenghten +(+(?x_1,+(?x_2,?y_2)),?z_2) and +(?x_1,+(?x_2,+(?y_2,?z_2))) strenghten +(+(+(?x_2,?y_2),?y_1),?z_1) and +(?x_2,+(?y_2,+(?y_1,?z_1))) obtain 37 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Root-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 unknown Huet (modulo AC) check by Reduction-Preserving Completion... STEP: 1 (parallel) S: [ +(0,?x) -> ?x ] P: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] S: terminating CP(S,S): PCP_in(symP,S): CP(S,symP): <+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes <+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no check joinability condition: check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable failed failure(Step 1) [ ] Added S-Rules: [ ] Added P-Rules: [ ] STEP: 2 (linear) S: [ +(0,?x) -> ?x ] P: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] S: terminating CP(S,S): CP_in(symP,S): CP(S,symP): <+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes <+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no check joinability condition: check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable failed failure(Step 2) [ ] Added S-Rules: [ ] Added P-Rules: [ ] STEP: 3 (relative) S: [ +(0,?x) -> ?x ] P: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Check relative termination: [ +(0,?x) -> ?x ] [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Polynomial Interpretation: +:= (1)+(1)*x1+(1)*x2 0:= 0 relatively terminating S/P: relatively terminating check CP condition: failed failure(Step 3) failure(no possibility remains) unknown Reduction-Preserving Completion Direct Methods: Can't judge Try Persistent Decomposition for... [ +(0,?x) -> ?x, +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Sort Assignment: + : 12*12=>12 0 : =>12 maximal types: {12} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ +(0,?x) -> ?x, +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ +(0,?x) -> ?x, +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Outside Critical Pair: <+(+(0,?y_1),?z_1), +(?y_1,?z_1)> by Rules <1, 0> develop reducts from lhs term... <{2}, +(0,+(?y_1,?z_1))> <{0}, +(?y_1,?z_1)> <{}, +(+(0,?y_1),?z_1)> develop reducts from rhs term... <{}, +(?y_1,?z_1)> Outside Critical Pair: <+(?x_2,+(?y_2,+(?y_1,?z_1))), +(+(+(?x_2,?y_2),?y_1),?z_1)> by Rules <2, 1> develop reducts from lhs term... <{1}, +(+(?x_2,?y_2),+(?y_1,?z_1))> <{1}, +(?x_2,+(+(?y_2,?y_1),?z_1))> <{}, +(?x_2,+(?y_2,+(?y_1,?z_1)))> develop reducts from rhs term... <{2}, +(+(?x_2,?y_2),+(?y_1,?z_1))> <{2}, +(+(?x_2,+(?y_2,?y_1)),?z_1)> <{}, +(+(+(?x_2,?y_2),?y_1),?z_1)> Inside Critical Pair: <+(?x_1,?x), +(+(?x_1,0),?x)> by Rules <0, 1> develop reducts from lhs term... <{}, +(?x_1,?x)> develop reducts from rhs term... <{2}, +(?x_1,+(0,?x))> <{}, +(+(?x_1,0),?x)> Inside Critical Pair: <+(?x_1,+(?x_2,+(?y_2,?z_2))), +(+(?x_1,+(?x_2,?y_2)),?z_2)> by Rules <2, 1> develop reducts from lhs term... <{1}, +(+(?x_1,?x_2),+(?y_2,?z_2))> <{1}, +(?x_1,+(+(?x_2,?y_2),?z_2))> <{}, +(?x_1,+(?x_2,+(?y_2,?z_2)))> develop reducts from rhs term... <{2}, +(?x_1,+(+(?x_2,?y_2),?z_2))> <{1}, +(+(+(?x_1,?x_2),?y_2),?z_2)> <{}, +(+(?x_1,+(?x_2,?y_2)),?z_2)> Inside Critical Pair: <+(?x,?z_2), +(0,+(?x,?z_2))> by Rules <0, 2> develop reducts from lhs term... <{}, +(?x,?z_2)> develop reducts from rhs term... <{1}, +(+(0,?x),?z_2)> <{0}, +(?x,?z_2)> <{}, +(0,+(?x,?z_2))> Inside Critical Pair: <+(+(+(?x_1,?y_1),?z_1),?z_2), +(?x_1,+(+(?y_1,?z_1),?z_2))> by Rules <1, 2> develop reducts from lhs term... <{2}, +(+(?x_1,?y_1),+(?z_1,?z_2))> <{2}, +(+(?x_1,+(?y_1,?z_1)),?z_2)> <{}, +(+(+(?x_1,?y_1),?z_1),?z_2)> develop reducts from rhs term... <{1}, +(+(?x_1,+(?y_1,?z_1)),?z_2)> <{2}, +(?x_1,+(?y_1,+(?z_1,?z_2)))> <{}, +(?x_1,+(+(?y_1,?z_1),?z_2))> Try A Minimal Decomposition {0,1}{2} {0,1} (cm)Rewrite Rules: [ +(0,?x) -> ?x, +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ] Apply Direct Methods... Inner CPs: [ +(?x_1,?x) = +(+(?x_1,0),?x), +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)) ] Outer CPs: [ +(?y_1,?z_1) = +(+(0,?y_1),?z_1) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2} (cm)Rewrite Rules: [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Apply Direct Methods... Inner CPs: [ +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge R1.trs: Failure(unknown) (3814 msec.)