Left Termination proof of /tmp/tmpdgnTle/d.pl

Left Termination of the query pattern d(b,b,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

d₃(X, X, 1₀).
d₃(T, underscore, 0₀) :- isnumber₁(T).
d₃(times₂(U, V), X, times₂(B, U) + times₂(A, V)) :- d₃(U, X, A), d₃(V, X, B).
d₃(div₂(U, V), X, W) :- d₃(times₂(U, power₂(V, p₁(0₀))), X, W).
d₃(power₂(U, V), X, times₂(V, times₂(W, power₂(U, p₁(V))))) :- isnumber₁(V), d₃(U, X, W).
isnumber₁(0₀).
isnumber₁(s₁(X)) :- isnumber₁(X).
isnumber₁(p₁(X)) :- isnumber₁(X).

With regard to the inferred argument filtering the predicates were used in the following modes:
d₃: (b,b,f)
isnumber₁: (b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

d_3_in_gga₃(X, X, 1_0) -> d_3_out_gga₃(X, X, 1_0)
d_3_in_gga₃(T, underscore, 0_0) -> if_d_3_in_1_gga₃(T, underscore, isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g₁(0_0)
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₂(X, isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₂(X, isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(p_1₁(X))
if_isnumber_1_in_1_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(s_1₁(X))
if_d_3_in_1_gga₃(T, underscore, isnumber_1_out_g₁(T)) -> d_3_out_gga₃(T, underscore, 0_0)
d_3_in_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> if_d_3_in_2_gga₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
d_3_in_gga₃(div_2₂(U, V), X, W) -> if_d_3_in_4_gga₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
d_3_in_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_out_g₁(V)) -> if_d_3_in_6_gga₅(U, V, X, W, d_3_in_gga₃(U, X, W))
if_d_3_in_6_gga₅(U, V, X, W, d_3_out_gga₃(U, X, W)) -> d_3_out_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₅(U, V, X, W, d_3_out_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)) -> d_3_out_gga₃(div_2₂(U, V), X, W)
if_d_3_in_2_gga₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> if_d_3_in_3_gga₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
if_d_3_in_3_gga₆(U, V, X, B, A, d_3_out_gga₃(V, X, B)) -> d_3_out_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V)))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

d_3_in_gga₃(X, X, 1_0) -> d_3_out_gga₃(X, X, 1_0)
d_3_in_gga₃(T, underscore, 0_0) -> if_d_3_in_1_gga₃(T, underscore, isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g₁(0_0)
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₂(X, isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₂(X, isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(p_1₁(X))
if_isnumber_1_in_1_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(s_1₁(X))
if_d_3_in_1_gga₃(T, underscore, isnumber_1_out_g₁(T)) -> d_3_out_gga₃(T, underscore, 0_0)
d_3_in_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> if_d_3_in_2_gga₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
d_3_in_gga₃(div_2₂(U, V), X, W) -> if_d_3_in_4_gga₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
d_3_in_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_out_g₁(V)) -> if_d_3_in_6_gga₅(U, V, X, W, d_3_in_gga₃(U, X, W))
if_d_3_in_6_gga₅(U, V, X, W, d_3_out_gga₃(U, X, W)) -> d_3_out_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₅(U, V, X, W, d_3_out_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)) -> d_3_out_gga₃(div_2₂(U, V), X, W)
if_d_3_in_2_gga₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> if_d_3_in_3_gga₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
if_d_3_in_3_gga₆(U, V, X, B, A, d_3_out_gga₃(V, X, B)) -> d_3_out_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V)))

