MAYBE Problem: cons(x,cons(y,z)) -> big() inf(x) -> cons(x,inf(s(x))) Proof: DP Processor: DPs: inf#(x) -> inf#(s(x)) inf#(x) -> cons#(x,inf(s(x))) TRS: cons(x,cons(y,z)) -> big() inf(x) -> cons(x,inf(s(x))) TDG Processor: DPs: inf#(x) -> inf#(s(x)) inf#(x) -> cons#(x,inf(s(x))) TRS: cons(x,cons(y,z)) -> big() inf(x) -> cons(x,inf(s(x))) graph: inf#(x) -> inf#(s(x)) -> inf#(x) -> cons#(x,inf(s(x))) inf#(x) -> inf#(s(x)) -> inf#(x) -> inf#(s(x)) Restore Modifier: DPs: inf#(x) -> inf#(s(x)) inf#(x) -> cons#(x,inf(s(x))) TRS: cons(x,cons(y,z)) -> big() inf(x) -> cons(x,inf(s(x))) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: inf#(x) -> inf#(s(x)) TRS: cons(x,cons(y,z)) -> big() inf(x) -> cons(x,inf(s(x))) Open