(ignored inputs)COMMENT Example 3 of \cite{GL06}
Rewrite Rules:
[ b -> a,
b -> c,
c -> h(b),
c -> d,
a -> h(a),
d -> h(d) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c,
h(b) = d ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ h(b) = d,
d = h(b),
a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
joinable by a reduction of rules <[([],2),([(h,1)],0)], [([],4)]>
Critical Pair by Rules <3, 2> preceded by []
joinable by a reduction of rules <[([],5)], [([(h,1)],1),([(h,1)],3)]>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Unknown
Direct Methods: Can't judge
Try Persistent Decomposition for...
[ b -> a,
b -> c,
c -> h(b),
c -> d,
a -> h(a),
d -> h(d) ]
Sort Assignment:
a : =>7
b : =>7
c : =>7
d : =>7
h : 7=>7
maximal types: {7}
Persistent Decomposition failed: Can't judge
Try Layer Preserving Decomposition for...
[ b -> a,
b -> c,
c -> h(b),
c -> d,
a -> h(a),
d -> h(d) ]
Layer Preserving Decomposition failed: Can't judge
Try Commutative Decomposition for...
[ b -> a,
b -> c,
c -> h(b),
c -> d,
a -> h(a),
d -> h(d) ]
Outside Critical Pair: by Rules <1, 0>
develop reducts from lhs term...
<{3}, d>
<{2}, h(b)>
<{}, c>
develop reducts from rhs term...
<{4}, h(a)>
<{}, a>
Outside Critical Pair: by Rules <3, 2>
develop reducts from lhs term...
<{5}, h(d)>
<{}, d>
develop reducts from rhs term...
<{1}, h(c)>
<{0}, h(a)>
<{}, h(b)>
Try A Minimal Decomposition {0,1}{2,3}{4}{5}
{0,1}
(cm)Rewrite Rules:
[ b -> a,
b -> c ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), not WCR
Knuth&Bendix
Direct Methods: not CR
{2,3}
(cm)Rewrite Rules:
[ c -> h(b),
c -> d ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ h(b) = d ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), not WCR
Knuth&Bendix
Direct Methods: not CR
{4}
(cm)Rewrite Rules:
[ a -> h(a) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
Development Closed
Direct Methods: CR
{5}
(cm)Rewrite Rules:
[ d -> h(d) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
Development Closed
Direct Methods: CR
Try to add other components to {0,1}
Add {2,3}
{0,1,2,3}
(cm)Rewrite Rules:
[ b -> a,
b -> c,
c -> h(b),
c -> d ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c,
h(b) = d ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ h(b) = d,
d = h(b),
a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from c
Not Confluent
Direct Methods: not CR
Add {2,3}{4}
{0,1,2,3,4}
(cm)Rewrite Rules:
[ b -> a,
b -> c,
c -> h(b),
c -> d,
a -> h(a) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c,
h(b) = d ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ h(b) = d,
d = h(b),
a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
joinable by a reduction of rules <[([],2),([(h,1)],0)], [([],4)]>
Critical Pair by Rules <3, 2> preceded by []
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from c
Not Confluent
Direct Methods: not CR
Add {2,3}{5}
{0,1,2,3,5}
(cm)Rewrite Rules:
[ b -> a,
b -> c,
c -> h(b),
c -> d,
d -> h(d) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c,
h(b) = d ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ h(b) = d,
d = h(b),
a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from c
Not Confluent
Direct Methods: not CR
Add {4}
{0,1,4}
(cm)Rewrite Rules:
[ b -> a,
b -> c,
a -> h(a) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from b
Not Confluent
Direct Methods: not CR
Add {5}
{0,1,5}
(cm)Rewrite Rules:
[ b -> a,
b -> c,
d -> h(d) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from b
Not Confluent
Direct Methods: not CR
Add {4}{5}
{0,1,4,5}
(cm)Rewrite Rules:
[ b -> a,
b -> c,
a -> h(a),
d -> h(d) ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ a = c,
c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <1, 0> preceded by []
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from b
Not Confluent
Direct Methods: not CR
Commutative Decomposition failed: Can't judge
No further decomposition possible
Final result: Can't judge
/local-scratch/hzankl/2012/cops2012/21.trs: Failure(unknown)
(24 msec.)