D_3_IN_GGA₃(T, underscore, 0_0) -> IF_D_3_IN_1_GGA₃(T, underscore, isnumber_1_in_g₁(T))
D_3_IN_GGA₃(T, underscore, 0_0) -> ISNUMBER_1_IN_G₁(T)
ISNUMBER_1_IN_G₁(s_1₁(X)) -> IF_ISNUMBER_1_IN_1_G₂(X, isnumber_1_in_g₁(X))
ISNUMBER_1_IN_G₁(s_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
ISNUMBER_1_IN_G₁(p_1₁(X)) -> IF_ISNUMBER_1_IN_2_G₂(X, isnumber_1_in_g₁(X))
ISNUMBER_1_IN_G₁(p_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
D_3_IN_GGA₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
D_3_IN_GGA₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> D_3_IN_GGA₃(U, X, A)
D_3_IN_GGA₃(div_2₂(U, V), X, W) -> IF_D_3_IN_4_GGA₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
D_3_IN_GGA₃(div_2₂(U, V), X, W) -> D_3_IN_GGA₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)
D_3_IN_GGA₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_in_g₁(V))
D_3_IN_GGA₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> ISNUMBER_1_IN_G₁(V)
IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_out_g₁(V)) -> IF_D_3_IN_6_GGA₅(U, V, X, W, d_3_in_gga₃(U, X, W))
IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_out_g₁(V)) -> D_3_IN_GGA₃(U, X, W)
IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> IF_D_3_IN_3_GGA₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> D_3_IN_GGA₃(V, X, B)

The TRS R consists of the following rules:

d_3_in_gga₃(X, X, 1_0) -> d_3_out_gga₃(X, X, 1_0)
d_3_in_gga₃(T, underscore, 0_0) -> if_d_3_in_1_gga₃(T, underscore, isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g₁(0_0)
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₂(X, isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₂(X, isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(p_1₁(X))
if_isnumber_1_in_1_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(s_1₁(X))
if_d_3_in_1_gga₃(T, underscore, isnumber_1_out_g₁(T)) -> d_3_out_gga₃(T, underscore, 0_0)
d_3_in_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> if_d_3_in_2_gga₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
d_3_in_gga₃(div_2₂(U, V), X, W) -> if_d_3_in_4_gga₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
d_3_in_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_out_g₁(V)) -> if_d_3_in_6_gga₅(U, V, X, W, d_3_in_gga₃(U, X, W))
if_d_3_in_6_gga₅(U, V, X, W, d_3_out_gga₃(U, X, W)) -> d_3_out_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₅(U, V, X, W, d_3_out_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)) -> d_3_out_gga₃(div_2₂(U, V), X, W)
if_d_3_in_2_gga₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> if_d_3_in_3_gga₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
if_d_3_in_3_gga₆(U, V, X, B, A, d_3_out_gga₃(V, X, B)) -> d_3_out_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V)))

