YES(?,O(n^1)) 0.16/0.36 YES(?,O(n^1)) 0.16/0.37 0.16/0.37 Problem: 0.16/0.37 a__g(X) -> a__h(X) 0.16/0.37 a__c() -> d() 0.16/0.37 a__h(d()) -> a__g(c()) 0.16/0.37 mark(g(X)) -> a__g(X) 0.16/0.37 mark(h(X)) -> a__h(X) 0.16/0.37 mark(c()) -> a__c() 0.16/0.37 mark(d()) -> d() 0.16/0.37 a__g(X) -> g(X) 0.16/0.37 a__h(X) -> h(X) 0.16/0.37 a__c() -> c() 0.16/0.37 0.16/0.37 Proof: 0.16/0.37 Complexity Transformation Processor: 0.16/0.37 strict: 0.16/0.37 a__g(X) -> a__h(X) 0.16/0.37 a__c() -> d() 0.16/0.37 a__h(d()) -> a__g(c()) 0.16/0.37 mark(g(X)) -> a__g(X) 0.16/0.37 mark(h(X)) -> a__h(X) 0.16/0.37 mark(c()) -> a__c() 0.16/0.37 mark(d()) -> d() 0.16/0.37 a__g(X) -> g(X) 0.16/0.37 a__h(X) -> h(X) 0.16/0.37 a__c() -> c() 0.16/0.37 weak: 0.16/0.37 0.16/0.37 Matrix Interpretation Processor: dim=1 0.16/0.37 0.16/0.37 max_matrix: 0.16/0.37 1 0.16/0.37 interpretation: 0.16/0.37 [h](x0) = x0 + 140, 0.16/0.37 0.16/0.37 [mark](x0) = x0 + 119, 0.16/0.37 0.16/0.37 [g](x0) = x0, 0.16/0.37 0.16/0.37 [c] = 0, 0.16/0.37 0.16/0.37 [d] = 193, 0.16/0.37 0.16/0.37 [a__c] = 1, 0.16/0.37 0.16/0.37 [a__h](x0) = x0 + 71, 0.16/0.37 0.16/0.37 [a__g](x0) = x0 + 16 0.16/0.37 orientation: 0.16/0.37 a__g(X) = X + 16 >= X + 71 = a__h(X) 0.16/0.37 0.16/0.37 a__c() = 1 >= 193 = d() 0.16/0.37 0.16/0.37 a__h(d()) = 264 >= 16 = a__g(c()) 0.16/0.37 0.16/0.37 mark(g(X)) = X + 119 >= X + 16 = a__g(X) 0.16/0.37 0.16/0.37 mark(h(X)) = X + 259 >= X + 71 = a__h(X) 0.16/0.37 0.16/0.37 mark(c()) = 119 >= 1 = a__c() 0.16/0.37 0.16/0.37 mark(d()) = 312 >= 193 = d() 0.16/0.37 0.16/0.37 a__g(X) = X + 16 >= X = g(X) 0.16/0.37 0.16/0.37 a__h(X) = X + 71 >= X + 140 = h(X) 0.16/0.37 0.16/0.37 a__c() = 1 >= 0 = c() 0.16/0.37 problem: 0.16/0.37 strict: 0.16/0.37 a__g(X) -> a__h(X) 0.16/0.37 a__c() -> d() 0.16/0.37 a__h(X) -> h(X) 0.16/0.37 weak: 0.16/0.37 a__h(d()) -> a__g(c()) 0.16/0.37 mark(g(X)) -> a__g(X) 0.16/0.37 mark(h(X)) -> a__h(X) 0.16/0.37 mark(c()) -> a__c() 0.16/0.37 mark(d()) -> d() 0.16/0.37 a__g(X) -> g(X) 0.16/0.37 a__c() -> c() 0.16/0.37 Matrix Interpretation Processor: dim=1 0.16/0.37 0.16/0.37 max_matrix: 0.16/0.37 1 0.16/0.37 interpretation: 0.16/0.37 [h](x0) = x0, 0.16/0.37 0.16/0.37 [mark](x0) = x0, 0.16/0.37 0.16/0.37 [g](x0) = x0 + 128, 0.16/0.37 0.16/0.37 [c] = 0, 0.16/0.37 0.16/0.37 [d] = 128, 0.16/0.37 0.16/0.37 [a__c] = 0, 0.16/0.37 0.16/0.37 [a__h](x0) = x0, 0.16/0.37 0.16/0.37 [a__g](x0) = x0 + 128 0.16/0.37 orientation: 0.16/0.37 a__g(X) = X + 128 >= X = a__h(X) 0.16/0.37 0.16/0.37 a__c() = 0 >= 128 = d() 0.16/0.37 0.16/0.37 a__h(X) = X >= X = h(X) 0.16/0.37 0.16/0.37 a__h(d()) = 128 >= 128 = a__g(c()) 0.16/0.37 0.16/0.37 mark(g(X)) = X + 128 >= X + 128 = a__g(X) 0.16/0.37 0.16/0.37 mark(h(X)) = X >= X = a__h(X) 0.16/0.37 0.16/0.37 mark(c()) = 0 >= 0 = a__c() 0.16/0.37 0.16/0.37 mark(d()) = 128 >= 128 = d() 0.16/0.37 0.16/0.37 a__g(X) = X + 128 >= X + 128 = g(X) 0.16/0.37 0.16/0.37 a__c() = 0 >= 0 = c() 0.16/0.37 problem: 0.16/0.37 strict: 0.16/0.37 a__c() -> d() 0.16/0.37 a__h(X) -> h(X) 0.16/0.37 weak: 0.16/0.37 a__g(X) -> a__h(X) 0.16/0.37 a__h(d()) -> a__g(c()) 0.16/0.37 mark(g(X)) -> a__g(X) 0.16/0.37 mark(h(X)) -> a__h(X) 0.16/0.37 mark(c()) -> a__c() 0.16/0.37 mark(d()) -> d() 0.16/0.37 a__g(X) -> g(X) 0.16/0.37 a__c() -> c() 0.16/0.37 Matrix Interpretation Processor: dim=1 0.16/0.37 0.16/0.37 max_matrix: 0.16/0.37 1 0.16/0.37 interpretation: 0.16/0.37 [h](x0) = x0 + 78, 0.16/0.37 0.16/0.37 [mark](x0) = x0 + 8, 0.16/0.37 0.16/0.37 [g](x0) = x0, 0.16/0.37 0.16/0.37 [c] = 0, 0.16/0.37 0.16/0.37 [d] = 4, 0.16/0.37 0.16/0.37 [a__c] = 6, 0.16/0.37 0.16/0.37 [a__h](x0) = x0 + 2, 0.16/0.37 0.16/0.37 [a__g](x0) = x0 + 4 0.16/0.37 orientation: 0.16/0.37 a__c() = 6 >= 4 = d() 0.16/0.37 0.16/0.37 a__h(X) = X + 2 >= X + 78 = h(X) 0.16/0.37 0.16/0.37 a__g(X) = X + 4 >= X + 2 = a__h(X) 0.16/0.37 0.16/0.37 a__h(d()) = 6 >= 4 = a__g(c()) 0.16/0.37 0.16/0.37 mark(g(X)) = X + 8 >= X + 4 = a__g(X) 0.16/0.37 0.16/0.37 mark(h(X)) = X + 86 >= X + 2 = a__h(X) 0.16/0.37 0.16/0.37 mark(c()) = 8 >= 6 = a__c() 0.16/0.37 0.16/0.37 mark(d()) = 12 >= 4 = d() 0.16/0.37 0.16/0.37 a__g(X) = X + 4 >= X = g(X) 0.16/0.37 0.16/0.37 a__c() = 6 >= 0 = c() 0.16/0.37 problem: 0.16/0.37 strict: 0.16/0.37 a__h(X) -> h(X) 0.16/0.37 weak: 0.16/0.37 a__c() -> d() 0.16/0.37 a__g(X) -> a__h(X) 0.16/0.37 a__h(d()) -> a__g(c()) 0.16/0.37 mark(g(X)) -> a__g(X) 0.16/0.37 mark(h(X)) -> a__h(X) 0.16/0.37 mark(c()) -> a__c() 0.16/0.37 mark(d()) -> d() 0.16/0.37 a__g(X) -> g(X) 0.16/0.37 a__c() -> c() 0.16/0.37 Matrix Interpretation Processor: dim=1 0.16/0.37 0.16/0.37 max_matrix: 0.16/0.37 1 0.16/0.37 interpretation: 0.16/0.37 [h](x0) = x0, 0.16/0.37 0.16/0.37 [mark](x0) = x0 + 8, 0.16/0.37 0.16/0.37 [g](x0) = x0 + 1, 0.16/0.37 0.16/0.37 [c] = 0, 0.16/0.37 0.16/0.37 [d] = 0, 0.16/0.37 0.16/0.37 [a__c] = 0, 0.16/0.37 0.16/0.37 [a__h](x0) = x0 + 2, 0.16/0.37 0.16/0.37 [a__g](x0) = x0 + 2 0.16/0.37 orientation: 0.16/0.37 a__h(X) = X + 2 >= X = h(X) 0.16/0.37 0.16/0.37 a__c() = 0 >= 0 = d() 0.16/0.37 0.16/0.37 a__g(X) = X + 2 >= X + 2 = a__h(X) 0.16/0.37 0.16/0.37 a__h(d()) = 2 >= 2 = a__g(c()) 0.16/0.37 0.16/0.37 mark(g(X)) = X + 9 >= X + 2 = a__g(X) 0.16/0.37 0.16/0.37 mark(h(X)) = X + 8 >= X + 2 = a__h(X) 0.16/0.37 0.16/0.37 mark(c()) = 8 >= 0 = a__c() 0.16/0.37 0.16/0.37 mark(d()) = 8 >= 0 = d() 0.16/0.37 0.16/0.37 a__g(X) = X + 2 >= X + 1 = g(X) 0.16/0.37 0.16/0.37 a__c() = 0 >= 0 = c() 0.16/0.37 problem: 0.16/0.37 strict: 0.16/0.37 0.16/0.37 weak: 0.16/0.37 a__h(X) -> h(X) 0.16/0.37 a__c() -> d() 0.16/0.37 a__g(X) -> a__h(X) 0.16/0.37 a__h(d()) -> a__g(c()) 0.16/0.37 mark(g(X)) -> a__g(X) 0.16/0.37 mark(h(X)) -> a__h(X) 0.16/0.37 mark(c()) -> a__c() 0.16/0.37 mark(d()) -> d() 0.16/0.37 a__g(X) -> g(X) 0.16/0.37 a__c() -> c() 0.16/0.37 Qed 0.16/0.37 EOF