Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/ExIntrod_Zan97_Z)

The rewrite relation of the following TRS is considered.

fact(X) → if(zero(X),n__s(0),n__prod(X,fact(p(X)))) (1)
add(0,X) → X (2)
add(s(X),Y) → s(add(X,Y)) (3)
prod(0,X) → 0 (4)
prod(s(X),Y) → add(Y,prod(X,Y)) (5)
if(true,X,Y) → activate(X) (6)
if(false,X,Y) → activate(Y) (7)
zero(0) → true (8)
zero(s(X)) → false (9)
p(s(X)) → X (10)
s(X) → n__s(X) (11)
prod(X1,X2) → n__prod(X1,X2) (12)
activate(n__s(X)) → s(X) (13)
activate(n__prod(X1,X2)) → prod(X1,X2) (14)
activate(X) → X (15)
The evaluation strategy is outermost

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = fact(X)
→ if(zero(X),n__s(0),n__prod(X,fact(p(X))))
= t1
where t1 = C[t0σ] and σ = {X/p(X)} and C = if(zero(X),n__s(0),n__prod(X,☐))