Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret1)

The rewrite relation of the following TRS is considered.

D(t) → s(h) (1)
D(constant) → h (2)
D(b(x,y)) → b(D(x),D(y)) (3)
D(c(x,y)) → b(c(y,D(x)),c(x,D(y))) (4)
D(m(x,y)) → m(D(x),D(y)) (5)
D(opp(x)) → opp(D(x)) (6)
D(div(x,y)) → m(div(D(x),y),div(c(x,D(y)),pow(y,2))) (7)
D(ln(x)) → div(D(x),x) (8)
D(pow(x,y)) → b(c(c(y,pow(x,m(y,1))),D(x)),c(c(pow(x,y),ln(x)),D(y))) (9)
b(h,x) → x (10)
b(x,h) → x (11)
b(s(x),s(y)) → s(s(b(x,y))) (12)
b(b(x,y),z) → b(x,b(y,z)) (13)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(D) = 9 stat(D) = mul
prec(t) = 10 stat(t) = mul
prec(h) = 0 stat(h) = mul
prec(constant) = 11 stat(constant) = mul
prec(b) = 1 stat(b) = lex
prec(c) = 2 stat(c) = mul
prec(m) = 3 stat(m) = mul
prec(opp) = 4 stat(opp) = mul
prec(div) = 6 stat(div) = mul
prec(pow) = 5 stat(pow) = mul
prec(2) = 7 stat(2) = mul
prec(ln) = 5 stat(ln) = mul
prec(1) = 8 stat(1) = mul

π(D) = [1]
π(t) = []
π(s) = 1
π(h) = []
π(constant) = []
π(b) = [1,2]
π(c) = [1,2]
π(m) = [1,2]
π(opp) = [1]
π(div) = [1,2]
π(pow) = [1,2]
π(2) = []
π(ln) = [1]
π(1) = []

all of the following rules can be deleted.
D(t) → s(h) (1)
D(constant) → h (2)
D(b(x,y)) → b(D(x),D(y)) (3)
D(c(x,y)) → b(c(y,D(x)),c(x,D(y))) (4)
D(m(x,y)) → m(D(x),D(y)) (5)
D(opp(x)) → opp(D(x)) (6)
D(div(x,y)) → m(div(D(x),y),div(c(x,D(y)),pow(y,2))) (7)
D(ln(x)) → div(D(x),x) (8)
D(pow(x,y)) → b(c(c(y,pow(x,m(y,1))),D(x)),c(c(pow(x,y),ln(x)),D(y))) (9)
b(h,x) → x (10)
b(x,h) → x (11)
b(b(x,y),z) → b(x,b(y,z)) (13)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(s) = 0 weight(s) = 1
prec(b) = 1 weight(b) = 0
all of the following rules can be deleted.
b(s(x),s(y)) → s(s(b(x,y))) (12)

1.1.1 R is empty

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