YES Problem: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Proof: DP Processor: DPs: rev#(++(x,y)) -> rev#(x) rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> ++#(rev(y),rev(x)) ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(++(x,y),z) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Usable Rule Processor: DPs: rev#(++(x,y)) -> rev#(x) rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> ++#(rev(y),rev(x)) ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(++(x,y),z) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) TDG Processor: DPs: rev#(++(x,y)) -> rev#(x) rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> ++#(rev(y),rev(x)) ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(++(x,y),z) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) graph: ++#(.(x,y),z) -> ++#(y,z) -> ++#(x,++(y,z)) -> ++#(++(x,y),z) ++#(.(x,y),z) -> ++#(y,z) -> ++#(x,++(y,z)) -> ++#(x,y) ++#(.(x,y),z) -> ++#(y,z) -> ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(++(x,y),z) -> ++#(x,++(y,z)) -> ++#(++(x,y),z) ++#(x,++(y,z)) -> ++#(++(x,y),z) -> ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(++(x,y),z) -> ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(x,y) -> ++#(x,++(y,z)) -> ++#(++(x,y),z) ++#(x,++(y,z)) -> ++#(x,y) -> ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(x,y) -> ++#(.(x,y),z) -> ++#(y,z) rev#(++(x,y)) -> ++#(rev(y),rev(x)) -> ++#(x,++(y,z)) -> ++#(++(x,y),z) rev#(++(x,y)) -> ++#(rev(y),rev(x)) -> ++#(x,++(y,z)) -> ++#(x,y) rev#(++(x,y)) -> ++#(rev(y),rev(x)) -> ++#(.(x,y),z) -> ++#(y,z) rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> ++#(rev(y),rev(x)) rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> rev#(x) rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> ++#(rev(y),rev(x)) rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> rev#(x) Restore Modifier: DPs: rev#(++(x,y)) -> rev#(x) rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> ++#(rev(y),rev(x)) ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(++(x,y),z) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) SCC Processor: #sccs: 2 #rules: 5 #arcs: 18/36 DPs: rev#(++(x,y)) -> rev#(y) rev#(++(x,y)) -> rev#(x) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [rev#](x0) = x0 + 1, [make](x0) = 1, [.](x0, x1) = 1, [++](x0, x1) = x0 + x1 + 1, [rev](x0) = x0, [nil] = 0 orientation: rev#(++(x,y)) = x + y + 2 >= y + 1 = rev#(y) rev#(++(x,y)) = x + y + 2 >= x + 1 = rev#(x) rev(nil()) = 0 >= 0 = nil() rev(rev(x)) = x >= x = x rev(++(x,y)) = x + y + 1 >= x + y + 1 = ++(rev(y),rev(x)) ++(nil(),y) = y + 1 >= y = y ++(x,nil()) = x + 1 >= x = x ++(.(x,y),z) = z + 2 >= 1 = .(x,++(y,z)) ++(x,++(y,z)) = x + y + z + 2 >= x + y + z + 2 = ++(++(x,y),z) make(x) = 1 >= 1 = .(x,nil()) problem: DPs: TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Qed DPs: ++#(.(x,y),z) -> ++#(y,z) ++#(x,++(y,z)) -> ++#(x,y) ++#(x,++(y,z)) -> ++#(++(x,y),z) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [++#](x0, x1) = x1 + 1, [make](x0) = 0, [.](x0, x1) = x1, [++](x0, x1) = x0 + x1 + 1, [rev](x0) = x0, [nil] = 0 orientation: ++#(.(x,y),z) = z + 1 >= z + 1 = ++#(y,z) ++#(x,++(y,z)) = y + z + 2 >= y + 1 = ++#(x,y) ++#(x,++(y,z)) = y + z + 2 >= z + 1 = ++#(++(x,y),z) rev(nil()) = 0 >= 0 = nil() rev(rev(x)) = x >= x = x rev(++(x,y)) = x + y + 1 >= x + y + 1 = ++(rev(y),rev(x)) ++(nil(),y) = y + 1 >= y = y ++(x,nil()) = x + 1 >= x = x ++(.(x,y),z) = y + z + 1 >= y + z + 1 = .(x,++(y,z)) ++(x,++(y,z)) = x + y + z + 2 >= x + y + z + 2 = ++(++(x,y),z) make(x) = 0 >= 0 = .(x,nil()) problem: DPs: ++#(.(x,y),z) -> ++#(y,z) TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Matrix Interpretation Processor: dimension: 1 interpretation: [++#](x0, x1) = x0 + 1, [make](x0) = x0 + 1, [.](x0, x1) = x1 + 1, [++](x0, x1) = x0 + x1, [rev](x0) = x0, [nil] = 0 orientation: ++#(.(x,y),z) = y + 2 >= y + 1 = ++#(y,z) rev(nil()) = 0 >= 0 = nil() rev(rev(x)) = x >= x = x rev(++(x,y)) = x + y >= x + y = ++(rev(y),rev(x)) ++(nil(),y) = y >= y = y ++(x,nil()) = x >= x = x ++(.(x,y),z) = y + z + 1 >= y + z + 1 = .(x,++(y,z)) ++(x,++(y,z)) = x + y + z >= x + y + z = ++(++(x,y),z) make(x) = x + 1 >= 1 = .(x,nil()) problem: DPs: TRS: rev(nil()) -> nil() rev(rev(x)) -> x rev(++(x,y)) -> ++(rev(y),rev(x)) ++(nil(),y) -> y ++(x,nil()) -> x ++(.(x,y),z) -> .(x,++(y,z)) ++(x,++(y,z)) -> ++(++(x,y),z) make(x) -> .(x,nil()) Qed