(ignored inputs)COMMENT due to Levy , from p.814 of \cite{Hue80}
Rewrite Rules:
[ F(A,A) -> G(B,B),
A -> A',
F(A',?x) -> F(?x,?x),
F(?x,A') -> F(?x,?x),
G(B,B) -> F(A,A),
B -> B',
G(B',?x) -> G(?x,?x),
G(?x,B') -> G(?x,?x) ]
Apply Direct Methods...
Inner CPs:
[ F(A',A) = G(B,B),
F(A,A') = G(B,B),
G(B',B) = F(A,A),
G(B,B') = F(A,A) ]
Outer CPs:
[ F(A',A') = F(A',A'),
G(B',B') = G(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:
[ F(A,A') = G(B,B) {},
F(A',A) = G(B,B) {},
F(A',A') = G(B,B) {},
G(B,B') = F(A,A) {},
G(B',B) = F(A,A) {},
G(B',B') = F(A,A) {} ]
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ G(B',B') = G(B',B'),
F(A,A) = G(B,B'),
F(A,A) = G(B',B),
G(B,B') = F(A,A),
G(B',B) = F(A,A),
G(B',B') = F(A,A),
F(A',A') = F(A',A'),
G(B,B) = F(A,A'),
G(B,B) = F(A',A),
F(A,A') = G(B,B),
F(A',A) = G(B,B),
F(A',A') = G(B,B) ]
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 [(F,1)]
joinable by a reduction of rules <[([],2)], [([],4)]>
Critical Pair by Rules <1, 0> preceded by [(F,2)]
joinable by a reduction of rules <[([],3)], [([],4)]>
Critical Pair by Rules <5, 4> preceded by [(G,1)]
joinable by a reduction of rules <[([],6)], [([],0)]>
Critical Pair by Rules <5, 4> preceded by [(G,2)]
joinable by a reduction of rules <[([],7)], [([],0)]>
Critical Pair by Rules <3, 2> preceded by []
joinable by a reduction of rules <[], []>
Critical Pair by Rules <7, 6> preceded by []
joinable by a reduction of rules <[], []>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
[ A -> A',
F(A',?x) -> F(?x,?x),
F(?x,A') -> F(?x,?x),
B -> B',
G(B',?x) -> G(?x,?x),
G(?x,B') -> G(?x,?x) ]
P:
[ F(A,A) -> G(B,B),
G(B,B) -> F(A,A) ]
S: unknown termination
failure(Step 1)
STEP: 2 (linear)
S:
[ A -> A',
F(A',?x) -> F(?x,?x),
F(?x,A') -> F(?x,?x),
B -> B',
G(B',?x) -> G(?x,?x),
G(?x,B') -> G(?x,?x) ]
P:
[ F(A,A) -> G(B,B),
G(B,B) -> F(A,A) ]
S: not linear
failure(Step 2)
STEP: 3 (relative)
S:
[ A -> A',
F(A',?x) -> F(?x,?x),
F(?x,A') -> F(?x,?x),
B -> B',
G(B',?x) -> G(?x,?x),
G(?x,B') -> G(?x,?x) ]
P:
[ F(A,A) -> G(B,B),
G(B,B) -> F(A,A) ]
Check relative termination:
[ A -> A',
F(A',?x) -> F(?x,?x),
F(?x,A') -> F(?x,?x),
B -> B',
G(B',?x) -> G(?x,?x),
G(?x,B') -> G(?x,?x) ]
[ F(A,A) -> G(B,B),
G(B,B) -> F(A,A) ]
unknown relative termination
S/P: unknown relative termination
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from G(B,B)
Not Confluent
Direct Methods: not CR
Final result: not CR
/local-scratch/hzankl/2012/cops2012/49.trs: Success(not CR)
(135 msec.)