YES Problem: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Proof: DP Processor: DPs: f#(.(nil(),y)) -> f#(y) f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) g#(.(x,nil())) -> g#(x) g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) EDG Processor: DPs: f#(.(nil(),y)) -> f#(y) f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) g#(.(x,nil())) -> g#(x) g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) graph: g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) -> g#(.(x,nil())) -> g#(x) g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) -> g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) g#(.(x,nil())) -> g#(x) -> g#(.(x,nil())) -> g#(x) g#(.(x,nil())) -> g#(x) -> g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) -> f#(.(nil(),y)) -> f#(y) f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) -> f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) f#(.(nil(),y)) -> f#(y) -> f#(.(nil(),y)) -> f#(y) f#(.(nil(),y)) -> f#(y) -> f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) SCC Processor: #sccs: 2 #rules: 4 #arcs: 8/16 DPs: f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) f#(.(nil(),y)) -> f#(y) TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0 + 1, [g](x0) = x0, [.](x0, x1) = x0 + x1, [f](x0) = x0, [nil] = 1 orientation: f#(.(.(x,y),z)) = x + y + z + 1 >= x + y + z + 1 = f#(.(x,.(y,z))) f#(.(nil(),y)) = y + 2 >= y + 1 = f#(y) f(nil()) = 1 >= 1 = nil() f(.(nil(),y)) = y + 1 >= y + 1 = .(nil(),f(y)) f(.(.(x,y),z)) = x + y + z >= x + y + z = f(.(x,.(y,z))) g(nil()) = 1 >= 1 = nil() g(.(x,nil())) = x + 1 >= x + 1 = .(g(x),nil()) g(.(x,.(y,z))) = x + y + z >= x + y + z = g(.(.(x,y),z)) problem: DPs: f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: f60() -> 2* f{#,0}(4) -> 1* .0(2,3) -> 4* .0(2,2) -> 3* .0(2,4) -> 4* problem: DPs: TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Qed DPs: g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) g#(.(x,nil())) -> g#(x) TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0, [g](x0) = x0 + 1, [.](x0, x1) = x0 + x1 + 1, [f](x0) = x0, [nil] = 1 orientation: g#(.(x,.(y,z))) = x + y + z + 2 >= x + y + z + 2 = g#(.(.(x,y),z)) g#(.(x,nil())) = x + 2 >= x = g#(x) f(nil()) = 1 >= 1 = nil() f(.(nil(),y)) = y + 2 >= y + 2 = .(nil(),f(y)) f(.(.(x,y),z)) = x + y + z + 2 >= x + y + z + 2 = f(.(x,.(y,z))) g(nil()) = 2 >= 1 = nil() g(.(x,nil())) = x + 3 >= x + 3 = .(g(x),nil()) g(.(x,.(y,z))) = x + y + z + 3 >= x + y + z + 3 = g(.(.(x,y),z)) problem: DPs: g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: g{#,0}(4) -> 1* .0(4,2) -> 4* .0(3,2) -> 4* .0(2,2) -> 3* f100() -> 2* problem: DPs: TRS: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Qed