Left Termination proof of /tmp/tmp3P8

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

gcd₃(X, Y, D) :- le₂(X, Y), gcd_le₃(X, Y, D).
gcd₃(X, Y, D) :- gt₂(X, Y), gcd_le₃(Y, X, D).
gcd_le₃(0₀, Y, Y).
gcd_le₃(s₁(X), Y, D) :- add₃(s₁(X), Z, Y), gcd₃(s₁(X), Z, D).
gt₂(s₁(X), s₁(Y)) :- gt₂(X, Y).
gt₂(s₁(X), 0₀).
le₂(s₁(X), s₁(Y)) :- le₂(X, Y).
le₂(0₀, s₁(Y)).
le₂(0₀, 0₀).
add₃(s₁(X), Y, s₁(Z)) :- add₃(X, Y, Z).
add₃(0₀, X, X).

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

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

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

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> LE_2_IN_GG₂(X, Y)
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_GG₃(X, Y, le_2_in_gg₂(X, Y))
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_2_GGA₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> ADD_3_IN_GAG₃(s_1₁(X), Z, Y)
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> IF_ADD_3_IN_1_GAG₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> IF_GCD_LE_3_IN_2_GGA₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> GT_2_IN_GG₂(X, Y)
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_GT_2_IN_1_GG₃(X, Y, gt_2_in_gg₂(X, Y))
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_4_GGA₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

