(ignored inputs)COMMENT from p.811 of \cite{Hue80}
Rewrite Rules:
[ F(?x) -> A,
F(?x) -> G(F(?x)),
G(F(?x)) -> F(H(?x)),
G(F(?x)) -> B ]
Apply Direct Methods...
Inner CPs:
[ G(A) = F(H(?x)),
G(G(F(?x_1))) = F(H(?x_1)),
G(A) = B,
G(G(F(?x_1))) = B ]
Outer CPs:
[ A = G(F(?x)),
F(H(?x_2)) = B ]
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:
[ G(G(F(?x))) = B,
G(A) = B,
F(H(?x)) = B,
G(G(F(?x))) = F(H(?x)),
G(A) = F(H(?x)),
B = F(H(?x)),
B = G(G(F(?x))),
F(H(?x)) = G(G(F(?x))),
A = G(F(?x)),
B = G(A),
F(H(?x)) = G(A),
G(F(?x)) = A ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair by Rules <0, 2> preceded by [(G,1)]
joinable by a reduction of rules <[], [([],1),([(G,1)],0)]>
Critical Pair by Rules <1, 2> preceded by [(G,1)]
joinable by a reduction of rules <[([(G,1)],2)], [([],1)]>
Critical Pair by Rules <0, 3> preceded by [(G,1)]
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: from G(F(?x_1))
Not Confluent
Direct Methods: not CR
Final result: not CR
/local-scratch/hzankl/2012/cops2012/43.trs: Success(not CR)
(2 msec.)