```
We consider the following Problem:

Strict Trs:
{  id(s(x)) -> s(id(x))
, id(0()) -> 0()
, f(s(x)) -> f(id(x))
, f(0()) -> 0()}
StartTerms: basic terms
Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
We consider the following Problem:

Strict Trs:
{  id(s(x)) -> s(id(x))
, id(0()) -> 0()
, f(s(x)) -> f(id(x))
, f(0()) -> 0()}
StartTerms: basic terms
Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
The weightgap principle applies, where following rules are oriented strictly:

TRS Component:
{  id(0()) -> 0()
, f(0()) -> 0()}

Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
0() = 

f(x1) = [1 0] x1 + 
[0 0]      
s(x1) = [1 0] x1 + 
[0 0]      
id(x1) = [0 0] x1 + 
[1 0]      

The strictly oriented rules are moved into the weak component.

We consider the following Problem:

Strict Trs:
{  id(s(x)) -> s(id(x))
, f(s(x)) -> f(id(x))}
Weak Trs:
{  id(0()) -> 0()
, f(0()) -> 0()}
StartTerms: basic terms
Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
The weightgap principle applies, where following rules are oriented strictly:

TRS Component: {f(s(x)) -> f(id(x))}

Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
0() = 

f(x1) = [1 0] x1 + 
[1 1]      
s(x1) = [1 0] x1 + 
[0 0]      
id(x1) = [0 0] x1 + 
[1 0]      

The strictly oriented rules are moved into the weak component.

We consider the following Problem:

Strict Trs: {id(s(x)) -> s(id(x))}
Weak Trs:
{  f(s(x)) -> f(id(x))
, id(0()) -> 0()
, f(0()) -> 0()}
StartTerms: basic terms
Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
We consider the following Problem:

Strict Trs: {id(s(x)) -> s(id(x))}
Weak Trs:
{  f(s(x)) -> f(id(x))
, id(0()) -> 0()
, f(0()) -> 0()}
StartTerms: basic terms
Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id) = {}
We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
0() = 


f(x1) = [2 1 0] x1 + 
[0 0 0]      
[1 1 0]      
s(x1) = [1 2 0] x1 + 
[0 0 2]      
[0 0 1]      
id(x1) = [1 0 1] x1 + 
[0 1 0]      
[0 0 1]