NO
(ignored inputs)COMMENT experiments for [36] submitted by: Takahito Aoto
Rewrite Rules:
[ br(0,?y,?z) -> ?y,
br(s(?x),?y,?z) -> ?z,
p(0) -> 0,
p(s(?x)) -> ?x,
+(?x,?y) -> br(?x,?y,+(p(?x),s(?y))),
+(?x,?y) -> br(?y,?x,+(s(?x),p(?y))) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ br(?x_3,?y_3,+(p(?x_3),s(?y_3))) = br(?y_3,?x_3,+(s(?x_3),p(?y_3))) ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development 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:
[ br(?y,?x,+(s(?x),p(?y))) = br(?x,?y,+(p(?x),s(?y))),
br(?x,?y,+(p(?x),s(?y))) = br(?y,?x,+(s(?x),p(?y))) ]
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 <5, 4> preceded by []
unknown Diagram Decreasing
[ br(0,?y,?z) -> ?y,
br(s(?x_1),?y_1,?z_1) -> ?z_1,
p(0) -> 0,
p(s(?x_2)) -> ?x_2,
+(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))),
+(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ]
Sort Assignment:
+ : 23*23=>23
0 : =>23
p : 23=>23
s : 23=>23
br : 23*23*23=>23
non-linear variables: {?x_3,?y_3,?y_4,?x_4}
non-linear types: {23}
types leq non-linear types: {23}
rules applicable to terms of non-linear types:
[ br(0,?y,?z) -> ?y,
br(s(?x_1),?y_1,?z_1) -> ?z_1,
p(0) -> 0,
p(s(?x_2)) -> ?x_2,
+(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))),
+(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ]
Rnl:
0: {}
1: {}
2: {}
3: {}
4: {0,1,2,3,4,5}
5: {0,1,2,3,4,5}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
[ br(0,?y,?z) -> ?y,
br(s(?x_1),?y_1,?z_1) -> ?z_1,
p(0) -> 0,
p(s(?x_2)) -> ?x_2,
+(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))),
+(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ]
Sort Assignment:
+ : 23*23=>23
0 : =>23
p : 23=>23
s : 23=>23
br : 23*23*23=>23
non-linear variables: {?x_3,?y_3,?y_4,?x_4}
non-linear types: {23}
types leq non-linear types: {23}
rules applicable to terms of non-linear types:
[ br(0,?y,?z) -> ?y,
br(s(?x_1),?y_1,?z_1) -> ?z_1,
p(0) -> 0,
p(s(?x_2)) -> ?x_2,
+(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))),
+(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 10 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(success)
(failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
where
F = {(+,2),(0,0),(p,1),(s,1),(br,3),(c_1,0)}
Q = {q_0,q_1,q_{+(0,s(p(c_1)))},q_{+(p(*),s(*))},q_{+(s(*),p(*))},q_{c_1},q_{*},q_{0},q_{p(*)},q_{s(*)},q_{p(c_1)},q_{s(p(c_1))}}
Qf = {q_0,q_1}
Delta =
[ +(q_{*},q_{*}) -> q_{*},
+(q_{*},q_{*}) -> q_{p(*)},
+(q_{0},q_{s(p(c_1))}) -> q_{+(0,s(p(c_1)))},
+(q_{p(*)},q_{s(*)}) -> q_{+(0,s(p(c_1)))},
+(q_{p(*)},q_{s(*)}) -> q_{+(p(*),s(*))},
+(q_{p(*)},q_{s(*)}) -> q_{+(s(*),p(*))},
+(q_{p(*)},q_{s(*)}) -> q_{p(*)},
+(q_{s(*)},q_{p(*)}) -> q_{+(0,s(p(c_1)))},
+(q_{s(*)},q_{p(*)}) -> q_{+(p(*),s(*))},
+(q_{s(*)},q_{p(*)}) -> q_{+(s(*),p(*))},
+(q_{s(*)},q_{p(*)}) -> q_{p(*)},
0 -> q_{*},
0 -> q_{0},
0 -> q_{p(*)},
p(q_{c_1}) -> q_{p(c_1)},
p(q_{*}) -> q_{*},
p(q_{*}) -> q_{p(*)},
s(q_{*}) -> q_{+(0,s(p(c_1)))},
s(q_{*}) -> q_{+(p(*),s(*))},
s(q_{*}) -> q_{+(s(*),p(*))},
s(q_{*}) -> q_{*},
s(q_{*}) -> q_{p(*)},
s(q_{*}) -> q_{s(*)},
s(q_{p(c_1)}) -> q_{+(0,s(p(c_1)))},
s(q_{p(c_1)}) -> q_{s(p(c_1))},
br(q_{c_1},q_{0},q_{+(0,s(p(c_1)))}) -> q_0,
br(q_{*},q_{*},q_{+(p(*),s(*))}) -> q_{p(*)},
br(q_{*},q_{*},q_{+(s(*),p(*))}) -> q_{p(*)},
br(q_{*},q_{*},q_{*}) -> q_{*},
br(q_{*},q_{*},q_{*}) -> q_{p(*)},
br(q_{0},q_{s(p(c_1))},q_{+(p(*),s(*))}) -> q_{+(0,s(p(c_1)))},
br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{+(0,s(p(c_1)))},
br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{+(p(*),s(*))},
br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{+(s(*),p(*))},
br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{p(*)},
br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{+(0,s(p(c_1)))},
br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{+(p(*),s(*))},
br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{+(s(*),p(*))},
br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{p(*)},
br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{+(0,s(p(c_1)))},
br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{+(p(*),s(*))},
br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{+(s(*),p(*))},
br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{p(*)},
br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{+(0,s(p(c_1)))},
br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{+(p(*),s(*))},
br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{+(s(*),p(*))},
br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{p(*)},
br(q_{s(p(c_1))},q_{0},q_{+(s(*),p(*))}) -> q_{+(0,s(p(c_1)))},
c_1 -> q_1,
c_1 -> q_{c_1},
c_1 -> q_{*},
c_1 -> q_{p(*)} ]
(failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (success)
Witness for Non-Confluence:
c_1>
Direct Methods: not CR
Combined result: not CR
584.trs: Success(not CR)
(1031 msec.)