The argument filtering Pi contains the following mapping:
d_3_in_gga₃(x1, x2, x3) = d_3_in_gga₂(x1, x2)
1_0 = 1_0
0_0 = 0_0
times_2₂(x1, x2) = times_2₂(x1, x2)
+₂(x1, x2) = +₂(x1, x2)
div_2₂(x1, x2) = div_2₂(x1, x2)
power_2₂(x1, x2) = power_2₂(x1, x2)
p_1₁(x1) = p_1₁(x1)
s_1₁(x1) = s_1₁(x1)
d_3_out_gga₃(x1, x2, x3) = d_3_out_gga₁(x3)
if_d_3_in_1_gga₃(x1, x2, x3) = if_d_3_in_1_gga₁(x3)
isnumber_1_in_g₁(x1) = isnumber_1_in_g₁(x1)
isnumber_1_out_g₁(x1) = isnumber_1_out_g
if_isnumber_1_in_1_g₂(x1, x2) = if_isnumber_1_in_1_g₁(x2)
if_isnumber_1_in_2_g₂(x1, x2) = if_isnumber_1_in_2_g₁(x2)
if_d_3_in_2_gga₆(x1, x2, x3, x4, x5, x6) = if_d_3_in_2_gga₄(x1, x2, x3, x6)
if_d_3_in_4_gga₅(x1, x2, x3, x4, x5) = if_d_3_in_4_gga₁(x5)
if_d_3_in_5_gga₅(x1, x2, x3, x4, x5) = if_d_3_in_5_gga₄(x1, x2, x3, x5)
if_d_3_in_6_gga₅(x1, x2, x3, x4, x5) = if_d_3_in_6_gga₃(x1, x2, x5)
if_d_3_in_3_gga₆(x1, x2, x3, x4, x5, x6) = if_d_3_in_3_gga₄(x1, x2, x5, x6)
IF_D_3_IN_1_GGA₃(x1, x2, x3) = IF_D_3_IN_1_GGA₁(x3)
ISNUMBER_1_IN_G₁(x1) = ISNUMBER_1_IN_G₁(x1)
IF_D_3_IN_3_GGA₆(x1, x2, x3, x4, x5, x6) = IF_D_3_IN_3_GGA₄(x1, x2, x5, x6)
IF_D_3_IN_2_GGA₆(x1, x2, x3, x4, x5, x6) = IF_D_3_IN_2_GGA₄(x1, x2, x3, x6)
IF_D_3_IN_5_GGA₅(x1, x2, x3, x4, x5) = IF_D_3_IN_5_GGA₄(x1, x2, x3, x5)
IF_ISNUMBER_1_IN_2_G₂(x1, x2) = IF_ISNUMBER_1_IN_2_G₁(x2)
IF_D_3_IN_6_GGA₅(x1, x2, x3, x4, x5) = IF_D_3_IN_6_GGA₃(x1, x2, x5)
D_3_IN_GGA₃(x1, x2, x3) = D_3_IN_GGA₂(x1, x2)
IF_ISNUMBER_1_IN_1_G₂(x1, x2) = IF_ISNUMBER_1_IN_1_G₁(x2)
IF_D_3_IN_4_GGA₅(x1, x2, x3, x4, x5) = IF_D_3_IN_4_GGA₁(x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

D_3_IN_GGA₃(T, underscore, 0_0) -> IF_D_3_IN_1_GGA₃(T, underscore, isnumber_1_in_g₁(T))
D_3_IN_GGA₃(T, underscore, 0_0) -> ISNUMBER_1_IN_G₁(T)
ISNUMBER_1_IN_G₁(s_1₁(X)) -> IF_ISNUMBER_1_IN_1_G₂(X, isnumber_1_in_g₁(X))
ISNUMBER_1_IN_G₁(s_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
ISNUMBER_1_IN_G₁(p_1₁(X)) -> IF_ISNUMBER_1_IN_2_G₂(X, isnumber_1_in_g₁(X))
ISNUMBER_1_IN_G₁(p_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
D_3_IN_GGA₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
D_3_IN_GGA₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> D_3_IN_GGA₃(U, X, A)
D_3_IN_GGA₃(div_2₂(U, V), X, W) -> IF_D_3_IN_4_GGA₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
D_3_IN_GGA₃(div_2₂(U, V), X, W) -> D_3_IN_GGA₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)
D_3_IN_GGA₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_in_g₁(V))
D_3_IN_GGA₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> ISNUMBER_1_IN_G₁(V)
IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_out_g₁(V)) -> IF_D_3_IN_6_GGA₅(U, V, X, W, d_3_in_gga₃(U, X, W))
IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_out_g₁(V)) -> D_3_IN_GGA₃(U, X, W)
IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> IF_D_3_IN_3_GGA₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> D_3_IN_GGA₃(V, X, B)

The TRS R consists of the following rules:

