YES(?,O(n^1)) 47.81/12.59 YES(?,O(n^1)) 47.91/12.60 47.91/12.60 Problem: 47.91/12.60 f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y)) 47.91/12.60 47.91/12.60 Proof: 47.91/12.60 Complexity Transformation Processor: 47.91/12.60 strict: 47.91/12.60 f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y)) 47.91/12.60 weak: 47.91/12.60 47.91/12.60 Root-Labeling Processor: 47.91/12.60 strict: 47.91/12.60 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.60 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.60 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.60 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.60 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.60 weak: 47.91/12.60 47.91/12.60 Matrix Interpretation Processor: dim=2 47.91/12.60 47.91/12.60 max_matrix: 47.91/12.60 [1 2] 47.91/12.60 [0 0] 47.91/12.60 interpretation: 47.91/12.60 [1 1] [1 0] 47.91/12.60 [f(a,a)](x0, x1) = [0 0]x0 + [0 0]x1, 47.91/12.60 47.91/12.60 [1 0] [1 2] [0] 47.91/12.60 [f(f,a)](x0, x1) = [0 0]x0 + [0 0]x1 + [1], 47.91/12.60 47.91/12.60 [0] 47.91/12.60 [a()] = [0], 47.91/12.60 47.91/12.60 [1 1] [1 0] 47.91/12.60 [f(a,f)](x0, x1) = [0 0]x0 + [0 0]x1, 47.91/12.60 47.91/12.60 [1 1] [1 0] 47.91/12.60 [f(f,f)](x0, x1) = [0 0]x0 + [0 0]x1 47.91/12.60 orientation: 47.91/12.60 [2 1] [1 1] [1 0] [1 0] [1 0] [1 0] 47.91/12.60 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 47.91/12.60 [2 1] [1 1] [1 0] [1 1] [1 0] [1 0] 47.91/12.60 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 47.91/12.60 [2 1] [1 0] [1 2] [1] [1 0] [1 0] [1 0] 47.91/12.60 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [0] >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 47.91/12.60 [2 1] [1 0] [1 2] [1] [1 1] [1 0] [1 0] 47.91/12.60 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [0] >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.60 47.91/12.60 [2 1] [1 1] [1 0] [1 0] [1 0] [1 0] 47.91/12.60 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.60 47.91/12.60 [2 1] [1 1] [1 0] [1 1] [1 0] [1 0] 47.91/12.60 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.60 47.91/12.60 [2 1] [1 1] [1 0] [1 0] [1 0] [1 0] 47.91/12.60 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.61 47.91/12.61 [2 1] [1 1] [1 0] [1 1] [1 0] [1 0] 47.91/12.61 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.61 problem: 47.91/12.61 strict: 47.91/12.61 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.61 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.61 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.61 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.61 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.61 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.61 weak: 47.91/12.61 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.61 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.61 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.61 Matrix Interpretation Processor: dim=5 47.91/12.61 47.91/12.61 max_matrix: 47.91/12.61 [1 1 1 1 0] 47.91/12.61 [0 0 1 1 0] 47.91/12.61 [0 0 0 1 1] 47.91/12.61 [0 0 0 0 0] 47.91/12.61 [0 0 0 0 0] 47.91/12.61 interpretation: 47.91/12.61 [1 0 0 0 0] [1 0 0 0 0] [0] 47.91/12.61 [0 0 0 0 0] [0 0 1 1 0] [0] 47.91/12.61 [f(a,a)](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [1] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [1], 47.91/12.61 47.91/12.61 [1 0 0 1 0] [1 0 1 0 0] [0] 47.91/12.61 [0 0 0 0 0] [0 0 0 1 0] [1] 47.91/12.61 [f(f,a)](x0, x1) = [0 0 0 1 1]x0 + [0 0 0 0 1]x1 + [0] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [1] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [0], 47.91/12.61 47.91/12.61 [0] 47.91/12.61 [0] 47.91/12.61 [a()] = [0] 47.91/12.61 [1] 47.91/12.61 [0], 47.91/12.61 47.91/12.61 [1 1 0 0 0] [1 0 0 0 0] [0] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [0] 47.91/12.61 [f(a,f)](x0, x1) = [0 0 0 1 0]x0 + [0 0 0 1 0]x1 + [1] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [0] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] [1], 47.91/12.61 47.91/12.61 [1 1 0 0 0] [1 0 1 0 0] 47.91/12.61 [0 0 0 1 0] [0 0 0 0 0] 47.91/12.61 [f(f,f)](x0, x1) = [0 0 0 1 1]x0 + [0 0 0 1 0]x1 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] 47.91/12.61 [0 0 0 0 0] [0 0 0 0 0] 47.91/12.61 orientation: 47.91/12.61 [2 1 0 2 1] [1 1 0 1 0] [1 0 1 0 0] [2] [1 0 0 2 1] [1 0 0 1 0] [1 0 0 0 0] [2] 47.91/12.61 [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] [0 0 0 0 0] [0] 47.91/12.61 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [0] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.61 [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] [0 0 0 0 0] [0] 47.91/12.61 [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] [0 0 0 0 0] [0] 47.91/12.62 47.91/12.62 [2 1 0 1 0] [1 1 0 1 0] [1 0 1 0 0] [2] [1 0 0 0 0] [1 0 0 1 0] [1 0 0 0 0] [2] 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [0] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 47.91/12.62 [2 1 0 2 1] [1 1 0 0 0] [1 0 0 0 0] [2] [1 0 0 2 1] [1 0 0 0 0] [1 0 0 0 0] [0] 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 47.91/12.62 [2 1 0 1 0] [1 1 0 0 0] [1 0 0 0 0] [2] [1 0 0 0 0] [1 0 0 0 0] [1 0 0 0 0] [0] 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.62 47.91/12.62 [2 1 0 2 1] [1 0 0 0 0] [1 0 1 1 0] [2] [1 0 0 2 1] [1 0 0 0 0] [1 0 1 1 0] [1] 47.91/12.62 [0 0 0 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 0 0 0] [0] 47.91/12.62 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [2] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.62 [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] [0 0 0 0 0] [0] 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 47.91/12.64 [2 1 0 1 0] [1 0 0 0 0] [1 0 1 1 0] [2] [1 0 0 0 0] [1 0 0 0 0] [1 0 1 1 0] [1] 47.91/12.64 [0 0 0 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 0 0 0] [0] 47.91/12.64 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [2] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 47.91/12.64 [2 1 0 2 1] [1 0 0 1 0] [1 0 1 1 0] [3] [1 0 0 2 1] [1 0 0 1 0] [1 0 1 1 0] [3] 47.91/12.64 [0 0 0 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 0 0 0] [0] 47.91/12.64 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 47.91/12.64 [2 1 0 1 0] [1 0 0 1 0] [1 0 1 1 0] [3] [1 0 0 0 0] [1 0 0 1 0] [1 0 1 1 0] [3] 47.91/12.64 [0 0 0 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 0 0 0] [0] 47.91/12.64 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 [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] [0 0 0 0 0] [0] 47.91/12.64 problem: 47.91/12.64 strict: 47.91/12.64 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 weak: 47.91/12.64 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.64 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 Matrix Interpretation Processor: dim=2 47.91/12.64 47.91/12.64 max_matrix: 47.91/12.64 [1 3] 47.91/12.64 [0 0] 47.91/12.64 interpretation: 47.91/12.64 [1 0] [1 0] 47.91/12.64 [f(a,a)](x0, x1) = [0 0]x0 + [0 0]x1, 47.91/12.64 47.91/12.64 [1 0] [1 0] [2] 47.91/12.64 [f(f,a)](x0, x1) = [0 0]x0 + [0 0]x1 + [2], 47.91/12.64 47.91/12.64 [0] 47.91/12.64 [a()] = [0], 47.91/12.64 47.91/12.64 [1 0] [1 0] 47.91/12.64 [f(a,f)](x0, x1) = [0 0]x0 + [0 0]x1, 47.91/12.64 47.91/12.64 [1 0] [1 3] [0] 47.91/12.64 [f(f,f)](x0, x1) = [0 0]x0 + [0 0]x1 + [3] 47.91/12.64 orientation: 47.91/12.64 [2 0] [1 0] [1 3] [9] [1 0] [1 0] [1 0] [8] 47.91/12.64 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 3] [0] [1 0] [1 0] [1 0] [0] 47.91/12.64 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 0] [9] [1 0] [1 0] [1 0] [8] 47.91/12.64 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 0] [0] [1 0] [1 0] [1 0] [0] 47.91/12.64 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 0] [9] [1 0] [1 0] [1 0] [8] 47.91/12.64 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 0] [0] [1 0] [1 0] [1 0] [0] 47.91/12.64 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 0] [11] [1 0] [1 0] [1 0] [8] 47.91/12.64 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3 ] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.64 47.91/12.64 [2 0] [1 0] [1 0] [2] [1 0] [1 0] [1 0] [0] 47.91/12.65 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0]x + [0 0]y + [0 0]z + [3] >= [0 0]x + [0 0]y + [0 0]z + [3] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 problem: 47.91/12.65 strict: 47.91/12.65 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 weak: 47.91/12.65 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.65 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.65 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.65 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.65 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.65 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 Matrix Interpretation Processor: dim=4 47.91/12.65 47.91/12.65 max_matrix: 47.91/12.65 [1 1 1 1] 47.91/12.65 [0 0 1 1] 47.91/12.65 [0 0 0 0] 47.91/12.65 [0 0 0 0] 47.91/12.65 interpretation: 47.91/12.65 [1 1 1 1] [1 0 0 0] [0] 47.91/12.65 [0 0 1 1] [0 0 0 1] [0] 47.91/12.65 [f(a,a)](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 47.91/12.65 [0 0 0 0] [0 0 0 0] [1], 47.91/12.65 47.91/12.65 [1 0 0 1] [1 0 1 0] [0] 47.91/12.65 [0 0 0 0] [0 0 0 1] [0] 47.91/12.65 [f(f,a)](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [1] 47.91/12.65 [0 0 0 0] [0 0 0 0] [1], 47.91/12.65 47.91/12.65 [0] 47.91/12.65 [0] 47.91/12.65 [a()] = [0] 47.91/12.65 [0], 47.91/12.65 47.91/12.65 [1 1 1 1] [1 0 0 0] [0] 47.91/12.65 [0 0 1 1] [0 0 0 1] [1] 47.91/12.65 [f(a,f)](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 47.91/12.65 [0 0 0 0] [0 0 0 0] [0], 47.91/12.65 47.91/12.65 [1 0 0 1] [1 1 0 0] [0] 47.91/12.65 [0 0 0 0] [0 0 0 0] [1] 47.91/12.65 [f(f,f)](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 47.91/12.65 [0 0 0 0] [0 0 0 0] [1] 47.91/12.65 orientation: 47.91/12.65 [2 1 2 2] [1 0 0 1] [1 1 0 0] [3] [1 1 2 2] [1 0 0 1] [1 0 0 0] [2] 47.91/12.65 [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] 47.91/12.65 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 [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] 47.91/12.65 47.91/12.65 [2 0 0 2] [1 0 0 1] [1 1 0 0] [3] [1 0 0 1] [1 0 0 1] [1 0 0 0] [2] 47.91/12.65 [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] 47.91/12.65 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.65 [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] 47.91/12.66 47.91/12.66 [2 0 0 2] [1 1 1 1] [1 0 0 0] [2] [1 0 0 1] [1 0 0 1] [1 0 0 0] [1] 47.91/12.66 [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] 47.91/12.66 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.66 [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] 47.91/12.66 47.91/12.66 [2 1 2 2] [1 1 1 1] [1 0 0 0] [2] [1 1 2 2] [1 0 0 1] [1 0 0 0] [1] 47.91/12.66 [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] 47.91/12.66 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.66 [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] 47.91/12.66 47.91/12.66 [2 0 0 2] [1 1 1 1] [1 0 0 0] [3] [1 0 0 1] [1 0 0 1] [1 0 0 0] [2] 47.91/12.66 [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] 47.91/12.66 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.66 [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] 47.91/12.66 47.91/12.66 [2 1 2 2] [1 1 1 1] [1 0 0 0] [3] [1 1 2 2] [1 0 0 1] [1 0 0 0] [2] 47.91/12.66 [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] 47.91/12.66 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.66 [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] 47.91/12.66 47.91/12.66 [2 0 0 2] [1 0 0 1] [1 0 1 0] [3] [1 0 0 1] [1 0 0 1] [1 0 0 0] [3] 47.91/12.66 [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] 47.91/12.66 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.67 [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] 47.91/12.67 47.91/12.67 [2 1 2 2] [1 0 0 1] [1 0 1 0] [3] [1 1 2 2] [1 0 0 1] [1 0 0 0] [3] 47.91/12.67 [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] 47.91/12.67 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.67 [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] 47.91/12.67 problem: 47.91/12.67 strict: 47.91/12.67 47.91/12.67 weak: 47.91/12.67 f(f,f)(f(f,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.67 f(f,f)(f(f,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.67 f(f,f)(f(a,f)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.67 f(f,f)(f(a,f)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,f)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.67 f(f,f)(f(a,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.67 f(f,f)(f(a,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,a)(a()(),y)) 47.91/12.67 f(f,f)(f(f,a)(y,z),f(f,f)(x,f(a,f)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(f,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.67 f(f,f)(f(f,a)(y,z),f(a,f)(x,f(a,a)(a()(),x))) -> 47.91/12.67 f(f,f)(f(f,f)(f(a,a)(a()(),z),f(a,a)(x,a()())),f(a,f)(a()(),y)) 47.91/12.67 Qed 47.91/12.67 EOF