YES(?,O(n^3)) 104.34/46.92 YES(?,O(n^3)) 104.34/46.93 104.34/46.93 Problem: 104.34/46.93 f(nil()) -> nil() 104.34/46.93 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.93 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.93 g(nil()) -> nil() 104.34/46.93 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.93 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.93 104.34/46.93 Proof: 104.34/46.93 Complexity Transformation Processor: 104.34/46.93 strict: 104.34/46.93 f(nil()) -> nil() 104.34/46.93 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.93 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.93 g(nil()) -> nil() 104.34/46.93 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.93 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.93 weak: 104.34/46.93 104.34/46.93 Matrix Interpretation Processor: dim=1 104.34/46.93 104.34/46.93 max_matrix: 104.34/46.93 1 104.34/46.93 interpretation: 104.34/46.93 [g](x0) = x0, 104.34/46.93 104.34/46.93 [.](x0, x1) = x0 + x1 + 8, 104.34/46.93 104.34/46.93 [f](x0) = x0 + 4, 104.34/46.93 104.34/46.93 [nil] = 15 104.34/46.93 orientation: 104.34/46.93 f(nil()) = 19 >= 15 = nil() 104.34/46.93 104.34/46.93 f(.(nil(),y)) = y + 27 >= y + 27 = .(nil(),f(y)) 104.34/46.93 104.34/46.93 f(.(.(x,y),z)) = x + y + z + 20 >= x + y + z + 20 = f(.(x,.(y,z))) 104.34/46.93 104.34/46.93 g(nil()) = 15 >= 15 = nil() 104.34/46.93 104.34/46.93 g(.(x,nil())) = x + 23 >= x + 23 = .(g(x),nil()) 104.34/46.93 104.34/46.93 g(.(x,.(y,z))) = x + y + z + 16 >= x + y + z + 16 = g(.(.(x,y),z)) 104.34/46.93 problem: 104.34/46.93 strict: 104.34/46.93 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.93 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.93 g(nil()) -> nil() 104.34/46.93 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.93 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.93 weak: 104.34/46.93 f(nil()) -> nil() 104.34/46.93 Matrix Interpretation Processor: dim=1 104.34/46.93 104.34/46.93 max_matrix: 104.34/46.93 1 104.34/46.93 interpretation: 104.34/46.93 [g](x0) = x0 + 12, 104.34/46.93 104.34/46.93 [.](x0, x1) = x0 + x1 + 4, 104.34/46.93 104.34/46.93 [f](x0) = x0, 104.34/46.93 104.34/46.93 [nil] = 12 104.34/46.93 orientation: 104.34/46.93 f(.(nil(),y)) = y + 16 >= y + 16 = .(nil(),f(y)) 104.34/46.93 104.34/46.93 f(.(.(x,y),z)) = x + y + z + 8 >= x + y + z + 8 = f(.(x,.(y,z))) 104.34/46.93 104.34/46.93 g(nil()) = 24 >= 12 = nil() 104.34/46.93 104.34/46.93 g(.(x,nil())) = x + 28 >= x + 28 = .(g(x),nil()) 104.34/46.93 104.34/46.93 g(.(x,.(y,z))) = x + y + z + 20 >= x + y + z + 20 = g(.(.(x,y),z)) 104.34/46.93 104.34/46.93 f(nil()) = 12 >= 12 = nil() 104.34/46.93 problem: 104.34/46.93 strict: 104.34/46.93 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.93 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.93 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.93 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.93 weak: 104.34/46.93 g(nil()) -> nil() 104.34/46.93 f(nil()) -> nil() 104.34/46.93 Matrix Interpretation Processor: dim=4 104.34/46.93 104.34/46.93 max_matrix: 104.34/46.93 [1 0 1 0] 104.34/46.93 [0 0 1 1] 104.34/46.93 [0 0 1 0] 104.34/46.93 [0 0 0 0] 104.34/46.93 interpretation: 104.34/46.93 [1 0 1 0] 104.34/46.93 [0 0 1 0] 104.34/46.93 [g](x0) = [0 0 1 0]x0 104.34/46.93 [0 0 0 0] , 104.34/46.93 104.34/46.93 [1 0 0 0] [1 0 0 0] [1] 104.34/46.93 [0 0 0 0] [0 0 1 1] [0] 104.34/46.93 [.](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 + [0] 104.34/46.93 [0 0 0 0] [0 0 0 0] [0], 104.34/46.93 104.34/46.93 [1 0 0 0] [0] 104.34/46.93 [0 0 1 1] [1] 104.34/46.93 [f](x0) = [0 0 1 0]x0 + [1] 104.34/46.93 [0 0 0 0] [1], 104.34/46.93 104.34/46.93 [0] 104.34/46.93 [0] 104.34/46.93 [nil] = [1] 104.34/46.93 [0] 104.34/46.93 orientation: 104.34/46.93 [1 0 0 0] [1] [1 0 0 0] [1] 104.34/46.93 [0 0 1 0] [2] [0 0 1 0] [2] 104.34/46.93 f(.(nil(),y)) = [0 0 1 0]y + [2] >= [0 0 1 0]y + [2] = .(nil(),f(y)) 104.34/46.93 [0 0 0 0] [1] [0 0 0 0] [0] 104.34/46.93 104.34/46.93 [1 0 0 0] [1 0 0 0] [1 0 0 0] [2] [1 0 0 0] [1 0 0 0] [1 0 0 0] [2] 104.34/46.93 [0 0 1 0] [0 0 1 0] [0 0 1 0] [1] [0 0 1 0] [0 0 1 0] [0 0 1 0] [1] 104.34/46.93 f(.(.(x,y),z)) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [1] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [1] = f(.(x,.(y,z))) 104.34/46.93 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] 104.34/46.93 104.34/46.93 [1 0 1 0] [2] [1 0 1 0] [1] 104.34/46.93 [0 0 1 0] [1] [0 0 0 0] [1] 104.34/46.93 g(.(x,nil())) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = .(g(x),nil()) 104.34/46.93 [0 0 0 0] [0] [0 0 0 0] [0] 104.34/46.93 104.34/46.93 [1 0 1 0] [1 0 1 0] [1 0 1 0] [2] [1 0 1 0] [1 0 1 0] [1 0 1 0] [2] 104.34/46.93 [0 0 1 0] [0 0 1 0] [0 0 1 0] [0] [0 0 1 0] [0 0 1 0] [0 0 1 0] [0] 104.34/46.94 g(.(x,.(y,z))) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [0] = g(.(.(x,y),z)) 104.34/46.94 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 104.34/46.94 104.34/46.94 [1] [0] 104.34/46.94 [1] [0] 104.34/46.94 g(nil()) = [1] >= [1] = nil() 104.34/46.94 [0] [0] 104.34/46.94 104.34/46.94 [0] [0] 104.34/46.94 [2] [0] 104.34/46.94 f(nil()) = [2] >= [1] = nil() 104.34/46.94 [1] [0] 104.34/46.94 problem: 104.34/46.94 strict: 104.34/46.94 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.94 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.94 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.94 weak: 104.34/46.94 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.94 g(nil()) -> nil() 104.34/46.94 f(nil()) -> nil() 104.34/46.94 Splitting Processor: 104.34/46.94 strict: 104.34/46.94 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.94 weak: 104.34/46.94 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.94 g(nil()) -> nil() 104.34/46.94 f(nil()) -> nil() 104.34/46.94 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.94 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.94 Matrix Interpretation Processor: dim=3 104.34/46.94 104.34/46.94 max_matrix: 104.34/46.94 [1 1 0] 104.34/46.94 [0 1 0] 104.34/46.94 [0 0 0] 104.34/46.94 interpretation: 104.34/46.94 [1 0 0] [0] 104.34/46.94 [g](x0) = [0 1 0]x0 + [1] 104.34/46.94 [0 0 0] [1], 104.34/46.94 104.34/46.94 [1 0 0] [1 0 0] [0] 104.34/46.94 [.](x0, x1) = [0 1 0]x0 + [0 1 0]x1 + [1] 104.34/46.94 [0 0 0] [0 0 0] [0], 104.34/46.94 104.34/46.94 [1 1 0] [1] 104.34/46.94 [f](x0) = [0 1 0]x0 + [0] 104.34/46.94 [0 0 0] [1], 104.34/46.94 104.34/46.94 [0] 104.34/46.94 [nil] = [1] 104.34/46.94 [0] 104.34/46.94 orientation: 104.34/46.94 [1 1 0] [3] [1 1 0] [1] 104.34/46.94 f(.(nil(),y)) = [0 1 0]y + [2] >= [0 1 0]y + [2] = .(nil(),f(y)) 104.34/46.94 [0 0 0] [1] [0 0 0] [0] 104.34/46.94 104.34/46.94 [1 0 0] [0] [1 0 0] [0] 104.34/46.94 g(.(x,nil())) = [0 1 0]x + [3] >= [0 1 0]x + [3] = .(g(x),nil()) 104.34/46.94 [0 0 0] [1] [0 0 0] [0] 104.34/46.94 104.34/46.94 [0] [0] 104.34/46.94 g(nil()) = [2] >= [1] = nil() 104.34/46.94 [1] [0] 104.34/46.94 104.34/46.94 [2] [0] 104.34/46.94 f(nil()) = [1] >= [1] = nil() 104.34/46.94 [1] [0] 104.34/46.94 104.34/46.94 [1 1 0] [1 1 0] [1 1 0] [3] [1 1 0] [1 1 0] [1 1 0] [3] 104.34/46.94 f(.(.(x,y),z)) = [0 1 0]x + [0 1 0]y + [0 1 0]z + [2] >= [0 1 0]x + [0 1 0]y + [0 1 0]z + [2] = f(.(x,.(y,z))) 104.34/46.94 [0 0 0] [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1] 104.34/46.94 104.34/46.94 [1 0 0] [1 0 0] [1 0 0] [0] [1 0 0] [1 0 0] [1 0 0] [0] 104.34/46.94 g(.(x,.(y,z))) = [0 1 0]x + [0 1 0]y + [0 1 0]z + [3] >= [0 1 0]x + [0 1 0]y + [0 1 0]z + [3] = g(.(.(x,y),z)) 104.34/46.94 [0 0 0] [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1] 104.34/46.94 problem: 104.34/46.94 strict: 104.34/46.94 104.34/46.94 weak: 104.34/46.94 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.94 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.94 g(nil()) -> nil() 104.34/46.94 f(nil()) -> nil() 104.34/46.94 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.94 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.94 Qed 104.34/46.94 104.34/46.94 strict: 104.34/46.94 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.94 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.94 weak: 104.34/46.94 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.94 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.94 g(nil()) -> nil() 104.34/46.94 f(nil()) -> nil() 104.34/46.94 Splitting Processor: 104.34/46.94 strict: 104.34/46.94 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.94 weak: 104.34/46.94 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.94 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.94 g(nil()) -> nil() 104.34/46.94 f(nil()) -> nil() 104.34/46.94 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.94 Matrix Interpretation Processor: dim=4 104.34/46.94 104.34/46.94 max_matrix: 104.34/46.94 [1 1 0 0] 104.34/46.94 [0 1 1 0] 104.34/46.94 [0 0 1 0] 104.34/46.94 [0 0 0 0] 104.34/46.94 interpretation: 104.34/46.94 [1 1 0 0] [0] 104.34/46.95 [0 0 0 0] [1] 104.34/46.95 [g](x0) = [0 0 1 0]x0 + [0] 104.34/46.95 [0 0 0 0] [0], 104.34/46.95 104.34/46.95 [1 1 0 0] [1 0 0 0] [0] 104.34/46.95 [0 0 0 0] [0 1 0 0] [1] 104.34/46.95 [.](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 + [0] 104.34/46.95 [0 0 0 0] [0 0 0 0] [0], 104.34/46.95 104.34/46.95 [1 0 0 0] [1] 104.34/46.95 [0 0 1 0] [0] 104.34/46.95 [f](x0) = [0 0 1 0]x0 + [0] 104.34/46.95 [0 0 0 0] [0], 104.34/46.95 104.34/46.95 [0] 104.34/46.95 [0] 104.34/46.95 [nil] = [1] 104.34/46.95 [0] 104.34/46.95 orientation: 104.34/46.95 [1 1 0 0] [1 1 0 0] [1 0 0 0] [2] [1 1 0 0] [1 1 0 0] [1 0 0 0] [1] 104.34/46.95 [0 0 1 0] [0 0 1 0] [0 0 1 0] [0] [0 0 1 0] [0 0 1 0] [0 0 1 0] [0] 104.34/46.95 f(.(.(x,y),z)) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [0] = f(.(x,.(y,z))) 104.34/46.95 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [1 1 0 0] [1 1 0 0] [1 1 0 0] [2] [1 1 0 0] [1 1 0 0] [1 1 0 0] [2] 104.34/46.95 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] 104.34/46.95 g(.(x,.(y,z))) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [0] = g(.(.(x,y),z)) 104.34/46.95 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [1 0 0 0] [1] [1 0 0 0] [1] 104.34/46.95 [0 0 1 0] [1] [0 0 1 0] [1] 104.34/46.95 f(.(nil(),y)) = [0 0 1 0]y + [1] >= [0 0 1 0]y + [1] = .(nil(),f(y)) 104.34/46.95 [0 0 0 0] [0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [1 1 0 0] [1] [1 1 0 0] [1] 104.34/46.95 [0 0 0 0] [1] [0 0 0 0] [1] 104.34/46.95 g(.(x,nil())) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = .(g(x),nil()) 104.34/46.95 [0 0 0 0] [0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [0] [0] 104.34/46.95 [1] [0] 104.34/46.95 g(nil()) = [1] >= [1] = nil() 104.34/46.95 [0] [0] 104.34/46.95 104.34/46.95 [1] [0] 104.34/46.95 [1] [0] 104.34/46.95 f(nil()) = [1] >= [1] = nil() 104.34/46.95 [0] [0] 104.34/46.95 problem: 104.34/46.95 strict: 104.34/46.95 104.34/46.95 weak: 104.34/46.95 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.95 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.95 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.95 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.95 g(nil()) -> nil() 104.34/46.95 f(nil()) -> nil() 104.34/46.95 Qed 104.34/46.95 104.34/46.95 strict: 104.34/46.95 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.95 weak: 104.34/46.95 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.95 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.95 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.95 g(nil()) -> nil() 104.34/46.95 f(nil()) -> nil() 104.34/46.95 Matrix Interpretation Processor: dim=4 104.34/46.95 104.34/46.95 max_matrix: 104.34/46.95 [1 1 0 0] 104.34/46.95 [0 1 1 0] 104.34/46.95 [0 0 1 0] 104.34/46.95 [0 0 0 0] 104.34/46.95 interpretation: 104.34/46.95 [1 1 0 0] [1] 104.34/46.95 [0 0 1 0] [0] 104.34/46.95 [g](x0) = [0 0 1 0]x0 + [1] 104.34/46.95 [0 0 0 0] [0], 104.34/46.95 104.34/46.95 [1 0 0 0] [1 0 0 0] [0] 104.34/46.95 [0 1 0 0] [0 0 1 0] [0] 104.34/46.95 [.](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 + [1] 104.34/46.95 [0 0 0 0] [0 0 0 0] [0], 104.34/46.95 104.34/46.95 [1 0 0 0] [0] 104.34/46.95 [0 0 1 0] [1] 104.34/46.95 [f](x0) = [0 0 1 0]x0 + [0] 104.34/46.95 [0 0 0 0] [0], 104.34/46.95 104.34/46.95 [0] 104.34/46.95 [0] 104.34/46.95 [nil] = [1] 104.34/46.95 [0] 104.34/46.95 orientation: 104.34/46.95 [1 1 0 0] [1 0 1 0] [1 0 1 0] [2] [1 1 0 0] [1 0 1 0] [1 0 1 0] [1] 104.34/46.95 [0 0 1 0] [0 0 1 0] [0 0 1 0] [2] [0 0 1 0] [0 0 1 0] [0 0 1 0] [2] 104.34/46.95 g(.(x,.(y,z))) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [3] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [3] = g(.(.(x,y),z)) 104.34/46.95 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [1 0 0 0] [0] [1 0 0 0] [0] 104.34/46.95 [0 0 1 0] [3] [0 0 1 0] [0] 104.34/46.95 f(.(nil(),y)) = [0 0 1 0]y + [2] >= [0 0 1 0]y + [2] = .(nil(),f(y)) 104.34/46.95 [0 0 0 0] [0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [1 1 0 0] [2] [1 1 0 0] [1] 104.34/46.95 [0 0 1 0] [2] [0 0 1 0] [1] 104.34/46.95 g(.(x,nil())) = [0 0 1 0]x + [3] >= [0 0 1 0]x + [3] = .(g(x),nil()) 104.34/46.95 [0 0 0 0] [0] [0 0 0 0] [0] 104.34/46.95 104.34/46.95 [1] [0] 104.34/46.95 [1] [0] 104.34/46.95 g(nil()) = [2] >= [1] = nil() 104.34/46.95 [0] [0] 104.34/46.95 104.34/46.95 [0] [0] 104.34/46.95 [2] [0] 104.34/46.95 f(nil()) = [1] >= [1] = nil() 104.34/46.95 [0] [0] 104.34/46.95 104.34/46.95 [1 0 0 0] [1 0 0 0] [1 0 0 0] [0] [1 0 0 0] [1 0 0 0] [1 0 0 0] [0] 104.34/46.95 [0 0 1 0] [0 0 1 0] [0 0 1 0] [3] [0 0 1 0] [0 0 1 0] [0 0 1 0] [3] 104.34/46.95 f(.(.(x,y),z)) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] = f(.(x,.(y,z))) 104.34/46.95 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 104.34/46.95 problem: 104.34/46.95 strict: 104.34/46.95 104.34/46.95 weak: 104.34/46.95 g(.(x,.(y,z))) -> g(.(.(x,y),z)) 104.34/46.95 f(.(nil(),y)) -> .(nil(),f(y)) 104.34/46.95 g(.(x,nil())) -> .(g(x),nil()) 104.34/46.95 g(nil()) -> nil() 104.34/46.95 f(nil()) -> nil() 104.34/46.95 f(.(.(x,y),z)) -> f(.(x,.(y,z))) 104.34/46.95 Qed 104.34/46.96 EOF