d_3_in_gga₃(X, X, 1_0) -> d_3_out_gga₃(X, X, 1_0)
d_3_in_gga₃(T, underscore, 0_0) -> if_d_3_in_1_gga₃(T, underscore, isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g₁(0_0)
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₂(X, isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₂(X, isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(p_1₁(X))
if_isnumber_1_in_1_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(s_1₁(X))
if_d_3_in_1_gga₃(T, underscore, isnumber_1_out_g₁(T)) -> d_3_out_gga₃(T, underscore, 0_0)
d_3_in_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> if_d_3_in_2_gga₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
d_3_in_gga₃(div_2₂(U, V), X, W) -> if_d_3_in_4_gga₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
d_3_in_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_out_g₁(V)) -> if_d_3_in_6_gga₅(U, V, X, W, d_3_in_gga₃(U, X, W))
if_d_3_in_6_gga₅(U, V, X, W, d_3_out_gga₃(U, X, W)) -> d_3_out_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₅(U, V, X, W, d_3_out_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)) -> d_3_out_gga₃(div_2₂(U, V), X, W)
if_d_3_in_2_gga₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> if_d_3_in_3_gga₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
if_d_3_in_3_gga₆(U, V, X, B, A, d_3_out_gga₃(V, X, B)) -> d_3_out_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V)))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ISNUMBER_1_IN_G₁(p_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
ISNUMBER_1_IN_G₁(s_1₁(X)) -> ISNUMBER_1_IN_G₁(X)

The TRS R consists of the following rules:

d_3_in_gga₃(X, X, 1_0) -> d_3_out_gga₃(X, X, 1_0)
d_3_in_gga₃(T, underscore, 0_0) -> if_d_3_in_1_gga₃(T, underscore, isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g₁(0_0)
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₂(X, isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₂(X, isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(p_1₁(X))
if_isnumber_1_in_1_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(s_1₁(X))
if_d_3_in_1_gga₃(T, underscore, isnumber_1_out_g₁(T)) -> d_3_out_gga₃(T, underscore, 0_0)
d_3_in_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> if_d_3_in_2_gga₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
d_3_in_gga₃(div_2₂(U, V), X, W) -> if_d_3_in_4_gga₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
d_3_in_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_out_g₁(V)) -> if_d_3_in_6_gga₅(U, V, X, W, d_3_in_gga₃(U, X, W))
if_d_3_in_6_gga₅(U, V, X, W, d_3_out_gga₃(U, X, W)) -> d_3_out_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₅(U, V, X, W, d_3_out_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)) -> d_3_out_gga₃(div_2₂(U, V), X, W)
if_d_3_in_2_gga₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> if_d_3_in_3_gga₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
if_d_3_in_3_gga₆(U, V, X, B, A, d_3_out_gga₃(V, X, B)) -> d_3_out_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V)))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ISNUMBER_1_IN_G₁(p_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
ISNUMBER_1_IN_G₁(s_1₁(X)) -> ISNUMBER_1_IN_G₁(X)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ISNUMBER_1_IN_G₁(p_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
ISNUMBER_1_IN_G₁(s_1₁(X)) -> ISNUMBER_1_IN_G₁(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ISNUMBER_1_IN_G₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ISNUMBER_1_IN_G₁(p_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
The graph contains the following edges 1 > 1
ISNUMBER_1_IN_G₁(s_1₁(X)) -> ISNUMBER_1_IN_G₁(X)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> D_3_IN_GGA₃(V, X, B)
D_3_IN_GGA₃(div_2₂(U, V), X, W) -> D_3_IN_GGA₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)
IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_out_g₁(V)) -> D_3_IN_GGA₃(U, X, W)
D_3_IN_GGA₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> IF_D_3_IN_2_GGA₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
D_3_IN_GGA₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> IF_D_3_IN_5_GGA₅(U, V, X, W, isnumber_1_in_g₁(V))
D_3_IN_GGA₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> D_3_IN_GGA₃(U, X, A)

The TRS R consists of the following rules:

d_3_in_gga₃(X, X, 1_0) -> d_3_out_gga₃(X, X, 1_0)
d_3_in_gga₃(T, underscore, 0_0) -> if_d_3_in_1_gga₃(T, underscore, isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g₁(0_0)
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₂(X, isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₂(X, isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(p_1₁(X))
if_isnumber_1_in_1_g₂(X, isnumber_1_out_g₁(X)) -> isnumber_1_out_g₁(s_1₁(X))
if_d_3_in_1_gga₃(T, underscore, isnumber_1_out_g₁(T)) -> d_3_out_gga₃(T, underscore, 0_0)
d_3_in_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V))) -> if_d_3_in_2_gga₆(U, V, X, B, A, d_3_in_gga₃(U, X, A))
d_3_in_gga₃(div_2₂(U, V), X, W) -> if_d_3_in_4_gga₅(U, V, X, W, d_3_in_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W))
d_3_in_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V))))) -> if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₅(U, V, X, W, isnumber_1_out_g₁(V)) -> if_d_3_in_6_gga₅(U, V, X, W, d_3_in_gga₃(U, X, W))
if_d_3_in_6_gga₅(U, V, X, W, d_3_out_gga₃(U, X, W)) -> d_3_out_gga₃(power_2₂(U, V), X, times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₅(U, V, X, W, d_3_out_gga₃(times_2₂(U, power_2₂(V, p_1₁(0_0))), X, W)) -> d_3_out_gga₃(div_2₂(U, V), X, W)
if_d_3_in_2_gga₆(U, V, X, B, A, d_3_out_gga₃(U, X, A)) -> if_d_3_in_3_gga₆(U, V, X, B, A, d_3_in_gga₃(V, X, B))
if_d_3_in_3_gga₆(U, V, X, B, A, d_3_out_gga₃(V, X, B)) -> d_3_out_gga₃(times_2₂(U, V), X, +₂(times_2₂(B, U), times_2₂(A, V)))

The argument filtering Pi contains the following mapping:
d_3_in_gga₃(x1, x2, x3) = d_3_in_gga₂(x1, x2)
1_0 = 1_0
0_0 = 0_0
times_2₂(x1, x2) = times_2₂(x1, x2)
+₂(x1, x2) = +₂(x1, x2)
div_2₂(x1, x2) = div_2₂(x1, x2)
power_2₂(x1, x2) = power_2₂(x1, x2)
p_1₁(x1) = p_1₁(x1)
s_1₁(x1) = s_1₁(x1)
d_3_out_gga₃(x1, x2, x3) = d_3_out_gga₁(x3)
if_d_3_in_1_gga₃(x1, x2, x3) = if_d_3_in_1_gga₁(x3)
isnumber_1_in_g₁(x1) = isnumber_1_in_g₁(x1)
isnumber_1_out_g₁(x1) = isnumber_1_out_g
if_isnumber_1_in_1_g₂(x1, x2) = if_isnumber_1_in_1_g₁(x2)
if_isnumber_1_in_2_g₂(x1, x2) = if_isnumber_1_in_2_g₁(x2)
if_d_3_in_2_gga₆(x1, x2, x3, x4, x5, x6) = if_d_3_in_2_gga₄(x1, x2, x3, x6)
if_d_3_in_4_gga₅(x1, x2, x3, x4, x5) = if_d_3_in_4_gga₁(x5)
if_d_3_in_5_gga₅(x1, x2, x3, x4, x5) = if_d_3_in_5_gga₄(x1, x2, x3, x5)
if_d_3_in_6_gga₅(x1, x2, x3, x4, x5) = if_d_3_in_6_gga₃(x1, x2, x5)
if_d_3_in_3_gga₆(x1, x2, x3, x4, x5, x6) = if_d_3_in_3_gga₄(x1, x2, x5, x6)
IF_D_3_IN_2_GGA₆(x1, x2, x3, x4, x5, x6) = IF_D_3_IN_2_GGA₄(x1, x2, x3, x6)
IF_D_3_IN_5_GGA₅(x1, x2, x3, x4, x5) = IF_D_3_IN_5_GGA₄(x1, x2, x3, x5)
D_3_IN_GGA₃(x1, x2, x3) = D_3_IN_GGA₂(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

                  ↳ QDP

                    ↳ QDPPoloProof

Q DP problem:
The TRS P consists of the following rules:

IF_D_3_IN_2_GGA₄(U, V, X, d_3_out_gga₁(A)) -> D_3_IN_GGA₂(V, X)
D_3_IN_GGA₂(div_2₂(U, V), X) -> D_3_IN_GGA₂(times_2₂(U, power_2₂(V, p_1₁(0_0))), X)
IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_out_g) -> D_3_IN_GGA₂(U, X)
D_3_IN_GGA₂(times_2₂(U, V), X) -> IF_D_3_IN_2_GGA₄(U, V, X, d_3_in_gga₂(U, X))
D_3_IN_GGA₂(power_2₂(U, V), X) -> IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_in_g₁(V))
D_3_IN_GGA₂(times_2₂(U, V), X) -> D_3_IN_GGA₂(U, X)

