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