Problem: c() -> f(n__g(n__c())) f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) c() -> n__c() activate(n__g(X)) -> g(X) activate(n__c()) -> c() activate(X) -> X Proof: Matrix Interpretation Processor: dim=1 interpretation: [g](x0) = x0, [activate](x0) = x0 + 1, [f](x0) = 4x0 + 1, [n__g](x0) = x0, [n__c] = 0, [c] = 1 orientation: c() = 1 >= 1 = f(n__g(n__c())) f(n__g(X)) = 4X + 1 >= X + 1 = g(activate(X)) g(X) = X >= X = n__g(X) c() = 1 >= 0 = n__c() activate(n__g(X)) = X + 1 >= X = g(X) activate(n__c()) = 1 >= 1 = c() activate(X) = X + 1 >= X = X problem: c() -> f(n__g(n__c())) f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) activate(n__c()) -> c() Unfolding Processor: loop length: 3 terms: c() f(n__g(n__c())) g(activate(n__c())) context: g([]) substitution: Qed