The TRS R consists of the following rules:

d_3_in_gga₂(X, X) -> d_3_out_gga₁(1_0)
d_3_in_gga₂(T, underscore) -> if_d_3_in_1_gga₁(isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₁(isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₁(isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₁(isnumber_1_out_g) -> isnumber_1_out_g
if_isnumber_1_in_1_g₁(isnumber_1_out_g) -> isnumber_1_out_g
if_d_3_in_1_gga₁(isnumber_1_out_g) -> d_3_out_gga₁(0_0)
d_3_in_gga₂(times_2₂(U, V), X) -> if_d_3_in_2_gga₄(U, V, X, d_3_in_gga₂(U, X))
d_3_in_gga₂(div_2₂(U, V), X) -> if_d_3_in_4_gga₁(d_3_in_gga₂(times_2₂(U, power_2₂(V, p_1₁(0_0))), X))
d_3_in_gga₂(power_2₂(U, V), X) -> if_d_3_in_5_gga₄(U, V, X, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₄(U, V, X, isnumber_1_out_g) -> if_d_3_in_6_gga₃(U, V, d_3_in_gga₂(U, X))
if_d_3_in_6_gga₃(U, V, d_3_out_gga₁(W)) -> d_3_out_gga₁(times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₁(d_3_out_gga₁(W)) -> d_3_out_gga₁(W)
if_d_3_in_2_gga₄(U, V, X, d_3_out_gga₁(A)) -> if_d_3_in_3_gga₄(U, V, A, d_3_in_gga₂(V, X))
if_d_3_in_3_gga₄(U, V, A, d_3_out_gga₁(B)) -> d_3_out_gga₁(+₂(times_2₂(B, U), times_2₂(A, V)))

The set Q consists of the following terms:

d_3_in_gga₂(x0, x1)
isnumber_1_in_g₁(x0)
if_isnumber_1_in_2_g₁(x0)
if_isnumber_1_in_1_g₁(x0)
if_d_3_in_1_gga₁(x0)
if_d_3_in_5_gga₄(x0, x1, x2, x3)
if_d_3_in_6_gga₃(x0, x1, x2)
if_d_3_in_4_gga₁(x0)
if_d_3_in_2_gga₄(x0, x1, x2, x3)
if_d_3_in_3_gga₄(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {D_3_IN_GGA₂, IF_D_3_IN_2_GGA₄, IF_D_3_IN_5_GGA₄}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

D_3_IN_GGA₂(div_2₂(U, V), X) -> D_3_IN_GGA₂(times_2₂(U, power_2₂(V, p_1₁(0_0))), X)

The remaining Dependency Pairs were at least non-strictly be oriented.

IF_D_3_IN_2_GGA₄(U, V, X, d_3_out_gga₁(A)) -> D_3_IN_GGA₂(V, X)
IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_out_g) -> D_3_IN_GGA₂(U, X)
D_3_IN_GGA₂(times_2₂(U, V), X) -> IF_D_3_IN_2_GGA₄(U, V, X, d_3_in_gga₂(U, X))
D_3_IN_GGA₂(power_2₂(U, V), X) -> IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_in_g₁(V))
D_3_IN_GGA₂(times_2₂(U, V), X) -> D_3_IN_GGA₂(U, X)

With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:

POL(D_3_IN_GGA₂(x₁, x₂)) = x₁
POL(0_0) = 0
POL(if_isnumber_1_in_1_g₁(x₁)) = 0
POL(if_d_3_in_3_gga₄(x₁, x₂, x₃, x₄)) = 0
POL(power_2₂(x₁, x₂)) = x₁
POL(if_d_3_in_1_gga₁(x₁)) = 0
POL(IF_D_3_IN_5_GGA₄(x₁, x₂, x₃, x₄)) = x₁
POL(times_2₂(x₁, x₂)) = x₁ + x₂
POL(p_1₁(x₁)) = 0
POL(if_isnumber_1_in_2_g₁(x₁)) = 0
POL(d_3_in_gga₂(x₁, x₂)) = 0
POL(if_d_3_in_6_gga₃(x₁, x₂, x₃)) = 0
POL(isnumber_1_out_g) = 0
POL(d_3_out_gga₁(x₁)) = 0
POL(isnumber_1_in_g₁(x₁)) = 0
POL(if_d_3_in_2_gga₄(x₁, x₂, x₃, x₄)) = 0
POL(+₂(x₁, x₂)) = 0
POL(if_d_3_in_5_gga₄(x₁, x₂, x₃, x₄)) = 0
POL(IF_D_3_IN_2_GGA₄(x₁, x₂, x₃, x₄)) = x₂
POL(if_d_3_in_4_gga₁(x₁)) = 0
POL(s_1₁(x₁)) = 0
POL(1_0) = 0
POL(div_2₂(x₁, x₂)) = 1 + x₁ + x₂

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

                  ↳ QDP

                    ↳ QDPPoloProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

IF_D_3_IN_2_GGA₄(U, V, X, d_3_out_gga₁(A)) -> D_3_IN_GGA₂(V, X)
IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_out_g) -> D_3_IN_GGA₂(U, X)
D_3_IN_GGA₂(times_2₂(U, V), X) -> IF_D_3_IN_2_GGA₄(U, V, X, d_3_in_gga₂(U, X))
D_3_IN_GGA₂(power_2₂(U, V), X) -> IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_in_g₁(V))
D_3_IN_GGA₂(times_2₂(U, V), X) -> D_3_IN_GGA₂(U, X)

The TRS R consists of the following rules:

d_3_in_gga₂(X, X) -> d_3_out_gga₁(1_0)
d_3_in_gga₂(T, underscore) -> if_d_3_in_1_gga₁(isnumber_1_in_g₁(T))
isnumber_1_in_g₁(0_0) -> isnumber_1_out_g
isnumber_1_in_g₁(s_1₁(X)) -> if_isnumber_1_in_1_g₁(isnumber_1_in_g₁(X))
isnumber_1_in_g₁(p_1₁(X)) -> if_isnumber_1_in_2_g₁(isnumber_1_in_g₁(X))
if_isnumber_1_in_2_g₁(isnumber_1_out_g) -> isnumber_1_out_g
if_isnumber_1_in_1_g₁(isnumber_1_out_g) -> isnumber_1_out_g
if_d_3_in_1_gga₁(isnumber_1_out_g) -> d_3_out_gga₁(0_0)
d_3_in_gga₂(times_2₂(U, V), X) -> if_d_3_in_2_gga₄(U, V, X, d_3_in_gga₂(U, X))
d_3_in_gga₂(div_2₂(U, V), X) -> if_d_3_in_4_gga₁(d_3_in_gga₂(times_2₂(U, power_2₂(V, p_1₁(0_0))), X))
d_3_in_gga₂(power_2₂(U, V), X) -> if_d_3_in_5_gga₄(U, V, X, isnumber_1_in_g₁(V))
if_d_3_in_5_gga₄(U, V, X, isnumber_1_out_g) -> if_d_3_in_6_gga₃(U, V, d_3_in_gga₂(U, X))
if_d_3_in_6_gga₃(U, V, d_3_out_gga₁(W)) -> d_3_out_gga₁(times_2₂(V, times_2₂(W, power_2₂(U, p_1₁(V)))))
if_d_3_in_4_gga₁(d_3_out_gga₁(W)) -> d_3_out_gga₁(W)
if_d_3_in_2_gga₄(U, V, X, d_3_out_gga₁(A)) -> if_d_3_in_3_gga₄(U, V, A, d_3_in_gga₂(V, X))
if_d_3_in_3_gga₄(U, V, A, d_3_out_gga₁(B)) -> d_3_out_gga₁(+₂(times_2₂(B, U), times_2₂(A, V)))

The set Q consists of the following terms:

d_3_in_gga₂(x0, x1)
isnumber_1_in_g₁(x0)
if_isnumber_1_in_2_g₁(x0)
if_isnumber_1_in_1_g₁(x0)
if_d_3_in_1_gga₁(x0)
if_d_3_in_5_gga₄(x0, x1, x2, x3)
if_d_3_in_6_gga₃(x0, x1, x2)
if_d_3_in_4_gga₁(x0)
if_d_3_in_2_gga₄(x0, x1, x2, x3)
if_d_3_in_3_gga₄(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {D_3_IN_GGA₂, IF_D_3_IN_2_GGA₄, IF_D_3_IN_5_GGA₄}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

D_3_IN_GGA₂(times_2₂(U, V), X) -> IF_D_3_IN_2_GGA₄(U, V, X, d_3_in_gga₂(U, X))
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3
D_3_IN_GGA₂(power_2₂(U, V), X) -> IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_in_g₁(V))
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3
D_3_IN_GGA₂(times_2₂(U, V), X) -> D_3_IN_GGA₂(U, X)
The graph contains the following edges 1 > 1, 2 >= 2
IF_D_3_IN_2_GGA₄(U, V, X, d_3_out_gga₁(A)) -> D_3_IN_GGA₂(V, X)
The graph contains the following edges 2 >= 1, 3 >= 2
IF_D_3_IN_5_GGA₄(U, V, X, isnumber_1_out_g) -> D_3_IN_GGA₂(U, X)
The graph contains the following edges 1 >= 1, 3 >= 2