MAYBE Problem: f(a(),X) -> f(X,X) c() -> a() c() -> b() Proof: DP Processor: DPs: f#(a(),X) -> f#(X,X) TRS: f(a(),X) -> f(X,X) c() -> a() c() -> b() Usable Rule Processor: DPs: f#(a(),X) -> f#(X,X) TRS: f6(x,y) -> x f6(x,y) -> y Restore Modifier: DPs: f#(a(),X) -> f#(X,X) TRS: f(a(),X) -> f(X,X) c() -> a() c() -> b() SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(a(),X) -> f#(X,X) TRS: f(a(),X) -> f(X,X) c() -> a() c() -> b() Open