(ignored inputs)COMMENT Example 3.3.2 of \cite{Gra96thesis}
Rewrite Rules:
[ f(b) -> a,
f(b) -> f(c),
f(c) -> f(b),
f(c) -> d,
b -> e,
c -> e',
f(e) -> a,
f(e') -> d ]
Apply Direct Methods...
Inner CPs:
[ f(e) = a,
f(e) = f(c),
f(e') = f(b),
f(e') = d ]
Outer CPs:
[ a = f(c),
f(b) = d ]
not Overlay, check Termination...
unknown/not 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:
[ d = f(e'),
f(b) = f(e'),
f(c) = f(e),
a = f(e),
f(e') = d,
f(b) = d,
f(e') = f(b),
d = f(b),
f(e) = f(c),
a = f(c),
f(e) = a,
f(c) = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <4, 0> preceded by [(f,1)]
joinable by a reduction of rules <[([],6)], []>
Critical Pair by Rules <4, 1> preceded by [(f,1)]
joinable by a reduction of rules <[], [([],2),([(f,1)],4)]>
joinable by a reduction of rules <[([],6)], [([],2),([],0)]>
Critical Pair by Rules <5, 2> preceded by [(f,1)]
joinable by a reduction of rules <[], [([],1),([(f,1)],5)]>
joinable by a reduction of rules <[([],7)], [([],1),([],3)]>
Critical Pair by Rules <5, 3> preceded by [(f,1)]
joinable by a reduction of rules <[([],7)], []>
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:
[ f(b) -> a,
f(c) -> d,
b -> e,
c -> e',
f(e) -> a,
f(e') -> d ]
P:
[ f(b) -> f(c),
f(c) -> f(b) ]
S: terminating
CP(S,S):
--> => yes
--> => yes
PCP_in(symP,S):
CP(S,symP):
--> => no
--> => no
--> => 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
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:
[ f(b) -> a,
f(c) -> d,
b -> e,
c -> e',
f(e) -> a,
f(e') -> d ]
P:
[ f(b) -> f(c),
f(c) -> f(b) ]
S: terminating
CP(S,S):
--> => yes
--> => yes
CP_in(symP,S):
CP(S,symP):
--> => no
--> => no
--> => 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
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:
[ f(b) -> a,
f(c) -> d,
b -> e,
c -> e',
f(e) -> a,
f(e') -> d ]
P:
[ f(b) -> f(c),
f(c) -> f(b) ]
Check relative termination:
[ f(b) -> a,
f(c) -> d,
b -> e,
c -> e',
f(e) -> a,
f(e') -> d ]
[ f(b) -> f(c),
f(c) -> f(b) ]
Polynomial Interpretation:
a:= 0
b:= 0
c:= 0
d:= (4)
e:= 0
f:= (9)+(8)*x1
e':= 0
retract f(b) -> a
retract f(c) -> d
retract f(e) -> a
retract f(e') -> d
Polynomial Interpretation:
a:= 0
b:= (2)
c:= (2)
d:= (12)
e:= 0
f:= (2)*x1*x1
e':= 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 f(c)
Not Confluent
Direct Methods: not CR
Final result: not CR
/local-scratch/hzankl/2012/cops2012/39.trs: Success(not CR)
(68 msec.)