NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(q0(0(x0))) → 0(0(q0(x0)))
0(q0(h(x0))) → 0(0(q0(h(x0))))
0(q0(1(x0))) → 0(1(q0(x0)))
1(q0(0(x0))) → 0(0(q1(x0)))
1(q0(h(x0))) → 0(0(q1(h(x0))))
1(q0(1(x0))) → 0(1(q1(x0)))
1(q1(0(x0))) → 1(0(q1(x0)))
1(q1(h(x0))) → 1(0(q1(h(x0))))
1(q1(1(x0))) → 1(1(q1(x0)))
0(q1(0(x0))) → 0(0(q2(x0)))
0(q1(h(x0))) → 0(0(q2(h(x0))))
0(q1(1(x0))) → 0(1(q2(x0)))
1(q2(0(x0))) → 1(0(q2(x0)))
1(q2(h(x0))) → 1(0(q2(h(x0))))
1(q2(1(x0))) → 1(1(q2(x0)))
0(q2(x0)) → q3(1(x0))
1(q3(x0)) → q3(1(x0))
0(q3(x0)) → q4(0(x0))
1(q4(x0)) → q4(1(x0))
0(q4(0(x0))) → 1(0(q5(x0)))
0(q4(h(x0))) → 1(0(q5(h(x0))))
0(q4(1(x0))) → 1(1(q5(x0)))
1(q5(0(x0))) → 0(0(q1(x0)))
1(q5(h(x0))) → 0(0(q1(h(x0))))
1(q5(1(x0))) → 0(1(q1(x0)))
h(q0(x0)) → h(0(q0(x0)))
h(q1(x0)) → h(0(q1(x0)))
h(q2(x0)) → h(0(q2(x0)))
h(q3(x0)) → h(0(q3(x0)))
h(q4(x0)) → h(0(q4(x0)))
h(q5(x0)) → h(0(q5(x0)))

Proof

1 Loop

The following loop proves nontermination.

t0 = 0(q0(h(x0)))
→ε 0(0(q0(h(x0))))
= t1
where t1 = C[t0σ] and σ = {x0/x0} and C = 0(☐)