(ignored inputs)COMMENT Example 8 from [HM11]: doi: http://dx.doi.org/10.1007/s10817-011-9238-x
Rewrite Rules:
[ f(a,a) -> c,
f(b,?x) -> f(?x,?x),
f(?x,b) -> f(?x,?x),
a -> b ]
Apply Direct Methods...
Inner CPs:
[ f(b,a) = c,
f(a,b) = c ]
Outer CPs:
[ f(b,b) = f(b,b) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Left-Linear, not Right-Linear
unknown Development Closed
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:
[ c = f(a,b),
c = f(b,a),
f(b,b) = f(b,b),
f(a,b) = c,
f(b,a) = c,
f(b,b) = c ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <3, 0> preceded by [(f,1)]
joinable by a reduction of rules <[([],1),([],0)], []>
Critical Pair by Rules <3, 0> preceded by [(f,2)]
joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair by Rules <2, 1> preceded by []
joinable by a reduction of rules <[], []>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from f(a,a)
Not Confluent
Direct Methods: not CR
Final result: not CR
/local-scratch/hzankl/2012/cops2012/113.trs: Success(not CR)
(15 msec.)