MAYBE Problem: g(X) -> h(X) c() -> d() h(d()) -> g(c()) Proof: DP Processor: DPs: g#(X) -> h#(X) h#(d()) -> c#() h#(d()) -> g#(c()) TRS: g(X) -> h(X) c() -> d() h(d()) -> g(c()) Usable Rule Processor: DPs: g#(X) -> h#(X) h#(d()) -> c#() h#(d()) -> g#(c()) TRS: c() -> d() EDG Processor: DPs: g#(X) -> h#(X) h#(d()) -> c#() h#(d()) -> g#(c()) TRS: c() -> d() graph: h#(d()) -> g#(c()) -> g#(X) -> h#(X) g#(X) -> h#(X) -> h#(d()) -> c#() g#(X) -> h#(X) -> h#(d()) -> g#(c()) Restore Modifier: DPs: g#(X) -> h#(X) h#(d()) -> c#() h#(d()) -> g#(c()) TRS: g(X) -> h(X) c() -> d() h(d()) -> g(c()) SCC Processor: #sccs: 1 #rules: 2 #arcs: 3/9 DPs: h#(d()) -> g#(c()) g#(X) -> h#(X) TRS: g(X) -> h(X) c() -> d() h(d()) -> g(c()) Open