Problem: a__g(X) -> a__h(X) a__c() -> d() a__h(d()) -> a__g(c()) mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) mark(c()) -> a__c() mark(d()) -> d() a__g(X) -> g(X) a__h(X) -> h(X) a__c() -> c() Proof: Complexity Transformation Processor: strict: a__g(X) -> a__h(X) a__c() -> d() a__h(d()) -> a__g(c()) mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) mark(c()) -> a__c() mark(d()) -> d() a__g(X) -> g(X) a__h(X) -> h(X) a__c() -> c() weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [h](x0) = x0 + 12, [mark](x0) = x0 + 6, [g](x0) = x0 + 12, [c] = 4, [d] = 0, [a__c] = 5, [a__h](x0) = x0, [a__g](x0) = x0 + 8 orientation: a__g(X) = X + 8 >= X = a__h(X) a__c() = 5 >= 0 = d() a__h(d()) = 0 >= 12 = a__g(c()) mark(g(X)) = X + 18 >= X + 8 = a__g(X) mark(h(X)) = X + 18 >= X = a__h(X) mark(c()) = 10 >= 5 = a__c() mark(d()) = 6 >= 0 = d() a__g(X) = X + 8 >= X + 12 = g(X) a__h(X) = X >= X + 12 = h(X) a__c() = 5 >= 4 = c() problem: strict: a__h(d()) -> a__g(c()) a__g(X) -> g(X) a__h(X) -> h(X) weak: a__g(X) -> a__h(X) a__c() -> d() mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) mark(c()) -> a__c() mark(d()) -> d() a__c() -> c() Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [h](x0) = x0 + 7, [mark](x0) = x0 + 1, [g](x0) = x0 + 7, [c] = 0, [d] = 1, [a__c] = 1, [a__h](x0) = x0 + 8, [a__g](x0) = x0 + 8 orientation: a__h(d()) = 9 >= 8 = a__g(c()) a__g(X) = X + 8 >= X + 7 = g(X) a__h(X) = X + 8 >= X + 7 = h(X) a__g(X) = X + 8 >= X + 8 = a__h(X) a__c() = 1 >= 1 = d() mark(g(X)) = X + 8 >= X + 8 = a__g(X) mark(h(X)) = X + 8 >= X + 8 = a__h(X) mark(c()) = 1 >= 1 = a__c() mark(d()) = 2 >= 1 = d() a__c() = 1 >= 0 = c() problem: strict: weak: a__h(d()) -> a__g(c()) a__g(X) -> g(X) a__h(X) -> h(X) a__g(X) -> a__h(X) a__c() -> d() mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) mark(c()) -> a__c() mark(d()) -> d() a__c() -> c() Qed