YES(?,O(n^3)) 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: RT Transformation Processor: strict: 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)) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [g](x0) = x0, [.](x0, x1) = x0 + x1, [f](x0) = x0 + 8, [nil] = 0 orientation: f(nil()) = 8 >= 0 = nil() f(.(nil(),y)) = y + 8 >= y + 8 = .(nil(),f(y)) f(.(.(x,y),z)) = x + y + z + 8 >= x + y + z + 8 = f(.(x,.(y,z))) g(nil()) = 0 >= 0 = nil() g(.(x,nil())) = x >= x = .(g(x),nil()) g(.(x,.(y,z))) = x + y + z >= x + y + z = g(.(.(x,y),z)) problem: strict: 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)) weak: f(nil()) -> nil() Matrix Interpretation Processor: dimension: 1 interpretation: [g](x0) = x0 + 5, [.](x0, x1) = x0 + x1, [f](x0) = x0 + 4, [nil] = 0 orientation: f(.(nil(),y)) = y + 4 >= y + 4 = .(nil(),f(y)) f(.(.(x,y),z)) = x + y + z + 4 >= x + y + z + 4 = f(.(x,.(y,z))) g(nil()) = 5 >= 0 = nil() g(.(x,nil())) = x + 5 >= x + 5 = .(g(x),nil()) g(.(x,.(y,z))) = x + y + z + 5 >= x + y + z + 5 = g(.(.(x,y),z)) f(nil()) = 4 >= 0 = nil() problem: strict: f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) weak: g(nil()) -> nil() f(nil()) -> nil() Matrix Interpretation Processor: dimension: 2 interpretation: [1 8] [g](x0) = [0 1]x0, [.](x0, x1) = x0 + x1, [0] [f](x0) = x0 + [2], [0] [nil] = [2] orientation: [0] [0] f(.(nil(),y)) = y + [4] >= y + [4] = .(nil(),f(y)) [0] [0] f(.(.(x,y),z)) = x + y + z + [2] >= x + y + z + [2] = f(.(x,.(y,z))) [1 8] [16] [1 8] [0] g(.(x,nil())) = [0 1]x + [2 ] >= [0 1]x + [2] = .(g(x),nil()) [1 8] [1 8] [1 8] [1 8] [1 8] [1 8] g(.(x,.(y,z))) = [0 1]x + [0 1]y + [0 1]z >= [0 1]x + [0 1]y + [0 1]z = g(.(.(x,y),z)) [16] [0] g(nil()) = [2 ] >= [2] = nil() [0] [0] f(nil()) = [4] >= [2] = nil() problem: strict: f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(.(x,.(y,z))) -> g(.(.(x,y),z)) weak: g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() f(nil()) -> nil() Matrix Interpretation Processor: dimension: 3 interpretation: [1 0 0] [2] [g](x0) = [0 1 0]x0 + [7] [0 0 0] [4], [1 0 0] [.](x0, x1) = [0 1 0]x0 + x1 [0 0 0] , [1 1 0] [0] [f](x0) = [0 1 1]x0 + [3] [0 0 1] [0], [0] [nil] = [1] [3] orientation: [1 1 0] [1] [1 1 0] [0] f(.(nil(),y)) = [0 1 1]y + [4] >= [0 1 1]y + [4] = .(nil(),f(y)) [0 0 1] [0] [0 0 1] [0] [1 1 0] [1 1 0] [1 1 0] [0] [1 1 0] [1 1 0] [1 1 0] [0] f(.(.(x,y),z)) = [0 1 0]x + [0 1 0]y + [0 1 1]z + [3] >= [0 1 0]x + [0 1 0]y + [0 1 1]z + [3] = f(.(x,.(y,z))) [0 0 0] [0 0 0] [0 0 1] [0] [0 0 0] [0 0 0] [0 0 1] [0] [1 0 0] [1 0 0] [1 0 0] [2] [1 0 0] [1 0 0] [1 0 0] [2] g(.(x,.(y,z))) = [0 1 0]x + [0 1 0]y + [0 1 0]z + [7] >= [0 1 0]x + [0 1 0]y + [0 1 0]z + [7] = g(.(.(x,y),z)) [0 0 0] [0 0 0] [0 0 0] [4] [0 0 0] [0 0 0] [0 0 0] [4] [1 0 0] [2] [1 0 0] [2] g(.(x,nil())) = [0 1 0]x + [8] >= [0 1 0]x + [8] = .(g(x),nil()) [0 0 0] [4] [0 0 0] [3] [2] [0] g(nil()) = [8] >= [1] = nil() [4] [3] [1] [0] f(nil()) = [7] >= [1] = nil() [3] [3] problem: strict: f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(.(x,.(y,z))) -> g(.(.(x,y),z)) weak: f(.(nil(),y)) -> .(nil(),f(y)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() f(nil()) -> nil() Matrix Interpretation Processor: dimension: 3 interpretation: [1 4 0] [0] [g](x0) = [0 0 2]x0 + [0] [0 0 1] [2], [1 0 0] [0] [.](x0, x1) = x0 + [0 0 1]x1 + [0] [0 0 1] [2], [1 0 0] [5] [f](x0) = [0 0 2]x0 + [1] [0 0 1] [0], [1] [nil] = [0] [3] orientation: [1 0 0] [1 0 0] [1 0 0] [5] [1 0 0] [1 0 0] [1 0 0] [5] f(.(.(x,y),z)) = [0 0 2]x + [0 0 2]y + [0 0 2]z + [9] >= [0 0 2]x + [0 0 2]y + [0 0 2]z + [9] = f(.(x,.(y,z))) [0 0 1] [0 0 1] [0 0 1] [4] [0 0 1] [0 0 1] [0 0 1] [4] [1 4 0] [1 0 4] [1 0 4] [8] [1 4 0] [1 0 4] [1 0 4] [0] g(.(x,.(y,z))) = [0 0 2]x + [0 0 2]y + [0 0 2]z + [8] >= [0 0 2]x + [0 0 2]y + [0 0 2]z + [8] = g(.(.(x,y),z)) [0 0 1] [0 0 1] [0 0 1] [6] [0 0 1] [0 0 1] [0 0 1] [6] [1 0 0] [6 ] [1 0 0] [6] f(.(nil(),y)) = [0 0 2]y + [11] >= [0 0 1]y + [0] = .(nil(),f(y)) [0 0 1] [5 ] [0 0 1] [5] [1 4 0] [13] [1 4 0] [1] g(.(x,nil())) = [0 0 2]x + [10] >= [0 0 2]x + [3] = .(g(x),nil()) [0 0 1] [7 ] [0 0 1] [7] [1] [1] g(nil()) = [6] >= [0] = nil() [5] [3] [6] [1] f(nil()) = [7] >= [0] = nil() [3] [3] problem: strict: f(.(.(x,y),z)) -> f(.(x,.(y,z))) weak: g(.(x,.(y,z))) -> g(.(.(x,y),z)) f(.(nil(),y)) -> .(nil(),f(y)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() f(nil()) -> nil() Matrix Interpretation Processor: dimension: 3 interpretation: [1 0 4] [1] [g](x0) = [0 0 7]x0 + [1] [0 0 1] [2], [1 0 0] [0] [.](x0, x1) = [0 0 6]x0 + x1 + [0] [0 0 1] [1], [1 2 0] [f](x0) = [0 0 4]x0 [0 0 1] , [0] [nil] = [2] [1] orientation: [1 0 12] [1 0 12] [1 2 0] [12] [1 0 12] [1 0 12] [1 2 0] [0] f(.(.(x,y),z)) = [0 0 4 ]x + [0 0 4 ]y + [0 0 4]z + [8 ] >= [0 0 4 ]x + [0 0 4 ]y + [0 0 4]z + [8] = f(.(x,.(y,z))) [0 0 1 ] [0 0 1 ] [0 0 1] [2 ] [0 0 1 ] [0 0 1 ] [0 0 1] [2] [1 0 4] [1 0 4] [1 0 4] [9 ] [1 0 4] [1 0 4] [1 0 4] [9 ] g(.(x,.(y,z))) = [0 0 7]x + [0 0 7]y + [0 0 7]z + [15] >= [0 0 7]x + [0 0 7]y + [0 0 7]z + [15] = g(.(.(x,y),z)) [0 0 1] [0 0 1] [0 0 1] [4 ] [0 0 1] [0 0 1] [0 0 1] [4 ] [1 2 0] [12] [1 2 0] [0] f(.(nil(),y)) = [0 0 4]y + [8 ] >= [0 0 4]y + [6] = .(nil(),f(y)) [0 0 1] [2 ] [0 0 1] [2] [1 0 4] [9 ] [1 0 4] [1 ] g(.(x,nil())) = [0 0 7]x + [15] >= [0 0 6]x + [14] = .(g(x),nil()) [0 0 1] [4 ] [0 0 1] [4 ] [5] [0] g(nil()) = [8] >= [2] = nil() [3] [1] [4] [0] f(nil()) = [4] >= [2] = nil() [1] [1] problem: strict: weak: f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(.(x,.(y,z))) -> g(.(.(x,y),z)) f(.(nil(),y)) -> .(nil(),f(y)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() f(nil()) -> nil() Qed