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(1(x0))) → 0(1(q0(x0)))
1(q0(0(x0))) → 0(0(q1(x0)))
1(q0(1(x0))) → 0(1(q1(x0)))
1(q1(0(x0))) → 1(0(q1(x0)))
1(q1(1(x0))) → 1(1(q1(x0)))
0(q1(0(x0))) → 0(0(q2(x0)))
0(q1(1(x0))) → 0(1(q2(x0)))
1(q2(0(x0))) → 1(0(q2(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(1(x0))) → 1(1(q5(x0)))
1(q5(0(x0))) → 0(0(q1(x0)))
1(q5(1(x0))) → 0(1(q1(x0)))
0(q5(x0)) → q6(0(x0))
1(q6(x0)) → q6(1(x0))
1(q7(0(x0))) → 0(0(q8(x0)))
1(q7(1(x0))) → 0(1(q8(x0)))
0(q8(x0)) → 0(q0(x0))
1(q8(0(x0))) → 1(0(q8(x0)))
1(q8(1(x0))) → 1(1(q8(x0)))
0(q6(x0)) → q9(0(x0))
0(q9(0(x0))) → 1(0(q7(x0)))
0(q9(1(x0))) → 1(1(q7(x0)))
1(q9(x0)) → q9(1(x0))
h(q0(x0)) → h(0(q0(x0)))
q0(h(x0)) → q0(0(h(x0)))
h(q1(x0)) → h(0(q1(x0)))
q1(h(x0)) → q1(0(h(x0)))
h(q2(x0)) → h(0(q2(x0)))
q2(h(x0)) → q2(0(h(x0)))
h(q3(x0)) → h(0(q3(x0)))
q3(h(x0)) → q3(0(h(x0)))
h(q4(x0)) → h(0(q4(x0)))
q4(h(x0)) → q4(0(h(x0)))
h(q5(x0)) → h(0(q5(x0)))
q5(h(x0)) → q5(0(h(x0)))
h(q6(x0)) → h(0(q6(x0)))
q6(h(x0)) → q6(0(h(x0)))

Proof

1 Loop

The following loop proves nontermination.

t0 = 0(q0(0(h(x117))))
→ε 0(0(q0(h(x117))))
→1.1 0(0(q0(0(h(x117)))))
= t2
where t2 = C[t0σ] and σ = {x117/x117} and C = 0(☐)