Problem:
f(n__b(),X,n__c()) -> f(X,c(),X)
c() -> b()
b() -> n__b()
c() -> n__c()
activate(n__b()) -> b()
activate(n__c()) -> c()
activate(X) -> X
Proof:
Matrix Interpretation Processor: dim=1
interpretation:
[activate](x0) = x0 + 6,
[b] = 4,
[c] = 4,
[f](x0, x1, x2) = 2x0 + 3x1 + x2,
[n__c] = 4,
[n__b] = 4
orientation:
f(n__b(),X,n__c()) = 3X + 12 >= 3X + 12 = f(X,c(),X)
c() = 4 >= 4 = b()
b() = 4 >= 4 = n__b()
c() = 4 >= 4 = n__c()
activate(n__b()) = 10 >= 4 = b()
activate(n__c()) = 10 >= 4 = c()
activate(X) = X + 6 >= X = X
problem:
f(n__b(),X,n__c()) -> f(X,c(),X)
c() -> b()
b() -> n__b()
c() -> n__c()
Unfolding Processor:
loop length: 4
terms:
f(c(),c(),c())
f(c(),c(),n__c())
f(b(),c(),n__c())
f(n__b(),c(),n__c())
context: []
substitution:
Qed