Certification Problem

Input (TPDB TRS_Standard/CiME_04/append-wrong)

The rewrite relation of the following TRS is considered.

is_empty(nil) → true (1)
is_empty(cons(x,l)) → false (2)
hd(cons(x,l)) → x (3)
tl(cons(x,l)) → cons(x,l) (4)
append(l1,l2) → ifappend(l1,l2,is_empty(l1)) (5)
ifappend(l1,l2,true) → l2 (6)
ifappend(l1,l2,false) → cons(hd(l1),append(tl(l1),l2)) (7)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = append(cons(x3062,x3063),x3001)
→ ifappend(cons(x3062,x3063),x3001,is_empty(cons(x3062,x3063)))
→ ifappend(cons(x3062,x3063),x3001,false)
→ cons(hd(cons(x3062,x3063)),append(tl(cons(x3062,x3063)),x3001))
→ cons(hd(cons(x3062,x3063)),append(cons(x3062,x3063),x3001))
= t4
where t4 = C[t0σ] and σ = {x3063/x3063, x3062/x3062, x3001/x3001} and C = cons(hd(cons(x3062,x3063)),☐)