NO Rewrite Rules: [ size(leaf) -> s(0), size(node(?x,?y)) -> +(size(?y),size(?x)), +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?x,?y)), +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?x,?y)), node(?x,?y) -> node(?y,?x) ] Apply Direct Methods... Inner CPs: [ size(node(?y_5,?x_5)) = +(size(?y_5),size(?x_5)) ] Outer CPs: [ 0 = 0, s(?y_4) = s(+(0,?y_4)), s(+(?x_2,0)) = s(?x_2), s(+(?x_2,s(?y_4))) = s(+(s(?x_2),?y_4)) ] 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: [ size(node(?y,?x)) = +(size(?y),size(?x)), 0 = 0, s(+(0,?y_4)) = s(?y_4), s(?x) = s(+(?x,0)), s(+(s(?x),?y_4)) = s(+(?x,s(?y_4))), s(+(?x_3,0)) = s(?x_3), s(?y) = s(+(0,?y)), s(+(?x_3,s(?y))) = s(+(s(?x_3),?y)), +(size(?y),size(?x)) = size(node(?y,?x)) ] 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 by Rules <6, 1> preceded by [(size,1)] joinable by a reduction of rules <[([(size,1)],6),([],1)], []> Critical Pair <0, 0> by Rules <4, 2> preceded by [] joinable by a reduction of rules <[], []> Critical Pair by Rules <5, 2> preceded by [] joinable by a reduction of rules <[([(s,1)],2)], []> Critical Pair by Rules <4, 3> preceded by [] joinable by a reduction of rules <[], [([(s,1)],4)]> Critical Pair by Rules <5, 3> preceded by [] joinable by a reduction of rules <[([(s,1)],3)], [([(s,1)],5)]> unknown Diagram Decreasing check Non-Confluence... obtain 10 rules by 3 steps unfolding obtain 15 candidates for checking non-joinability check by TCAP-Approximation [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] [ size(leaf) -> s(0), size(node(?x:Tree,?y:Tree)) -> +(size(?y:Tree),size(?x:Tree)), +(0,?y:Nat) -> ?y:Nat, +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)), +(?x:Nat,0) -> ?x:Nat, +(?x:Nat,s(?y:Nat)) -> s(+(?x:Nat,?y:Nat)), node(?x:Tree,?y:Tree) -> node(?y:Tree,?x:Tree) ] (success) Witness for Non-Confluence: <+(size(c_2),size(c_1)) <- size(node(c_1,c_2)) -> +(size(c_1),size(c_2))> Direct Methods: not CR Final result: not CR new/tree2.trs: Success(not CR) (26 msec.)