Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, M, N) → U12(tt, activate(M), activate(N))
U12(tt, M, N) → s(plus(activate(N), activate(M)))
U21(tt, M, N) → U22(tt, activate(M), activate(N))
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
plus(N, 0) → N
plus(N, s(M)) → U11(tt, M, N)
x(N, 0) → 0
x(N, s(M)) → U21(tt, M, N)
activate(X) → X

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
U11(x1, x2, x3)  =  U11(x1, x2, x3)
tt  =  tt
U12(x1, x2, x3)  =  U12(x1, x2, x3)
activate(x1)  =  x1
s(x1)  =  s(x1)
plus(x1, x2)  =  plus(x1, x2)
U21(x1, x2, x3)  =  U21(x1, x2, x3)
U22(x1, x2, x3)  =  U22(x1, x2, x3)
x(x1, x2)  =  x(x1, x2)
0  =  0

Recursive path order with status [RPO].
Quasi-Precedence:

[U21₃, U22₃, x₂] > [U11₃, U12₃, plus₂] > s₁ > tt
[U21₃, U22₃, x₂] > 0

Status:

plus₂: [1,2]
tt: multiset
U22₃: multiset
U11₃: [3,2,1]
s₁: [1]
x₂: multiset
U12₃: [3,2,1]
U21₃: multiset
0: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U12(tt, M, N) → s(plus(activate(N), activate(M)))
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
plus(N, 0) → N
plus(N, s(M)) → U11(tt, M, N)
x(N, 0) → 0
x(N, s(M)) → U21(tt, M, N)

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, M, N) → U12(tt, activate(M), activate(N))
U21(tt, M, N) → U22(tt, activate(M), activate(N))
activate(X) → X

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁, x₂, x₃)) = 1 + x₁ + 2·x₂ + 2·x₃   
POL(U12(x₁, x₂, x₃)) = 1 + 2·x₁ + x₂ + x₃   
POL(U21(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + 2·x₃   
POL(U22(x₁, x₂, x₃)) = 1 + 2·x₁ + 2·x₂ + 2·x₃   
POL(activate(x₁)) = x₁   
POL(tt) = 0   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U21(tt, M, N) → U22(tt, activate(M), activate(N))

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, M, N) → U12(tt, activate(M), activate(N))
activate(X) → X

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁, x₂, x₃)) = 3 + x₁ + x₂ + x₃   
POL(U12(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(activate(x₁)) = 1 + x₁   
POL(tt) = 0   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U11(tt, M, N) → U12(tt, activate(M), activate(N))
activate(X) → X

(6) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(7) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(8) TRUE

(9) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(10) TRUE