(ignored inputs)COMMENT doi:10.4230/LIPIcs.FSCD.2016.33 [36] Example 24 submitted by: Takahito Aoto
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(s(0),?y) -> s(?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     s(s(?x)) -> s(?x),
     s(?x) -> s(s(?x)) ]
Apply Direct Methods...
Inner CPs:
   [ +(s(s(0)),?y_1) = s(?y_1),
     +(?y,?z_2) = +(0,+(?y,?z_2)),
     +(s(?y_1),?z_2) = +(s(0),+(?y_1,?z_2)),
     +(+(?y_3,?x_3),?z_2) = +(?x_3,+(?y_3,?z_2)),
     s(s(s(?x_5))) = s(?x_5),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     s(s(?x)) = s(s(?x)) ]
Outer CPs:
   [ ?y = +(?y,0),
     s(?y_1) = +(?y_1,s(0)),
     +(?x_2,+(?y_2,?z_2)) = +(?z_2,+(?x_2,?y_2)),
     s(?x_4) = s(s(s(?x_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:
   [ +(?y,0) = ?y,
     +(0,+(?y,?z_3)) = +(?y,?z_3),
     +(?y,s(s(0))) = s(?y),
     +(?y,s(0)) = s(?y),
     +(s(s(0)),?y) = s(?y),
     +(s(s(0)),+(?y,?z_3)) = +(s(?y),?z_3),
     +(s(0),+(?y,?z_3)) = +(s(?y),?z_3),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,s(?y)) = +(s(0),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(s(?y),?z) = +(s(0),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(s(?y),+(?z,?z_1)) = +(+(s(0),+(?y,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     ?y = +(?y,0),
     s(?y) = +(?y,s(0)),
     +(?x_3,+(?y_3,?y)) = +(?y,+(?x_3,?y_3)),
     +(?x,+(?y,?z_4)) = +(+(?y,?x),?z_4),
     s(s(s(?x_1))) = s(s(?x_1)),
     s(s(s(s(?x)))) = s(?x),
     s(s(s(?x))) = s(?x),
     s(s(?x_1)) = s(s(?x_1)),
     s(s(?x_1)) = s(s(s(?x_1))),
     s(?x_5) = s(s(s(?x_5))),
     s(?y_3) = +(s(s(0)),?y_3) ]
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 <+(s(s(0)),?y_1), s(?y_1)> by Rules <5, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],4),([],1)], []>
Critical Pair <+(?y,?z_2), +(0,+(?y,?z_2))> by Rules <0, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <+(s(?y_1),?z_2), +(s(0),+(?y_1,?z_2))> by Rules <1, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[([],3)], [([(+,2)],3),([],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([],3)], [([],3),([(+,1)],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([],3)], [([],3),([],2),([],3),([],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([],3),([(+,2)],4)], [([(+,2)],3),([],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([],3),([(+,2)],4)], [([],3),([(+,1)],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([],3),([(+,2)],4)], [([],3),([],2),([],3),([],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1),(s,1)],5),([],3),([(+,2),(s,1)],4),([(+,2)],4)], [([(+,2)],3),([],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1),(s,1)],5),([],3),([(+,2),(s,1)],4),([(+,2)],4)], [([],3),([(+,1)],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1),(s,1)],5),([],3),([(+,2),(s,1)],4),([(+,2)],4)], [([],3),([],2),([],3),([],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1),(s,1)],5),([],3),([(+,2)],4),([(+,2)],4)], [([(+,2)],3),([],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1),(s,1)],5),([],3),([(+,2)],4),([(+,2)],4)], [([],3),([(+,1)],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1),(s,1)],5),([],3),([(+,2)],4),([(+,2)],4)], [([],3),([],2),([],3),([],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],5),([],3),([(+,2),(s,1)],4),([(+,2)],4)], [([(+,2)],3),([],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],5),([],3),([(+,2),(s,1)],4),([(+,2)],4)], [([],3),([(+,1)],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],5),([],3),([(+,2),(s,1)],4),([(+,2)],4)], [([],3),([],2),([],3),([],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],5),([],3),([(+,2)],4),([(+,2)],4)], [([(+,2)],3),([],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],5),([],3),([(+,2)],4),([(+,2)],4)], [([],3),([(+,1)],3),([],2),([(+,2)],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],5),([],3),([(+,2)],4),([(+,2)],4)], [([],3),([],2),([],3),([],2),([(+,2)],1)]>
Critical Pair <+(+(?y_3,?x_3),?z_2), +(?x_3,+(?y_3,?z_2))> by Rules <3, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],3),([],2)], []>
 joinable by a reduction of rules <[([],2),([(+,2)],3)], [([],3),([],2)]>
Critical Pair <s(s(s(?x_5))), s(?x_5)> by Rules <5, 4> preceded by [(s,1)]
 joinable by a reduction of rules <[([(s,1)],4)], [([],5)]>
 joinable by a reduction of rules <[([],4)], [([],5)]>
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 <[([],2),([(+,2)],2)], [([],2)]>
Critical Pair <s(s(?x)), s(s(?x))> by Rules <4, 4> preceded by [(s,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <+(?y_3,0), ?y_3> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([],3),([],0)], []>
Critical Pair <+(?y_3,s(0)), s(?y_3)> by Rules <3, 1> preceded by []
 joinable by a reduction of rules <[([],3),([],1)], []>
Critical Pair <+(?y_3,+(?x_2,?y_2)), +(?x_2,+(?y_2,?y_3))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([],3),([],2)], []>
Critical Pair <s(s(s(?x_4))), s(?x_4)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([(s,1)],4)], [([],5)]>
 joinable by a reduction of rules <[([],4)], [([],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 (success)
<F,Q,Q_f,Delta> where
   F = {(+,2),(0,0),(s,1),(c_1,0),(c_2,0)}
   Q = {q_0,q_1,q_{+(*,*)},q_{c_1},q_{c_2},q_{s(c_1)},q_{*},q_{+(c_1,c_2)}}
   Qf = {q_0,q_1}
   Delta = 
   [ +(q_{+(*,*)},q_{+(*,*)}) -> q_{+(*,*)},
     +(q_{+(*,*)},q_{*}) -> q_{+(*,*)},
     +(q_{c_1},q_{c_2}) -> q_{+(c_1,c_2)},
     +(q_{c_2},q_{c_1}) -> q_{+(c_1,c_2)},
     +(q_{c_2},q_{s(c_1)}) -> q_1,
     +(q_{s(c_1)},q_{c_2}) -> q_1,
     +(q_{*},q_{+(*,*)}) -> q_{+(*,*)},
     +(q_{*},q_{*}) -> q_{+(*,*)},
     +(q_{*},q_{*}) -> q_{*},
     0 -> q_{+(*,*)},
     0 -> q_{*},
     s(q_0) -> q_0,
     s(q_{+(*,*)}) -> q_{+(*,*)},
     s(q_{c_1}) -> q_{s(c_1)},
     s(q_{s(c_1)}) -> q_{s(c_1)},
     s(q_{*}) -> q_{+(*,*)},
     s(q_{*}) -> q_{*},
     s(q_{+(c_1,c_2)}) -> q_0,
     c_1 -> q_{+(*,*)},
     c_1 -> q_{c_1},
     c_1 -> q_{*},
     c_2 -> q_{+(*,*)},
     c_2 -> q_{c_2},
     c_2 -> q_{*} ]
Witness for Non-Confluence: <s(+(c_1,c_2)), +(s(c_1),c_2)>
Direct Methods: not CR

Combined result: not CR
574.trs: Success(not CR)
NO
(453 msec.)