(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.)