The argument filtering Pi contains the following mapping:
gcd_3_in_gga₃(x1, x2, x3) = gcd_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_gcd_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_3_in_1_gga₃(x1, x2, x4)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₁(x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg
if_gcd_3_in_2_gga₄(x1, x2, x3, x4) = if_gcd_3_in_2_gga₁(x4)
gcd_le_3_in_gga₃(x1, x2, x3) = gcd_le_3_in_gga₂(x1, x2)
gcd_le_3_out_gga₃(x1, x2, x3) = gcd_le_3_out_gga₁(x3)
if_gcd_le_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_le_3_in_1_gga₂(x1, x4)
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₁(x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₁(x2)
if_gcd_le_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_gcd_le_3_in_2_gga₁(x5)
if_gcd_3_in_3_gga₄(x1, x2, x3, x4) = if_gcd_3_in_3_gga₃(x1, x2, x4)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₁(x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg
if_gcd_3_in_4_gga₄(x1, x2, x3, x4) = if_gcd_3_in_4_gga₁(x4)
gcd_3_out_gga₃(x1, x2, x3) = gcd_3_out_gga₁(x3)
GT_2_IN_GG₂(x1, x2) = GT_2_IN_GG₂(x1, x2)
IF_GT_2_IN_1_GG₃(x1, x2, x3) = IF_GT_2_IN_1_GG₁(x3)
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₂(x1, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
IF_LE_2_IN_1_GG₃(x1, x2, x3) = IF_LE_2_IN_1_GG₁(x3)
IF_GCD_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_2_GGA₁(x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_ADD_3_IN_1_GAG₄(x1, x2, x3, x4) = IF_ADD_3_IN_1_GAG₁(x4)
IF_GCD_3_IN_4_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_4_GGA₁(x4)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)
LE_2_IN_GG₂(x1, x2) = LE_2_IN_GG₂(x1, x2)
IF_GCD_LE_3_IN_2_GGA₅(x1, x2, x3, x4, x5) = IF_GCD_LE_3_IN_2_GGA₁(x5)
ADD_3_IN_GAG₃(x1, x2, x3) = ADD_3_IN_GAG₂(x1, x3)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> LE_2_IN_GG₂(X, Y)
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_GG₃(X, Y, le_2_in_gg₂(X, Y))
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_2_GGA₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> ADD_3_IN_GAG₃(s_1₁(X), Z, Y)
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> IF_ADD_3_IN_1_GAG₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> IF_GCD_LE_3_IN_2_GGA₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> GT_2_IN_GG₂(X, Y)
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_GT_2_IN_1_GG₃(X, Y, gt_2_in_gg₂(X, Y))
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_4_GGA₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)

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

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {GT_2_IN_GG₂}.
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:

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1₁(x1)
ADD_3_IN_GAG₃(x1, x2, x3) = ADD_3_IN_GAG₂(x1, x3)

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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

ADD_3_IN_GAG₂(s_1₁(X), s_1₁(Z)) -> ADD_3_IN_GAG₂(X, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ADD_3_IN_GAG₂}.
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:

ADD_3_IN_GAG₂(s_1₁(X), s_1₁(Z)) -> ADD_3_IN_GAG₂(X, Z)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)

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

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LE_2_IN_GG₂}.
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:

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

The argument filtering Pi contains the following mapping:
gcd_3_in_gga₃(x1, x2, x3) = gcd_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_gcd_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_3_in_1_gga₃(x1, x2, x4)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₁(x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg
if_gcd_3_in_2_gga₄(x1, x2, x3, x4) = if_gcd_3_in_2_gga₁(x4)
gcd_le_3_in_gga₃(x1, x2, x3) = gcd_le_3_in_gga₂(x1, x2)
gcd_le_3_out_gga₃(x1, x2, x3) = gcd_le_3_out_gga₁(x3)
if_gcd_le_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_le_3_in_1_gga₂(x1, x4)
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₁(x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₁(x2)
if_gcd_le_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_gcd_le_3_in_2_gga₁(x5)
if_gcd_3_in_3_gga₄(x1, x2, x3, x4) = if_gcd_3_in_3_gga₃(x1, x2, x4)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₁(x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg
if_gcd_3_in_4_gga₄(x1, x2, x3, x4) = if_gcd_3_in_4_gga₁(x4)
gcd_3_out_gga₃(x1, x2, x3) = gcd_3_out_gga₁(x3)
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₂(x1, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)

The argument filtering Pi contains the following mapping:
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₁(x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₁(x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₁(x2)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₁(x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₂(x1, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)

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

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

  ↳ PrologToPiTRSProof

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

IF_GCD_LE_3_IN_1_GGA₂(X, add_3_out_gag₁(Z)) -> GCD_3_IN_GGA₂(s_1₁(X), Z)
GCD_LE_3_IN_GGA₂(s_1₁(X), Y) -> IF_GCD_LE_3_IN_1_GGA₂(X, add_3_in_gag₂(s_1₁(X), Y))
IF_GCD_3_IN_1_GGA₃(X, Y, le_2_out_gg) -> GCD_LE_3_IN_GGA₂(X, Y)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_out_gg) -> GCD_LE_3_IN_GGA₂(Y, X)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_1_GGA₃(X, Y, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

add_3_in_gag₂(s_1₁(X), s_1₁(Z)) -> if_add_3_in_1_gag₁(add_3_in_gag₂(X, Z))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₁(gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₁(le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg
if_add_3_in_1_gag₁(add_3_out_gag₁(Y)) -> add_3_out_gag₁(Y)
if_gt_2_in_1_gg₁(gt_2_out_gg) -> gt_2_out_gg
if_le_2_in_1_gg₁(le_2_out_gg) -> le_2_out_gg
add_3_in_gag₂(0_0, X) -> add_3_out_gag₁(X)

The set Q consists of the following terms:

add_3_in_gag₂(x0, x1)
gt_2_in_gg₂(x0, x1)
le_2_in_gg₂(x0, x1)
if_add_3_in_1_gag₁(x0)
if_gt_2_in_1_gg₁(x0)
if_le_2_in_1_gg₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {GCD_3_IN_GGA₂, IF_GCD_LE_3_IN_1_GGA₂, GCD_LE_3_IN_GGA₂, IF_GCD_3_IN_1_GGA₃, IF_GCD_3_IN_3_GGA₃}.
With regard to the inferred argument filtering the predicates were used in the following modes:
gcd₃: (b,b,f)
le₂: (b,b)
gcd_le₃: (b,b,f)
add₃: (b,f,b)
gt₂: (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> LE_2_IN_GG₂(X, Y)
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_GG₃(X, Y, le_2_in_gg₂(X, Y))
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_2_GGA₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> ADD_3_IN_GAG₃(s_1₁(X), Z, Y)
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> IF_ADD_3_IN_1_GAG₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> IF_GCD_LE_3_IN_2_GGA₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> GT_2_IN_GG₂(X, Y)
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_GT_2_IN_1_GG₃(X, Y, gt_2_in_gg₂(X, Y))
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_4_GGA₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

The argument filtering Pi contains the following mapping:
gcd_3_in_gga₃(x1, x2, x3) = gcd_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_gcd_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_3_in_1_gga₃(x1, x2, x4)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₃(x1, x2, x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg₂(x1, x2)
if_gcd_3_in_2_gga₄(x1, x2, x3, x4) = if_gcd_3_in_2_gga₃(x1, x2, x4)
gcd_le_3_in_gga₃(x1, x2, x3) = gcd_le_3_in_gga₂(x1, x2)
gcd_le_3_out_gga₃(x1, x2, x3) = gcd_le_3_out_gga₃(x1, x2, x3)
if_gcd_le_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_le_3_in_1_gga₃(x1, x2, x4)
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₃(x1, x3, x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₃(x1, x2, x3)
if_gcd_le_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_gcd_le_3_in_2_gga₃(x1, x2, x5)
if_gcd_3_in_3_gga₄(x1, x2, x3, x4) = if_gcd_3_in_3_gga₃(x1, x2, x4)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₃(x1, x2, x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg₂(x1, x2)
if_gcd_3_in_4_gga₄(x1, x2, x3, x4) = if_gcd_3_in_4_gga₃(x1, x2, x4)
gcd_3_out_gga₃(x1, x2, x3) = gcd_3_out_gga₃(x1, x2, x3)
GT_2_IN_GG₂(x1, x2) = GT_2_IN_GG₂(x1, x2)
IF_GT_2_IN_1_GG₃(x1, x2, x3) = IF_GT_2_IN_1_GG₃(x1, x2, x3)
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₃(x1, x2, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
IF_LE_2_IN_1_GG₃(x1, x2, x3) = IF_LE_2_IN_1_GG₃(x1, x2, x3)
IF_GCD_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_2_GGA₃(x1, x2, x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_ADD_3_IN_1_GAG₄(x1, x2, x3, x4) = IF_ADD_3_IN_1_GAG₃(x1, x3, x4)
IF_GCD_3_IN_4_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_4_GGA₃(x1, x2, x4)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)
LE_2_IN_GG₂(x1, x2) = LE_2_IN_GG₂(x1, x2)
IF_GCD_LE_3_IN_2_GGA₅(x1, x2, x3, x4, x5) = IF_GCD_LE_3_IN_2_GGA₃(x1, x2, x5)
ADD_3_IN_GAG₃(x1, x2, x3) = ADD_3_IN_GAG₂(x1, x3)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> LE_2_IN_GG₂(X, Y)
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_GG₃(X, Y, le_2_in_gg₂(X, Y))
LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_2_GGA₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> ADD_3_IN_GAG₃(s_1₁(X), Z, Y)
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> IF_ADD_3_IN_1_GAG₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> IF_GCD_LE_3_IN_2_GGA₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
GCD_3_IN_GGA₃(X, Y, D) -> GT_2_IN_GG₂(X, Y)
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_GT_2_IN_1_GG₃(X, Y, gt_2_in_gg₂(X, Y))
GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> IF_GCD_3_IN_4_GGA₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

The argument filtering Pi contains the following mapping:
gcd_3_in_gga₃(x1, x2, x3) = gcd_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_gcd_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_3_in_1_gga₃(x1, x2, x4)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₃(x1, x2, x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg₂(x1, x2)
if_gcd_3_in_2_gga₄(x1, x2, x3, x4) = if_gcd_3_in_2_gga₃(x1, x2, x4)
gcd_le_3_in_gga₃(x1, x2, x3) = gcd_le_3_in_gga₂(x1, x2)
gcd_le_3_out_gga₃(x1, x2, x3) = gcd_le_3_out_gga₃(x1, x2, x3)
if_gcd_le_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_le_3_in_1_gga₃(x1, x2, x4)
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₃(x1, x3, x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₃(x1, x2, x3)
if_gcd_le_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_gcd_le_3_in_2_gga₃(x1, x2, x5)
if_gcd_3_in_3_gga₄(x1, x2, x3, x4) = if_gcd_3_in_3_gga₃(x1, x2, x4)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₃(x1, x2, x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg₂(x1, x2)
if_gcd_3_in_4_gga₄(x1, x2, x3, x4) = if_gcd_3_in_4_gga₃(x1, x2, x4)
gcd_3_out_gga₃(x1, x2, x3) = gcd_3_out_gga₃(x1, x2, x3)
GT_2_IN_GG₂(x1, x2) = GT_2_IN_GG₂(x1, x2)
IF_GT_2_IN_1_GG₃(x1, x2, x3) = IF_GT_2_IN_1_GG₃(x1, x2, x3)
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₃(x1, x2, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
IF_LE_2_IN_1_GG₃(x1, x2, x3) = IF_LE_2_IN_1_GG₃(x1, x2, x3)
IF_GCD_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_2_GGA₃(x1, x2, x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_ADD_3_IN_1_GAG₄(x1, x2, x3, x4) = IF_ADD_3_IN_1_GAG₃(x1, x3, x4)
IF_GCD_3_IN_4_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_4_GGA₃(x1, x2, x4)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)
LE_2_IN_GG₂(x1, x2) = LE_2_IN_GG₂(x1, x2)
IF_GCD_LE_3_IN_2_GGA₅(x1, x2, x3, x4, x5) = IF_GCD_LE_3_IN_2_GGA₃(x1, x2, x5)
ADD_3_IN_GAG₃(x1, x2, x3) = ADD_3_IN_GAG₂(x1, x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 4 SCCs with 9 less nodes.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)

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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)

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

GT_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> GT_2_IN_GG₂(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

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

ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

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

ADD_3_IN_GAG₃(s_1₁(X), Y, s_1₁(Z)) -> ADD_3_IN_GAG₃(X, Y, Z)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

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

ADD_3_IN_GAG₂(s_1₁(X), s_1₁(Z)) -> ADD_3_IN_GAG₂(X, Z)

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

ADD_3_IN_GAG₂(s_1₁(X), s_1₁(Z)) -> ADD_3_IN_GAG₂(X, Z)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)

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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)

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

LE_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_GG₂(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_1_gga₄(X, Y, D, le_2_in_gg₂(X, Y))
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_1_gga₄(X, Y, D, le_2_out_gg₂(X, Y)) -> if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_in_gga₃(X, Y, D))
gcd_le_3_in_gga₃(0_0, Y, Y) -> gcd_le_3_out_gga₃(0_0, Y, Y)
gcd_le_3_in_gga₃(s_1₁(X), Y, D) -> if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gcd_le_3_in_1_gga₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_in_gga₃(s_1₁(X), Z, D))
gcd_3_in_gga₃(X, Y, D) -> if_gcd_3_in_3_gga₄(X, Y, D, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_gcd_3_in_3_gga₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_in_gga₃(Y, X, D))
if_gcd_3_in_4_gga₄(X, Y, D, gcd_le_3_out_gga₃(Y, X, D)) -> gcd_3_out_gga₃(X, Y, D)
if_gcd_le_3_in_2_gga₅(X, Y, D, Z, gcd_3_out_gga₃(s_1₁(X), Z, D)) -> gcd_le_3_out_gga₃(s_1₁(X), Y, D)
if_gcd_3_in_2_gga₄(X, Y, D, gcd_le_3_out_gga₃(X, Y, D)) -> gcd_3_out_gga₃(X, Y, D)

The argument filtering Pi contains the following mapping:
gcd_3_in_gga₃(x1, x2, x3) = gcd_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_gcd_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_3_in_1_gga₃(x1, x2, x4)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₃(x1, x2, x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg₂(x1, x2)
if_gcd_3_in_2_gga₄(x1, x2, x3, x4) = if_gcd_3_in_2_gga₃(x1, x2, x4)
gcd_le_3_in_gga₃(x1, x2, x3) = gcd_le_3_in_gga₂(x1, x2)
gcd_le_3_out_gga₃(x1, x2, x3) = gcd_le_3_out_gga₃(x1, x2, x3)
if_gcd_le_3_in_1_gga₄(x1, x2, x3, x4) = if_gcd_le_3_in_1_gga₃(x1, x2, x4)
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₃(x1, x3, x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₃(x1, x2, x3)
if_gcd_le_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_gcd_le_3_in_2_gga₃(x1, x2, x5)
if_gcd_3_in_3_gga₄(x1, x2, x3, x4) = if_gcd_3_in_3_gga₃(x1, x2, x4)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₃(x1, x2, x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg₂(x1, x2)
if_gcd_3_in_4_gga₄(x1, x2, x3, x4) = if_gcd_3_in_4_gga₃(x1, x2, x4)
gcd_3_out_gga₃(x1, x2, x3) = gcd_3_out_gga₃(x1, x2, x3)
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₃(x1, x2, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₃(s_1₁(X), Z, D)
GCD_LE_3_IN_GGA₃(s_1₁(X), Y, D) -> IF_GCD_LE_3_IN_1_GGA₄(X, Y, D, add_3_in_gag₃(s_1₁(X), Z, Y))
IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(X, Y, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₄(X, Y, D, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₃(Y, X, D)
GCD_3_IN_GGA₃(X, Y, D) -> IF_GCD_3_IN_1_GGA₄(X, Y, D, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

add_3_in_gag₃(s_1₁(X), Y, s_1₁(Z)) -> if_add_3_in_1_gag₄(X, Y, Z, add_3_in_gag₃(X, Y, Z))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_add_3_in_1_gag₄(X, Y, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
add_3_in_gag₃(0_0, X, X) -> add_3_out_gag₃(0_0, X, X)

The argument filtering Pi contains the following mapping:
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
le_2_in_gg₂(x1, x2) = le_2_in_gg₂(x1, x2)
if_le_2_in_1_gg₃(x1, x2, x3) = if_le_2_in_1_gg₃(x1, x2, x3)
le_2_out_gg₂(x1, x2) = le_2_out_gg₂(x1, x2)
add_3_in_gag₃(x1, x2, x3) = add_3_in_gag₂(x1, x3)
if_add_3_in_1_gag₄(x1, x2, x3, x4) = if_add_3_in_1_gag₃(x1, x3, x4)
add_3_out_gag₃(x1, x2, x3) = add_3_out_gag₃(x1, x2, x3)
gt_2_in_gg₂(x1, x2) = gt_2_in_gg₂(x1, x2)
if_gt_2_in_1_gg₃(x1, x2, x3) = if_gt_2_in_1_gg₃(x1, x2, x3)
gt_2_out_gg₂(x1, x2) = gt_2_out_gg₂(x1, x2)
GCD_3_IN_GGA₃(x1, x2, x3) = GCD_3_IN_GGA₂(x1, x2)
IF_GCD_LE_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_LE_3_IN_1_GGA₃(x1, x2, x4)
IF_GCD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_1_GGA₃(x1, x2, x4)
GCD_LE_3_IN_GGA₃(x1, x2, x3) = GCD_LE_3_IN_GGA₂(x1, x2)
IF_GCD_3_IN_3_GGA₄(x1, x2, x3, x4) = IF_GCD_3_IN_3_GGA₃(x1, x2, x4)

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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPPoloProof

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

IF_GCD_LE_3_IN_1_GGA₃(X, Y, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₂(s_1₁(X), Z)
GCD_LE_3_IN_GGA₂(s_1₁(X), Y) -> IF_GCD_LE_3_IN_1_GGA₃(X, Y, add_3_in_gag₂(s_1₁(X), Y))
IF_GCD_3_IN_1_GGA₃(X, Y, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₂(X, Y)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₂(Y, X)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_1_GGA₃(X, Y, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

add_3_in_gag₂(s_1₁(X), s_1₁(Z)) -> if_add_3_in_1_gag₃(X, Z, add_3_in_gag₂(X, Z))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_add_3_in_1_gag₃(X, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
add_3_in_gag₂(0_0, X) -> add_3_out_gag₃(0_0, X, X)

The set Q consists of the following terms:

add_3_in_gag₂(x0, x1)
gt_2_in_gg₂(x0, x1)
le_2_in_gg₂(x0, x1)
if_add_3_in_1_gag₃(x0, x1, x2)
if_gt_2_in_1_gg₃(x0, x1, x2)
if_le_2_in_1_gg₃(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {GCD_3_IN_GGA₂, IF_GCD_LE_3_IN_1_GGA₃, GCD_LE_3_IN_GGA₂, IF_GCD_3_IN_1_GGA₃, IF_GCD_3_IN_3_GGA₃}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

GCD_LE_3_IN_GGA₂(s_1₁(X), Y) -> IF_GCD_LE_3_IN_1_GGA₃(X, Y, add_3_in_gag₂(s_1₁(X), Y))

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

IF_GCD_LE_3_IN_1_GGA₃(X, Y, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₂(s_1₁(X), Z)
IF_GCD_3_IN_1_GGA₃(X, Y, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₂(X, Y)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₂(Y, X)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_1_GGA₃(X, Y, le_2_in_gg₂(X, Y))

With the implicit AFS we had to orient the following set of usable rules non-strictly.

add_3_in_gag₂(0_0, X) -> add_3_out_gag₃(0_0, X, X)
add_3_in_gag₂(s_1₁(X), s_1₁(Z)) -> if_add_3_in_1_gag₃(X, Z, add_3_in_gag₂(X, Z))
if_add_3_in_1_gag₃(X, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))

Used ordering: POLO with Polynomial interpretation:

POL(add_3_in_gag₂(x₁, x₂)) = x₂
POL(0_0) = 0
POL(gt_2_in_gg₂(x₁, x₂)) = 0
POL(add_3_out_gag₃(x₁, x₂, x₃)) = x₁ + x₂
POL(if_gt_2_in_1_gg₃(x₁, x₂, x₃)) = 0
POL(le_2_out_gg₂(x₁, x₂)) = 0
POL(if_add_3_in_1_gag₃(x₁, x₂, x₃)) = 1 + x₃
POL(IF_GCD_3_IN_3_GGA₃(x₁, x₂, x₃)) = x₁ + x₂
POL(if_le_2_in_1_gg₃(x₁, x₂, x₃)) = 0
POL(gt_2_out_gg₂(x₁, x₂)) = 0
POL(IF_GCD_3_IN_1_GGA₃(x₁, x₂, x₃)) = x₁ + x₂
POL(GCD_LE_3_IN_GGA₂(x₁, x₂)) = x₁ + x₂
POL(IF_GCD_LE_3_IN_1_GGA₃(x₁, x₂, x₃)) = x₃
POL(le_2_in_gg₂(x₁, x₂)) = 0
POL(s_1₁(x₁)) = 1 + x₁
POL(GCD_3_IN_GGA₂(x₁, x₂)) = x₁ + x₂

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPPoloProof

                          ↳ QDP

                            ↳ DependencyGraphProof

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

IF_GCD_LE_3_IN_1_GGA₃(X, Y, add_3_out_gag₃(s_1₁(X), Z, Y)) -> GCD_3_IN_GGA₂(s_1₁(X), Z)
IF_GCD_3_IN_1_GGA₃(X, Y, le_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₂(X, Y)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_in_gg₂(X, Y))
IF_GCD_3_IN_3_GGA₃(X, Y, gt_2_out_gg₂(X, Y)) -> GCD_LE_3_IN_GGA₂(Y, X)
GCD_3_IN_GGA₂(X, Y) -> IF_GCD_3_IN_1_GGA₃(X, Y, le_2_in_gg₂(X, Y))

The TRS R consists of the following rules:

add_3_in_gag₂(s_1₁(X), s_1₁(Z)) -> if_add_3_in_1_gag₃(X, Z, add_3_in_gag₂(X, Z))
gt_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_gt_2_in_1_gg₃(X, Y, gt_2_in_gg₂(X, Y))
gt_2_in_gg₂(s_1₁(X), 0_0) -> gt_2_out_gg₂(s_1₁(X), 0_0)
le_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_gg₃(X, Y, le_2_in_gg₂(X, Y))
le_2_in_gg₂(0_0, s_1₁(Y)) -> le_2_out_gg₂(0_0, s_1₁(Y))
le_2_in_gg₂(0_0, 0_0) -> le_2_out_gg₂(0_0, 0_0)
if_add_3_in_1_gag₃(X, Z, add_3_out_gag₃(X, Y, Z)) -> add_3_out_gag₃(s_1₁(X), Y, s_1₁(Z))
if_gt_2_in_1_gg₃(X, Y, gt_2_out_gg₂(X, Y)) -> gt_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_le_2_in_1_gg₃(X, Y, le_2_out_gg₂(X, Y)) -> le_2_out_gg₂(s_1₁(X), s_1₁(Y))
add_3_in_gag₂(0_0, X) -> add_3_out_gag₃(0_0, X, X)

The set Q consists of the following terms:

add_3_in_gag₂(x0, x1)
gt_2_in_gg₂(x0, x1)
le_2_in_gg₂(x0, x1)
if_add_3_in_1_gag₃(x0, x1, x2)
if_gt_2_in_1_gg₃(x0, x1, x2)
if_le_2_in_1_gg₃(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {GCD_3_IN_GGA₂, IF_GCD_LE_3_IN_1_GGA₃, GCD_LE_3_IN_GGA₂, IF_GCD_3_IN_1_GGA₃, IF_GCD_3_IN_3_GGA₃}.
The approximation of the Dependency Graph contains 0 SCCs with 5 less nodes.