YES(?,O(n^2)) 83.64/41.70 YES(?,O(n^2)) 83.64/41.70 83.64/41.70 Problem: 83.64/41.70 a__f(f(X)) -> a__c(f(g(f(X)))) 83.64/41.70 a__c(X) -> d(X) 83.64/41.70 a__h(X) -> a__c(d(X)) 83.64/41.70 mark(f(X)) -> a__f(mark(X)) 83.64/41.70 mark(c(X)) -> a__c(X) 83.64/41.70 mark(h(X)) -> a__h(mark(X)) 83.64/41.70 mark(g(X)) -> g(X) 83.64/41.70 mark(d(X)) -> d(X) 83.64/41.70 a__f(X) -> f(X) 83.64/41.70 a__c(X) -> c(X) 83.64/41.70 a__h(X) -> h(X) 83.64/41.70 83.64/41.70 Proof: 83.64/41.70 Complexity Transformation Processor: 83.64/41.70 strict: 83.64/41.70 a__f(f(X)) -> a__c(f(g(f(X)))) 83.64/41.70 a__c(X) -> d(X) 83.64/41.70 a__h(X) -> a__c(d(X)) 83.64/41.70 mark(f(X)) -> a__f(mark(X)) 83.64/41.70 mark(c(X)) -> a__c(X) 83.64/41.70 mark(h(X)) -> a__h(mark(X)) 83.64/41.70 mark(g(X)) -> g(X) 83.64/41.70 mark(d(X)) -> d(X) 83.64/41.70 a__f(X) -> f(X) 83.64/41.70 a__c(X) -> c(X) 83.64/41.70 a__h(X) -> h(X) 83.64/41.70 weak: 83.64/41.70 83.64/41.70 Matrix Interpretation Processor: dim=1 83.64/41.70 83.64/41.70 max_matrix: 83.64/41.70 1 83.64/41.70 interpretation: 83.64/41.70 [h](x0) = x0, 83.64/41.70 83.64/41.70 [c](x0) = x0 + 72, 83.64/41.70 83.64/41.70 [mark](x0) = x0 + 224, 83.64/41.70 83.64/41.70 [a__h](x0) = x0 + 1, 83.64/41.70 83.64/41.70 [d](x0) = x0 + 4, 83.64/41.70 83.64/41.70 [a__c](x0) = x0 + 252, 83.64/41.70 83.64/41.70 [g](x0) = x0 + 32, 83.64/41.70 83.64/41.70 [a__f](x0) = x0 + 157, 83.64/41.70 83.64/41.70 [f](x0) = x0 + 12 83.64/41.70 orientation: 83.64/41.70 a__f(f(X)) = X + 169 >= X + 308 = a__c(f(g(f(X)))) 83.64/41.70 83.64/41.70 a__c(X) = X + 252 >= X + 4 = d(X) 83.64/41.70 83.64/41.70 a__h(X) = X + 1 >= X + 256 = a__c(d(X)) 83.64/41.70 83.64/41.70 mark(f(X)) = X + 236 >= X + 381 = a__f(mark(X)) 83.64/41.70 83.64/41.70 mark(c(X)) = X + 296 >= X + 252 = a__c(X) 83.64/41.70 83.64/41.70 mark(h(X)) = X + 224 >= X + 225 = a__h(mark(X)) 83.64/41.70 83.64/41.70 mark(g(X)) = X + 256 >= X + 32 = g(X) 83.64/41.70 83.64/41.70 mark(d(X)) = X + 228 >= X + 4 = d(X) 83.64/41.70 83.64/41.70 a__f(X) = X + 157 >= X + 12 = f(X) 83.64/41.70 83.64/41.70 a__c(X) = X + 252 >= X + 72 = c(X) 83.64/41.70 83.64/41.70 a__h(X) = X + 1 >= X = h(X) 83.64/41.70 problem: 83.64/41.70 strict: 83.64/41.70 a__f(f(X)) -> a__c(f(g(f(X)))) 83.64/41.70 a__h(X) -> a__c(d(X)) 83.64/41.70 mark(f(X)) -> a__f(mark(X)) 83.64/41.70 mark(h(X)) -> a__h(mark(X)) 83.64/41.70 weak: 83.64/41.70 a__c(X) -> d(X) 83.64/41.70 mark(c(X)) -> a__c(X) 83.64/41.70 mark(g(X)) -> g(X) 83.64/41.70 mark(d(X)) -> d(X) 83.64/41.70 a__f(X) -> f(X) 83.64/41.70 a__c(X) -> c(X) 83.64/41.70 a__h(X) -> h(X) 83.64/41.70 Matrix Interpretation Processor: dim=1 83.64/41.70 83.64/41.70 max_matrix: 83.64/41.70 1 83.64/41.70 interpretation: 83.64/41.70 [h](x0) = x0 + 9, 83.64/41.70 83.64/41.70 [c](x0) = x0 + 4, 83.64/41.70 83.64/41.70 [mark](x0) = x0, 83.64/41.70 83.64/41.70 [a__h](x0) = x0 + 11, 83.64/41.70 83.64/41.70 [d](x0) = x0 + 4, 83.64/41.70 83.64/41.70 [a__c](x0) = x0 + 4, 83.64/41.70 83.64/41.70 [g](x0) = x0, 83.64/41.70 83.64/41.70 [a__f](x0) = x0 + 1, 83.64/41.70 83.64/41.70 [f](x0) = x0 + 1 83.64/41.70 orientation: 83.64/41.70 a__f(f(X)) = X + 2 >= X + 6 = a__c(f(g(f(X)))) 83.64/41.70 83.64/41.70 a__h(X) = X + 11 >= X + 8 = a__c(d(X)) 83.64/41.70 83.64/41.70 mark(f(X)) = X + 1 >= X + 1 = a__f(mark(X)) 83.64/41.70 83.64/41.70 mark(h(X)) = X + 9 >= X + 11 = a__h(mark(X)) 83.64/41.70 83.64/41.70 a__c(X) = X + 4 >= X + 4 = d(X) 83.64/41.70 83.64/41.70 mark(c(X)) = X + 4 >= X + 4 = a__c(X) 83.64/41.70 83.64/41.70 mark(g(X)) = X >= X = g(X) 83.64/41.70 83.64/41.70 mark(d(X)) = X + 4 >= X + 4 = d(X) 83.64/41.70 83.64/41.70 a__f(X) = X + 1 >= X + 1 = f(X) 83.64/41.70 83.64/41.70 a__c(X) = X + 4 >= X + 4 = c(X) 83.64/41.70 83.64/41.70 a__h(X) = X + 11 >= X + 9 = h(X) 83.64/41.70 problem: 83.64/41.70 strict: 83.64/41.70 a__f(f(X)) -> a__c(f(g(f(X)))) 83.64/41.70 mark(f(X)) -> a__f(mark(X)) 83.64/41.70 mark(h(X)) -> a__h(mark(X)) 83.64/41.70 weak: 83.64/41.70 a__h(X) -> a__c(d(X)) 83.64/41.70 a__c(X) -> d(X) 83.64/41.70 mark(c(X)) -> a__c(X) 83.64/41.70 mark(g(X)) -> g(X) 83.64/41.70 mark(d(X)) -> d(X) 83.64/41.70 a__f(X) -> f(X) 83.64/41.70 a__c(X) -> c(X) 83.64/41.70 a__h(X) -> h(X) 83.64/41.70 Matrix Interpretation Processor: dim=1 83.64/41.70 83.64/41.70 max_matrix: 83.74/41.70 1 83.74/41.70 interpretation: 83.74/41.70 [h](x0) = x0 + 25, 83.74/41.70 83.74/41.70 [c](x0) = x0 + 78, 83.74/41.70 83.74/41.70 [mark](x0) = x0 + 4, 83.74/41.70 83.74/41.70 [a__h](x0) = x0 + 162, 83.74/41.70 83.74/41.70 [d](x0) = x0 + 81, 83.74/41.70 83.74/41.70 [a__c](x0) = x0 + 81, 83.74/41.70 83.74/41.70 [g](x0) = x0 + 18, 83.74/41.70 83.74/41.70 [a__f](x0) = x0 + 128, 83.74/41.70 83.74/41.70 [f](x0) = x0 + 9 83.74/41.70 orientation: 83.74/41.70 a__f(f(X)) = X + 137 >= X + 117 = a__c(f(g(f(X)))) 83.74/41.70 83.74/41.70 mark(f(X)) = X + 13 >= X + 132 = a__f(mark(X)) 83.74/41.70 83.74/41.70 mark(h(X)) = X + 29 >= X + 166 = a__h(mark(X)) 83.74/41.70 83.74/41.70 a__h(X) = X + 162 >= X + 162 = a__c(d(X)) 83.74/41.70 83.74/41.70 a__c(X) = X + 81 >= X + 81 = d(X) 83.74/41.70 83.74/41.70 mark(c(X)) = X + 82 >= X + 81 = a__c(X) 83.74/41.70 83.74/41.70 mark(g(X)) = X + 22 >= X + 18 = g(X) 83.74/41.70 83.74/41.70 mark(d(X)) = X + 85 >= X + 81 = d(X) 83.74/41.70 83.74/41.70 a__f(X) = X + 128 >= X + 9 = f(X) 83.74/41.70 83.74/41.70 a__c(X) = X + 81 >= X + 78 = c(X) 83.74/41.70 83.74/41.70 a__h(X) = X + 162 >= X + 25 = h(X) 83.74/41.70 problem: 83.74/41.70 strict: 83.74/41.70 mark(f(X)) -> a__f(mark(X)) 83.74/41.70 mark(h(X)) -> a__h(mark(X)) 83.74/41.70 weak: 83.74/41.71 a__f(f(X)) -> a__c(f(g(f(X)))) 83.74/41.71 a__h(X) -> a__c(d(X)) 83.74/41.71 a__c(X) -> d(X) 83.74/41.71 mark(c(X)) -> a__c(X) 83.74/41.71 mark(g(X)) -> g(X) 83.74/41.71 mark(d(X)) -> d(X) 83.74/41.71 a__f(X) -> f(X) 83.74/41.71 a__c(X) -> c(X) 83.74/41.71 a__h(X) -> h(X) 83.74/41.71 Matrix Interpretation Processor: dim=4 83.74/41.71 83.74/41.71 max_matrix: 83.74/41.71 [1 1 1 1] 83.74/41.71 [0 0 0 0] 83.74/41.71 [0 0 0 0] 83.74/41.71 [0 0 0 1] 83.74/41.71 interpretation: 83.74/41.71 [1 1 1 0] [0] 83.74/41.71 [0 0 0 0] [0] 83.74/41.71 [h](x0) = [0 0 0 0]x0 + [0] 83.74/41.71 [0 0 0 1] [1], 83.74/41.71 83.74/41.71 [1 0 1 0] 83.74/41.71 [0 0 0 0] 83.74/41.71 [c](x0) = [0 0 0 0]x0 83.74/41.71 [0 0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0 1] 83.74/41.71 [0 0 0 0] 83.74/41.71 [mark](x0) = [0 0 0 0]x0 83.74/41.71 [0 0 0 1] , 83.74/41.71 83.74/41.71 [1 1 1 0] [0] 83.74/41.71 [0 0 0 0] [0] 83.74/41.71 [a__h](x0) = [0 0 0 0]x0 + [0] 83.74/41.71 [0 0 0 1] [1], 83.74/41.71 83.74/41.71 [1 0 1 0] 83.74/41.71 [0 0 0 0] 83.74/41.71 [d](x0) = [0 0 0 0]x0 83.74/41.71 [0 0 0 0] , 83.74/41.71 83.74/41.71 [1 0 1 0] 83.74/41.71 [0 0 0 0] 83.74/41.71 [a__c](x0) = [0 0 0 0]x0 83.74/41.71 [0 0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0 0] [0] 83.74/41.71 [0 0 0 0] [0] 83.74/41.71 [g](x0) = [0 0 0 0]x0 + [0] 83.74/41.71 [0 0 0 0] [1], 83.74/41.71 83.74/41.71 [1 1 1 0] 83.74/41.71 [0 0 0 0] 83.74/41.71 [a__f](x0) = [0 0 0 0]x0 83.74/41.71 [0 0 0 1] , 83.74/41.71 83.74/41.71 [1 0 0 0] 83.74/41.71 [0 0 0 0] 83.74/41.71 [f](x0) = [0 0 0 0]x0 83.74/41.71 [0 0 0 1] 83.74/41.71 orientation: 83.74/41.71 [1 0 0 1] [1 0 0 1] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 mark(f(X)) = [0 0 0 0]X >= [0 0 0 0]X = a__f(mark(X)) 83.74/41.71 [0 0 0 1] [0 0 0 1] 83.74/41.71 83.74/41.71 [1 1 1 1] [1] [1 0 0 1] [0] 83.74/41.71 [0 0 0 0] [0] [0 0 0 0] [0] 83.74/41.71 mark(h(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__h(mark(X)) 83.74/41.71 [0 0 0 1] [1] [0 0 0 1] [1] 83.74/41.71 83.74/41.71 [1 0 0 0] [1 0 0 0] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 a__f(f(X)) = [0 0 0 0]X >= [0 0 0 0]X = a__c(f(g(f(X)))) 83.74/41.71 [0 0 0 1] [0 0 0 0] 83.74/41.71 83.74/41.71 [1 1 1 0] [0] [1 0 1 0] 83.74/41.71 [0 0 0 0] [0] [0 0 0 0] 83.74/41.71 a__h(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X = a__c(d(X)) 83.74/41.71 [0 0 0 1] [1] [0 0 0 0] 83.74/41.71 83.74/41.71 [1 0 1 0] [1 0 1 0] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 a__c(X) = [0 0 0 0]X >= [0 0 0 0]X = d(X) 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 83.74/41.71 [1 0 1 0] [1 0 1 0] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 mark(c(X)) = [0 0 0 0]X >= [0 0 0 0]X = a__c(X) 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 83.74/41.71 [1 0 0 0] [1] [1 0 0 0] [0] 83.74/41.71 [0 0 0 0] [0] [0 0 0 0] [0] 83.74/41.71 mark(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(X) 83.74/41.71 [0 0 0 0] [1] [0 0 0 0] [1] 83.74/41.71 83.74/41.71 [1 0 1 0] [1 0 1 0] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 mark(d(X)) = [0 0 0 0]X >= [0 0 0 0]X = d(X) 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 83.74/41.71 [1 1 1 0] [1 0 0 0] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 a__f(X) = [0 0 0 0]X >= [0 0 0 0]X = f(X) 83.74/41.71 [0 0 0 1] [0 0 0 1] 83.74/41.71 83.74/41.71 [1 0 1 0] [1 0 1 0] 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 a__c(X) = [0 0 0 0]X >= [0 0 0 0]X = c(X) 83.74/41.71 [0 0 0 0] [0 0 0 0] 83.74/41.71 83.74/41.71 [1 1 1 0] [0] [1 1 1 0] [0] 83.74/41.71 [0 0 0 0] [0] [0 0 0 0] [0] 83.74/41.71 a__h(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = h(X) 83.74/41.71 [0 0 0 1] [1] [0 0 0 1] [1] 83.74/41.71 problem: 83.74/41.71 strict: 83.74/41.71 mark(f(X)) -> a__f(mark(X)) 83.74/41.71 weak: 83.74/41.71 mark(h(X)) -> a__h(mark(X)) 83.74/41.71 a__f(f(X)) -> a__c(f(g(f(X)))) 83.74/41.71 a__h(X) -> a__c(d(X)) 83.74/41.71 a__c(X) -> d(X) 83.74/41.71 mark(c(X)) -> a__c(X) 83.74/41.71 mark(g(X)) -> g(X) 83.74/41.71 mark(d(X)) -> d(X) 83.74/41.71 a__f(X) -> f(X) 83.74/41.71 a__c(X) -> c(X) 83.74/41.71 a__h(X) -> h(X) 83.74/41.71 Matrix Interpretation Processor: dim=3 83.74/41.71 83.74/41.71 max_matrix: 83.74/41.71 [1 1 0] 83.74/41.71 [0 1 1] 83.74/41.71 [0 0 0] 83.74/41.71 interpretation: 83.74/41.71 [1 0 0] 83.74/41.71 [h](x0) = [0 1 0]x0 83.74/41.71 [0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0] 83.74/41.71 [c](x0) = [0 1 1]x0 83.74/41.71 [0 0 0] , 83.74/41.71 83.74/41.71 [1 1 0] [0] 83.74/41.71 [mark](x0) = [0 1 0]x0 + [0] 83.74/41.71 [0 0 0] [1], 83.74/41.71 83.74/41.71 [1 0 0] 83.74/41.71 [a__h](x0) = [0 1 0]x0 83.74/41.71 [0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0] 83.74/41.71 [d](x0) = [0 0 0]x0 83.74/41.71 [0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0] 83.74/41.71 [a__c](x0) = [0 1 1]x0 83.74/41.71 [0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0] 83.74/41.71 [g](x0) = [0 0 0]x0 83.74/41.71 [0 0 0] , 83.74/41.71 83.74/41.71 [1 0 0] [0] 83.74/41.71 [a__f](x0) = [0 1 0]x0 + [1] 83.74/41.71 [0 0 0] [1], 83.74/41.71 83.74/41.71 [1 0 0] [0] 83.74/41.71 [f](x0) = [0 1 0]x0 + [1] 83.74/41.71 [0 0 0] [0] 83.74/41.71 orientation: 83.74/41.71 [1 1 0] [1] [1 1 0] [0] 83.74/41.71 mark(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = a__f(mark(X)) 83.74/41.71 [0 0 0] [1] [0 0 0] [1] 83.74/41.71 83.74/41.71 [1 1 0] [0] [1 1 0] 83.74/41.71 mark(h(X)) = [0 1 0]X + [0] >= [0 1 0]X = a__h(mark(X)) 83.74/41.71 [0 0 0] [1] [0 0 0] 83.74/41.71 83.74/41.71 [1 0 0] [0] [1 0 0] [0] 83.74/41.71 a__f(f(X)) = [0 1 0]X + [2] >= [0 0 0]X + [1] = a__c(f(g(f(X)))) 83.74/41.71 [0 0 0] [1] [0 0 0] [0] 83.74/41.71 83.74/41.71 [1 0 0] [1 0 0] 83.74/41.71 a__h(X) = [0 1 0]X >= [0 0 0]X = a__c(d(X)) 83.74/41.71 [0 0 0] [0 0 0] 83.74/41.71 83.74/41.71 [1 0 0] [1 0 0] 83.74/41.71 a__c(X) = [0 1 1]X >= [0 0 0]X = d(X) 83.74/41.71 [0 0 0] [0 0 0] 83.74/41.71 83.74/41.71 [1 1 1] [0] [1 0 0] 83.74/41.71 mark(c(X)) = [0 1 1]X + [0] >= [0 1 1]X = a__c(X) 83.74/41.71 [0 0 0] [1] [0 0 0] 83.74/41.71 83.74/41.71 [1 0 0] [0] [1 0 0] 83.74/41.71 mark(g(X)) = [0 0 0]X + [0] >= [0 0 0]X = g(X) 83.74/41.71 [0 0 0] [1] [0 0 0] 83.74/41.71 83.74/41.71 [1 0 0] [0] [1 0 0] 83.74/41.71 mark(d(X)) = [0 0 0]X + [0] >= [0 0 0]X = d(X) 83.74/41.71 [0 0 0] [1] [0 0 0] 83.74/41.71 83.74/41.71 [1 0 0] [0] [1 0 0] [0] 83.74/41.71 a__f(X) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(X) 83.74/41.71 [0 0 0] [1] [0 0 0] [0] 83.74/41.71 83.74/41.71 [1 0 0] [1 0 0] 83.74/41.71 a__c(X) = [0 1 1]X >= [0 1 1]X = c(X) 83.74/41.71 [0 0 0] [0 0 0] 83.74/41.71 83.74/41.71 [1 0 0] [1 0 0] 83.74/41.71 a__h(X) = [0 1 0]X >= [0 1 0]X = h(X) 83.74/41.71 [0 0 0] [0 0 0] 83.74/41.71 problem: 83.74/41.71 strict: 83.74/41.71 83.74/41.71 weak: 83.74/41.71 mark(f(X)) -> a__f(mark(X)) 83.74/41.71 mark(h(X)) -> a__h(mark(X)) 83.74/41.71 a__f(f(X)) -> a__c(f(g(f(X)))) 83.74/41.71 a__h(X) -> a__c(d(X)) 83.74/41.71 a__c(X) -> d(X) 83.74/41.71 mark(c(X)) -> a__c(X) 83.74/41.71 mark(g(X)) -> g(X) 83.74/41.71 mark(d(X)) -> d(X) 83.74/41.71 a__f(X) -> f(X) 83.74/41.71 a__c(X) -> c(X) 83.74/41.71 a__h(X) -> h(X) 83.74/41.71 Qed 83.74/41.72 EOF