YES
(VAR x)
(RULES 
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)
)

Proving termination of rewriting for dj:

-> Dependency pairs:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_1(0(x)) -> nF_0(0(1(x)))
nF_1(0(x)) -> nF_0(1(x))
nF_1(0(x)) -> nF_1(x)
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(0(0(x))))
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(x))
nF_1(1(x)) -> nF_0(x)
nF_0(0(x)) -> nF_0(x)

-> Proof of termination for dj_1:
-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_0(1(x)) -> nF_1(x)
nF_0(0(x)) -> nF_0(x)
nF_1(1(x)) -> nF_0(x)
nF_1(0(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(x))
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(0(0(x))))
nF_1(0(x)) -> nF_0(1(x))
nF_1(0(x)) -> nF_0(0(1(x)))

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X + 4
[nF_1](X) = 4.X
[nF_0](X) = X

TIME: 1.116329

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_1(0(x)) -> nF_1(x)
nF_0(1(x)) -> nF_1(x)
nF_1(0(x)) -> nF_0(1(x))
nF_1(1(x)) -> nF_0(0(0(0(x))))
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(x))
nF_1(1(x)) -> nF_0(x)
nF_0(0(x)) -> nF_0(x)

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X + 4
[nF_1](X) = 4.X
[nF_0](X) = X

TIME: 1.624e-3

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(x)
nF_1(0(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(x))
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(0(0(x))))
nF_1(0(x)) -> nF_0(1(x))

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X + 4
[nF_1](X) = 4.X
[nF_0](X) = X

TIME: 4.0323e-2

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_1(0(x)) -> nF_1(x)
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(0(0(x))))
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(x))
nF_1(1(x)) -> nF_0(x)

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X + 4
[nF_1](X) = 4.X
[nF_0](X) = X

TIME: 3.699e-3

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(x))
nF_1(0(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(0(0(x))))

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X
[nF_1](X) = 4.X + 4
[nF_0](X) = X

TIME: 2.477e-3

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_1(0(x)) -> nF_1(x)
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(1(x)) -> nF_0(0(x))

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X
[nF_1](X) = 4.X + 4
[nF_0](X) = X

TIME: 2.173e-3

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(0(x)))
nF_1(0(x)) -> nF_1(x)

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X + 4
[nF_1](X) = 4.X
[nF_0](X) = X

TIME: 4.32e-4

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_0(1(x)) -> nF_1(x)
nF_1(1(x)) -> nF_0(0(0(x)))

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X
[nF_1](X) = 4.X + 4
[nF_0](X) = X

TIME: 4.407e-3

-> -> Dependency pairs in cycle:
nF_1(0(x)) -> nF_0(0(0(1(x))))
nF_0(1(x)) -> nF_1(x)

UsableRules:
1(0(x)) -> 0(0(0(1(x))))
0(1(x)) -> 1(x)
1(1(x)) -> 0(0(0(0(x))))
0(0(x)) -> 0(x)

Polynomial Interpretation:

[1](X) = 4.X + 4
[0](X) = X + 4
[nF_1](X) = 4.X
[nF_0](X) = X

TIME: 1.935e-3


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 4
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.