(ignored inputs)COMMENT from van Oostrom ( AJSW 2016 ) submitted by: Vincent van Oostrom
Rewrite Rules:
   [ g(f(b,?x)) -> g(h(h(f(f(h(k(k(?x,?x),?x)),h(k(k(?x,?x),?x))),h(k(k(?x,?x),?x)))))),
     f(?x,b) -> h(f(f(?x,?x),?x)),
     k(?x,?y) -> q(?x,?y,?y),
     q(?x,?y,b) -> r(?x,?y),
     r(?x,b) -> f(?x,b) ]
Apply Direct Methods...
Inner CPs:
   [ g(h(f(f(b,b),b))) = g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b)))))) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development 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:
   [ g(h(f(f(b,b),b))) = g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b)))))),
     g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b)))))) = g(h(f(f(b,b),b))) ]
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 <g(h(f(f(b,b),b))), g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b))))))> by Rules <1, 0> preceded by [(g,1)]
unknown Diagram Decreasing
   [ g(f(b,?x)) -> g(h(h(f(f(h(k(k(?x,?x),?x)),h(k(k(?x,?x),?x))),h(k(k(?x,?x),?x)))))),
     f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)),
     k(?x_2,?y_2) -> q(?x_2,?y_2,?y_2),
     q(?x_3,?y_3,b) -> r(?x_3,?y_3),
     r(?x_4,b) -> f(?x_4,b) ]
Sort Assignment:
 b : =>26
 f : 26*26=>26
 g : 26=>30
 h : 26=>26
 k : 26*26=>26
 q : 26*26*26=>26
 r : 26*26=>26
non-linear variables: {?x,?x_1,?y_2}
non-linear types: {26}
types leq non-linear types: {26}
rules applicable to terms of non-linear types:
   [ f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)),
     k(?x_2,?y_2) -> q(?x_2,?y_2,?y_2),
     q(?x_3,?y_3,b) -> r(?x_3,?y_3),
     r(?x_4,b) -> f(?x_4,b) ]
Rnl:
0: {1,2,3,4}
1: {1,2,3,4}
2: {1,2,3,4}
3: {}
4: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ g(f(b,?x)) -> g(h(h(f(f(h(k(k(?x,?x),?x)),h(k(k(?x,?x),?x))),h(k(k(?x,?x),?x)))))),
     f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)),
     k(?x_2,?y_2) -> q(?x_2,?y_2,?y_2),
     q(?x_3,?y_3,b) -> r(?x_3,?y_3),
     r(?x_4,b) -> f(?x_4,b) ]
Sort Assignment:
 b : =>26
 f : 26*26=>26
 g : 26=>30
 h : 26=>26
 k : 26*26=>26
 q : 26*26*26=>26
 r : 26*26=>26
non-linear variables: {?x,?x_1,?y_2}
non-linear types: {26}
types leq non-linear types: {26}
rules applicable to terms of non-linear types:
   [ f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)),
     k(?x_2,?y_2) -> q(?x_2,?y_2,?y_2),
     q(?x_3,?y_3,b) -> r(?x_3,?y_3),
     r(?x_4,b) -> f(?x_4,b) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 11 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)