NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(0(0(0(x0)))) → 0(1(1(0(x0))))
1(0(0(1(x0)))) → 0(0(1(0(x0))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
0(0(0(0(x0)))) → 0(1(1(0(x0))))
1(0(0(1(x0)))) → 0(1(0(0(x0))))

1.1 Loop

The following loop proves nontermination.

t0 = 0(0(0(0(1(0(0(1(0(0(0(0(1(x0)))))))))))))
→1.1.1.1 0(0(0(0(0(1(0(0(0(0(0(0(1(x0)))))))))))))
→1.1.1.1.1.1.1.1 0(0(0(0(0(1(0(0(0(1(1(0(1(x0)))))))))))))
→ε 0(1(1(0(0(1(0(0(0(1(1(0(1(x0)))))))))))))
→1.1 0(1(0(1(0(0(0(0(0(1(1(0(1(x0)))))))))))))
→1.1.1.1 0(1(0(1(0(1(1(0(0(1(1(0(1(x0)))))))))))))
→1.1.1.1.1.1 0(1(0(1(0(1(0(1(0(0(1(0(1(x0)))))))))))))
→1.1.1.1.1.1.1 0(1(0(1(0(1(0(0(1(0(0(0(1(x0)))))))))))))
→1.1.1.1.1 0(1(0(1(0(0(1(0(0(0(0(0(1(x0)))))))))))))
→1.1.1 0(1(0(0(1(0(0(0(0(0(0(0(1(x0)))))))))))))
→1 0(0(1(0(0(0(0(0(0(0(0(0(1(x0)))))))))))))
→1.1.1 0(0(1(0(1(1(0(0(0(0(0(0(1(x0)))))))))))))
→1.1.1.1.1.1.1 0(0(1(0(1(1(0(0(1(1(0(0(1(x0)))))))))))))
→1.1.1.1.1 0(0(1(0(1(0(1(0(0(1(0(0(1(x0)))))))))))))
→1.1.1.1.1.1 0(0(1(0(1(0(0(1(0(0(0(0(1(x0)))))))))))))
→1.1.1.1 0(0(1(0(0(1(0(0(0(0(0(0(1(x0)))))))))))))
→1.1 0(0(0(1(0(0(0(0(0(0(0(0(1(x0)))))))))))))
→1.1.1.1.1 0(0(0(1(0(0(1(1(0(0(0(0(1(x0)))))))))))))
→1.1.1 0(0(0(0(1(0(0(1(0(0(0(0(1(x0)))))))))))))
= t18
where t18 = t0σ and σ = {x0/x0}