NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(b(b(x0))) → b(b(a(a(x0))))
a(a(x0)) → b(x0)

Proof

1 Loop

The following loop proves nontermination.

t0 = a(b(b(b(b(b(b(x887)))))))
→ε b(b(a(a(b(b(b(b(x887))))))))
→1.1.1 b(b(a(b(b(a(a(b(b(x887)))))))))
→1.1.1.1.1.1 b(b(a(b(b(a(b(b(a(a(x887))))))))))
→1.1.1.1.1 b(b(a(b(b(b(b(a(a(a(a(x887)))))))))))
→1.1.1.1.1.1.1 b(b(a(b(b(b(b(b(a(a(x887))))))))))
→1.1.1.1.1.1.1.1 b(b(a(b(b(b(b(b(b(x887)))))))))
= t6
where t6 = C[t0σ] and σ = {x887/x887} and C = b(b(☐))