(ignored inputs)COMMENT [117] Example 4.3.12 submitted by: Aart Middeldorp
Rewrite Rules:
   [ max(L(?x)) -> ?x,
     max(N(L(0),L(?y))) -> ?y,
     max(N(L(s(?x)),L(s(?y)))) -> s(max(N(L(?x),L(?y)))),
     max(N(L(?x),N(?y,?z))) -> max(N(L(?x),L(max(N(?y,?z))))),
     N(?x,N(?y,?z)) -> N(N(?x,?y),?z),
     N(N(?x,?y),?z) -> N(?x,N(?y,?z)),
     N(?x,?y) -> N(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ max(N(L(?y_1),L(0))) = ?y_1,
     max(N(L(s(?y_2)),L(s(?x_2)))) = s(max(N(L(?x_2),L(?y_2)))),
     max(N(N(L(?x_3),?y_4),?z_4)) = max(N(L(?x_3),L(max(N(?y_4,?z_4))))),
     max(N(L(?x_3),N(N(?x_4,?y_4),?z_4))) = max(N(L(?x_3),L(max(N(?x_4,N(?y_4,?z_4)))))),
     max(N(L(?x_3),N(?x_5,N(?y_5,?z_5)))) = max(N(L(?x_3),L(max(N(N(?x_5,?y_5),?z_5))))),
     max(N(N(?y_3,?z_3),L(?x_3))) = max(N(L(?x_3),L(max(N(?y_3,?z_3))))),
     max(N(L(?x_3),N(?y_6,?x_6))) = max(N(L(?x_3),L(max(N(?x_6,?y_6))))),
     N(?x_4,N(?x_5,N(?y_5,?z_5))) = N(N(?x_4,N(?x_5,?y_5)),?z_5),
     N(?x_4,N(?y_6,?x_6)) = N(N(?x_4,?x_6),?y_6),
     N(N(N(?x_4,?y_4),?z_4),?z_5) = N(?x_4,N(N(?y_4,?z_4),?z_5)),
     N(N(?y_6,?x_6),?z_5) = N(?x_6,N(?y_6,?z_5)),
     N(?x_1,N(N(?x,?y),?z)) = N(N(?x_1,?x),N(?y,?z)),
     N(N(?x,N(?y,?z)),?z_1) = N(N(?x,?y),N(?z,?z_1)) ]
Outer CPs:
   [ N(N(N(?x_5,?y_5),?y_4),?z_4) = N(?x_5,N(?y_5,N(?y_4,?z_4))),
     N(N(?x_4,?y_4),?z_4) = N(N(?y_4,?z_4),?x_4),
     N(?x_5,N(?y_5,?z_5)) = N(?z_5,N(?x_5,?y_5)) ]
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:
   [ max(N(L(?y),L(0))) = ?y,
     max(N(L(s(?y)),L(s(?x)))) = s(max(N(L(?x),L(?y)))),
     max(N(N(N(?y,?y_5),?z_5),L(?x))) = max(N(L(?x),L(max(N(?y,N(?y_5,?z_5)))))),
     max(N(N(?x_6,N(?y_6,?z)),L(?x))) = max(N(L(?x),L(max(N(N(?x_6,?y_6),?z))))),
     max(N(N(?z,?y),L(?x))) = max(N(L(?x),L(max(N(?y,?z))))),
     max(N(N(L(?x),?y),?z)) = max(N(L(?x),L(max(N(?y,?z))))),
     max(N(N(?y,?z),L(?x))) = max(N(L(?x),L(max(N(?y,?z))))),
     max(N(L(?x),N(N(?y,?y_5),?z_5))) = max(N(L(?x),L(max(N(?y,N(?y_5,?z_5)))))),
     max(N(L(?x),N(?x_6,N(?y_6,?z)))) = max(N(L(?x),L(max(N(N(?x_6,?y_6),?z))))),
     max(N(L(?x),N(?z,?y))) = max(N(L(?x),L(max(N(?y,?z))))),
     N(?x_5,N(?y_5,N(N(?y,?y_6),?z_6))) = N(N(N(?x_5,?y_5),?y),N(?y_6,?z_6)),
     N(?x_5,N(?y_5,N(?x_11,N(?y_11,?z)))) = N(N(N(?x_5,?y_5),N(?x_11,?y_11)),?z),
     N(?x_5,N(?y_5,N(?z,?y))) = N(N(N(?x_5,?y_5),?y),?z),
     N(N(N(?y,?y_1),?z_1),?x) = N(N(?x,?y),N(?y_1,?z_1)),
     N(N(?x_6,N(?y_6,?z)),?x) = N(N(?x,N(?x_6,?y_6)),?z),
     N(N(?z,?y),?x) = N(N(?x,?y),?z),
     N(?x_5,N(?y_5,N(?y,?z))) = N(N(N(?x_5,?y_5),?y),?z),
     N(N(?y,?z),?x) = N(N(?x,?y),?z),
     N(?x,N(N(?y,?y_1),?z_1)) = N(N(?x,?y),N(?y_1,?z_1)),
     N(?x,N(?x_6,N(?y_6,?z))) = N(N(?x,N(?x_6,?y_6)),?z),
     N(?x,N(?z,?y)) = N(N(?x,?y),?z),
     N(N(?x_1,?x),N(N(?y,?y_2),?z_2)) = N(?x_1,N(N(?x,?y),N(?y_2,?z_2))),
     N(N(?x_1,?x),N(?x_7,N(?y_7,?z))) = N(?x_1,N(N(?x,N(?x_7,?y_7)),?z)),
     N(N(?x_1,?x),N(?z,?y)) = N(?x_1,N(N(?x,?y),?z)),
     max(N(L(?x_5),L(max(N(?x,N(N(?y,?y_6),?z_6)))))) = max(N(L(?x_5),N(N(?x,?y),N(?y_6,?z_6)))),
     max(N(L(?x_5),L(max(N(?x,N(?x_11,N(?y_11,?z))))))) = max(N(L(?x_5),N(N(?x,N(?x_11,?y_11)),?z))),
     max(N(L(?x_5),L(max(N(?x,N(?z,?y)))))) = max(N(L(?x_5),N(N(?x,?y),?z))),
     N(?x,N(N(N(?y,?y_7),?z_7),?z_6)) = N(N(N(?x,?y),N(?y_7,?z_7)),?z_6),
     N(?x,N(N(?x_12,N(?y_12,?z)),?z_6)) = N(N(N(?x,N(?x_12,?y_12)),?z),?z_6),
     N(?x,N(N(?z,?y),?z_6)) = N(N(N(?x,?y),?z),?z_6),
     N(N(?x_1,?x),N(?y,?z)) = N(?x_1,N(N(?x,?y),?z)),
     max(N(L(?x_5),L(max(N(?y,?z))))) = max(N(N(L(?x_5),?y),?z)),
     max(N(L(?x_5),L(max(N(?x,N(?y,?z)))))) = max(N(L(?x_5),N(N(?x,?y),?z))),
     N(?x,N(N(?y,?z),?z_6)) = N(N(N(?x,?y),?z),?z_6),
     N(N(N(?x_6,N(?y_6,?y)),?y_5),?z_5) = N(N(?x_6,?y_6),N(?y,N(?y_5,?z_5))),
     N(N(N(N(?x,?y_11),?z_11),?y_5),?z_5) = N(?x,N(N(?y_11,?z_11),N(?y_5,?z_5))),
     N(N(N(?y,?x),?y_5),?z_5) = N(?x,N(?y,N(?y_5,?z_5))),
     N(?z,N(?x_1,N(?y_1,?y))) = N(N(?x_1,?y_1),N(?y,?z)),
     N(?z,N(N(?x,?y_6),?z_6)) = N(?x,N(N(?y_6,?z_6),?z)),
     N(?z,N(?y,?x)) = N(?x,N(?y,?z)),
     N(N(N(?x,?y),?y_5),?z_5) = N(?x,N(?y,N(?y_5,?z_5))),
     N(?z,N(?x,?y)) = N(?x,N(?y,?z)),
     N(N(?x_1,N(?y_1,?y)),?z) = N(N(?x_1,?y_1),N(?y,?z)),
     N(N(N(?x,?y_6),?z_6),?z) = N(?x,N(N(?y_6,?z_6),?z)),
     N(N(?y,?x),?z) = N(?x,N(?y,?z)),
     N(N(?x_2,N(?y_2,?y)),N(?z,?z_1)) = N(N(N(?x_2,?y_2),N(?y,?z)),?z_1),
     N(N(N(?x,?y_7),?z_7),N(?z,?z_1)) = N(N(?x,N(N(?y_7,?z_7),?z)),?z_1),
     N(N(?y,?x),N(?z,?z_1)) = N(N(?x,N(?y,?z)),?z_1),
     max(N(L(?x_5),L(max(N(N(?x_6,N(?y_6,?y)),?z))))) = max(N(L(?x_5),N(N(?x_6,?y_6),N(?y,?z)))),
     max(N(L(?x_5),L(max(N(N(N(?x,?y_11),?z_11),?z))))) = max(N(L(?x_5),N(?x,N(N(?y_11,?z_11),?z)))),
     max(N(L(?x_5),L(max(N(N(?y,?x),?z))))) = max(N(L(?x_5),N(?x,N(?y,?z)))),
     N(N(?x_6,N(?x_7,N(?y_7,?y))),?z) = N(?x_6,N(N(?x_7,?y_7),N(?y,?z))),
     N(N(?x_6,N(N(?x,?y_12),?z_12)),?z) = N(?x_6,N(?x,N(N(?y_12,?z_12),?z))),
     N(N(?x_6,N(?y,?x)),?z) = N(?x_6,N(?x,N(?y,?z))),
     N(N(?x,?y),N(?z,?z_1)) = N(N(?x,N(?y,?z)),?z_1),
     max(N(L(?x_5),L(max(N(N(?x,?y),?z))))) = max(N(L(?x_5),N(?x,N(?y,?z)))),
     N(N(?x_6,N(?x,?y)),?z) = N(?x_6,N(?x,N(?y,?z))),
     N(N(?x,?y_5),?z_5) = N(N(?y_5,?z_5),?x),
     N(?x_6,N(?y_6,?y)) = N(?y,N(?x_6,?y_6)),
     ?y_3 = max(N(L(?y_3),L(0))),
     s(max(N(L(?x_4),L(?y_4)))) = max(N(L(s(?y_4)),L(s(?x_4)))),
     max(N(L(?x_5),L(max(N(?y_5,?z_5))))) = max(N(N(?y_5,?z_5),L(?x_5))),
     max(N(L(?x_5),L(max(N(?x,?y))))) = max(N(L(?x_5),N(?y,?x))),
     N(N(?x_6,?x),?y) = N(?x_6,N(?y,?x)),
     N(?x,N(?y,?z_7)) = N(N(?y,?x),?z_7) ]
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 <max(N(L(?y_1),L(0))), ?y_1> by Rules <6, 1> preceded by [(max,1)]
 joinable by a reduction of rules <[([(max,1)],6),([],1)], []>
Critical Pair <max(N(L(s(?y_2)),L(s(?x_2)))), s(max(N(L(?x_2),L(?y_2))))> by Rules <6, 2> preceded by [(max,1)]
 joinable by a reduction of rules <[([],2)], [([(s,1),(max,1)],6)]>
Critical Pair <max(N(N(L(?x_3),?y_4),?z_4)), max(N(L(?x_3),L(max(N(?y_4,?z_4)))))> by Rules <4, 3> preceded by [(max,1)]
 joinable by a reduction of rules <[([(max,1)],5),([],3)], []>
Critical Pair <max(N(L(?x_3),N(N(?x_4,?y_4),?z_4))), max(N(L(?x_3),L(max(N(?x_4,N(?y_4,?z_4))))))> by Rules <4, 3> preceded by [(max,1),(N,2)]
 joinable by a reduction of rules <[([],3)], [([(max,1),(N,2),(L,1),(max,1)],4)]>
Critical Pair <max(N(L(?x_3),N(?x_5,N(?y_5,?z_5)))), max(N(L(?x_3),L(max(N(N(?x_5,?y_5),?z_5)))))> by Rules <5, 3> preceded by [(max,1),(N,2)]
 joinable by a reduction of rules <[([],3)], [([(max,1),(N,2),(L,1),(max,1)],5)]>
Critical Pair <max(N(N(?y_3,?z_3),L(?x_3))), max(N(L(?x_3),L(max(N(?y_3,?z_3)))))> by Rules <6, 3> preceded by [(max,1)]
 joinable by a reduction of rules <[([(max,1)],6),([],3)], []>
Critical Pair <max(N(L(?x_3),N(?y_6,?x_6))), max(N(L(?x_3),L(max(N(?x_6,?y_6)))))> by Rules <6, 3> preceded by [(max,1),(N,2)]
 joinable by a reduction of rules <[([],3)], [([(max,1),(N,2),(L,1),(max,1)],6)]>
Critical Pair <N(?x_4,N(?x_5,N(?y_5,?z_5))), N(N(?x_4,N(?x_5,?y_5)),?z_5)> by Rules <5, 4> preceded by [(N,2)]
 joinable by a reduction of rules <[([(N,2)],4)], [([],5)]>
Critical Pair <N(?x_4,N(?y_6,?x_6)), N(N(?x_4,?x_6),?y_6)> by Rules <6, 4> preceded by [(N,2)]
 joinable by a reduction of rules <[([(N,2)],6)], [([],5)]>
Critical Pair <N(N(N(?x_4,?y_4),?z_4),?z_5), N(?x_4,N(N(?y_4,?z_4),?z_5))> by Rules <4, 5> preceded by [(N,1)]
 joinable by a reduction of rules <[([(N,1)],5)], [([],4)]>
Critical Pair <N(N(?y_6,?x_6),?z_5), N(?x_6,N(?y_6,?z_5))> by Rules <6, 5> preceded by [(N,1)]
 joinable by a reduction of rules <[([(N,1)],6)], [([],4)]>
Critical Pair <N(?x_1,N(N(?x,?y),?z)), N(N(?x_1,?x),N(?y,?z))> by Rules <4, 4> preceded by [(N,2)]
 joinable by a reduction of rules <[([(N,2)],5)], [([],5)]>
Critical Pair <N(N(?x,N(?y,?z)),?z_1), N(N(?x,?y),N(?z,?z_1))> by Rules <5, 5> preceded by [(N,1)]
 joinable by a reduction of rules <[([(N,1)],4)], [([],4)]>
Critical Pair <N(?x_5,N(?y_5,N(?y_4,?z_4))), N(N(N(?x_5,?y_5),?y_4),?z_4)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],4)], [([],5)]>
Critical Pair <N(N(?y_4,?z_4),?x_6), N(N(?x_6,?y_4),?z_4)> by Rules <6, 4> preceded by []
 joinable by a reduction of rules <[([],6)], [([],5)]>
Critical Pair <N(?y_6,N(?x_5,?y_5)), N(?x_5,N(?y_5,?y_6))> by Rules <6, 5> preceded by []
 joinable by a reduction of rules <[([],6)], [([],4)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 9 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:
   [ max(L(?x)) -> ?x,
     max(N(L(0),L(?y))) -> ?y,
     max(N(L(s(?x)),L(s(?y)))) -> s(max(N(L(?x),L(?y)))),
     max(N(L(?x),N(?y,?z))) -> max(N(L(?x),L(max(N(?y,?z))))) ]
   [ N(?x,N(?y,?z)) -> N(N(?x,?y),?z),
     N(N(?x,?y),?z) -> N(?x,N(?y,?z)),
     N(?x,?y) -> N(?y,?x) ]