Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nosorts-noand_FR)

The rewrite relation of the following TRS is considered.

U11(tt,M,N) → U12(tt,activate(M),activate(N)) (1)
U12(tt,M,N) → s(plus(activate(N),activate(M))) (2)
U21(tt,M,N) → U22(tt,activate(M),activate(N)) (3)
U22(tt,M,N) → plus(x(activate(N),activate(M)),activate(N)) (4)
plus(N,0) → N (5)
plus(N,s(M)) → U11(tt,M,N) (6)
x(N,0) → 0 (7)
x(N,s(M)) → U21(tt,M,N) (8)
activate(X) → X (9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(U11) = 2 stat(U11) = mul
prec(tt) = 0 stat(tt) = mul
prec(U12) = 2 stat(U12) = mul
prec(s) = 1 stat(s) = mul
prec(plus) = 2 stat(plus) = mul
prec(U21) = 3 stat(U21) = mul
prec(U22) = 3 stat(U22) = mul
prec(x) = 3 stat(x) = mul
prec(0) = 0 stat(0) = mul

π(U11) = [1,2,3]
π(tt) = []
π(U12) = [1,2,3]
π(activate) = 1
π(s) = [1]
π(plus) = [1,2]
π(U21) = [1,2,3]
π(U22) = [1,2,3]
π(x) = [1,2]
π(0) = []

all of the following rules can be deleted.
U12(tt,M,N) → s(plus(activate(N),activate(M))) (2)
U22(tt,M,N) → plus(x(activate(N),activate(M)),activate(N)) (4)
plus(N,0) → N (5)
plus(N,s(M)) → U11(tt,M,N) (6)
x(N,0) → 0 (7)
x(N,s(M)) → U21(tt,M,N) (8)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(tt) = 0 weight(tt) = 1
prec(activate) = 3 weight(activate) = 1
prec(U11) = 2 weight(U11) = 2
prec(U12) = 1 weight(U12) = 0
prec(U21) = 5 weight(U21) = 2
prec(U22) = 4 weight(U22) = 0
all of the following rules can be deleted.
U11(tt,M,N) → U12(tt,activate(M),activate(N)) (1)
U21(tt,M,N) → U22(tt,activate(M),activate(N)) (3)
activate(X) → X (9)

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.