MAYBE Problem: f(x,empty()) -> x f(empty(),cons(a,k)) -> f(cons(a,k),k) f(cons(a,k),y) -> f(y,k) Proof: DP Processor: DPs: f#(empty(),cons(a,k)) -> f#(cons(a,k),k) f#(cons(a,k),y) -> f#(y,k) TRS: f(x,empty()) -> x f(empty(),cons(a,k)) -> f(cons(a,k),k) f(cons(a,k),y) -> f(y,k) Usable Rule Processor: DPs: f#(empty(),cons(a,k)) -> f#(cons(a,k),k) f#(cons(a,k),y) -> f#(y,k) TRS: f4(x,y) -> x f4(x,y) -> y Restore Modifier: DPs: f#(empty(),cons(a,k)) -> f#(cons(a,k),k) f#(cons(a,k),y) -> f#(y,k) TRS: f(x,empty()) -> x f(empty(),cons(a,k)) -> f(cons(a,k),k) f(cons(a,k),y) -> f(y,k) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(empty(),cons(a,k)) -> f#(cons(a,k),k) f#(cons(a,k),y) -> f#(y,k) TRS: f(x,empty()) -> x f(empty(),cons(a,k)) -> f(cons(a,k),k) f(cons(a,k),y) -> f(y,k) Open