(ignored inputs)COMMENT Example 3.3.1 of \cite{Gra96thesis}
Rewrite Rules:
[ b -> a,
b -> c,
c -> b,
c -> d ]
Apply Direct Methods...
Inner CPs:
[ ]
Outer CPs:
[ a = c,
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:
[ b = d,
d = 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),([],0)], []>
Critical Pair by Rules <3, 2> preceded by []
joinable by a reduction of rules <[], [([],1),([],3)]>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
[ b -> a,
c -> d ]
P:
[ b -> c,
c -> b ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
--> => no
--> => no
check joinability condition:
check modulo joinability of a and d: maybe not joinable
check modulo joinability of d and a: maybe not joinable
failed
failure(Step 1)
[ ]
Added S-Rules:
[ ]
Added P-Rules:
[ ]
STEP: 2 (linear)
S:
[ b -> a,
c -> d ]
P:
[ b -> c,
c -> b ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
--> => no
--> => no
check joinability condition:
check modulo joinability of a and d: maybe not joinable
check modulo joinability of d and a: maybe not joinable
failed
failure(Step 2)
[ ]
Added S-Rules:
[ ]
Added P-Rules:
[ ]
STEP: 3 (relative)
S:
[ b -> a,
c -> d ]
P:
[ b -> c,
c -> b ]
Check relative termination:
[ b -> a,
c -> d ]
[ b -> c,
c -> b ]
Polynomial Interpretation:
a:= 0
b:= (1)
c:= (1)
d:= (1)
retract b -> a
Polynomial Interpretation:
a:= 0
b:= (1)
c:= (1)
d:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from c
Not Confluent
Direct Methods: not CR
Final result: not CR
/local-scratch/hzankl/2012/cops2012/38.trs: Success(not CR)
(16 msec.)