(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,b) -> q(?x),
     q(?x) -> 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,b) -> q(?x_2),
     q(?x_3) -> f(?x_3,b) ]
Sort Assignment:
 b : =>18
 f : 18*18=>18
 g : 18=>21
 h : 18=>18
 k : 18*18=>18
 q : 18=>18
non-linear variables: {?x,?x_1}
non-linear types: {18}
types leq non-linear types: {18}
rules applicable to terms of non-linear types:
   [ f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)),
     k(?x_2,b) -> q(?x_2),
     q(?x_3) -> f(?x_3,b) ]
Rnl:
0: {1,2,3}
1: {1,2,3}
2: {}
3: {}
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,b) -> q(?x_2),
     q(?x_3) -> f(?x_3,b) ]
Sort Assignment:
 b : =>18
 f : 18*18=>18
 g : 18=>21
 h : 18=>18
 k : 18*18=>18
 q : 18=>18
non-linear variables: {?x,?x_1}
non-linear types: {18}
types leq non-linear types: {18}
rules applicable to terms of non-linear types:
   [ f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)),
     k(?x_2,b) -> q(?x_2),
     q(?x_3) -> f(?x_3,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) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ 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,b) -> q(?x),
     q(?x) -> f(?x,b) ]
Sort Assignment:
 b : =>18
 f : 18*18=>18
 g : 18=>21
 h : 18=>18
 k : 18*18=>18
 q : 18=>18
maximal types: {18,21}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ 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,b) -> q(?x),
     q(?x) -> f(?x,b) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ 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,b) -> q(?x),
     q(?x) -> f(?x,b) ]
Inside 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>
develop reducts from lhs term...
<{1}, g(h(h(f(f(h(f(f(b,b),b)),h(f(f(b,b),b))),h(f(f(b,b),b))))))>
<{1}, g(h(h(f(f(f(b,b),f(b,b)),f(b,b)))))>
<{1}, g(h(f(h(f(f(b,b),b)),b)))>
<{}, g(h(f(f(b,b),b)))>
develop reducts from rhs term...
<{2}, g(h(h(f(f(h(q(q(b))),h(q(q(b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(q(b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(q(b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(q(b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(k(b,b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(k(b,b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(k(b,b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(q(k(b,b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(q(b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(q(b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(q(b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(q(b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(k(b,b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(k(b,b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(k(b,b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(q(b))),h(k(k(b,b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(q(b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(q(b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(q(b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(q(b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(k(b,b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(k(b,b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(k(b,b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(q(k(b,b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(q(b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(q(b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(q(b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(q(b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(k(b,b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(k(b,b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(k(b,b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(q(k(b,b))),h(k(k(b,b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(q(b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(q(b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(q(b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(q(b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(k(b,b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(k(b,b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(k(b,b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(q(k(b,b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(q(b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(q(b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(q(b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(q(b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(k(b,b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(k(b,b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(k(b,b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(q(b),b)),h(k(k(b,b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(q(b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(q(b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(q(b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(q(b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(k(b,b)))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(k(b,b)))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(k(b,b)))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(q(k(b,b)))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(q(b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(q(b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(q(b),b))),h(k(q(b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(q(b),b))),h(k(k(b,b),b))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(q(q(b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(q(k(b,b)))))))>
<{2}, g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(q(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))))))>
Try A Minimal Decomposition {0,1}{2}{3}
{0,1}
(cm)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)) ]
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)) ]
Sort Assignment:
 b : =>14
 f : 14*14=>14
 g : 14=>15
 h : 14=>14
 k : 14*14=>14
non-linear variables: {?x,?x_1}
non-linear types: {14}
types leq non-linear types: {14}
rules applicable to terms of non-linear types:
   [ f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)) ]
Rnl:
0: {1}
1: {1}
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)) ]
Sort Assignment:
 b : =>14
 f : 14*14=>14
 g : 14=>15
 h : 14=>14
 k : 14*14=>14
non-linear variables: {?x,?x_1}
non-linear types: {14}
types leq non-linear types: {14}
rules applicable to terms of non-linear types:
   [ f(?x_1,b) -> h(f(f(?x_1,?x_1),?x_1)) ]
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)