Left Termination proof of /tmp/tmppHQlwl/fib

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

↳ PROLOG

  ↳ PrologToPiTRSProof

add₃(0₀, 0₀, 0₀).
add₃(s₁(X), Y, s₁(N)) :- add₃(X, Y, N).
add₃(X, s₁(Y), s₁(N)) :- add₃(X, Y, N).
fib₂(0₀, 0₀).
fib₂(s₁(0₀), s₁(0₀)).
fib₂(s₁²(X), N) :- fib₂(s₁(X), N1), fib₂(X, N2), add₃(N1, N2, N).

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

fib_2_in_ga₂(0_0, 0_0) -> fib_2_out_ga₂(0_0, 0_0)
fib_2_in_ga₂(s_1₁(0_0), s_1₁(0_0)) -> fib_2_out_ga₂(s_1₁(0_0), s_1₁(0_0))
fib_2_in_ga₂(s_1₁(s_1₁(X)), N) -> if_fib_2_in_1_ga₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
if_fib_2_in_1_ga₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> if_fib_2_in_2_ga₄(X, N, N1, fib_2_in_ga₂(X, N2))
if_fib_2_in_2_ga₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
add_3_in_gga₃(0_0, 0_0, 0_0) -> add_3_out_gga₃(0_0, 0_0, 0_0)
add_3_in_gga₃(s_1₁(X), Y, s_1₁(N)) -> if_add_3_in_1_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
add_3_in_gga₃(X, s_1₁(Y), s_1₁(N)) -> if_add_3_in_2_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
if_add_3_in_2_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(X, s_1₁(Y), s_1₁(N))
if_add_3_in_1_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(s_1₁(X), Y, s_1₁(N))
if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_out_gga₃(N1, N2, N)) -> fib_2_out_ga₂(s_1₁(s_1₁(X)), N)

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:

fib_2_in_ga₂(0_0, 0_0) -> fib_2_out_ga₂(0_0, 0_0)
fib_2_in_ga₂(s_1₁(0_0), s_1₁(0_0)) -> fib_2_out_ga₂(s_1₁(0_0), s_1₁(0_0))
fib_2_in_ga₂(s_1₁(s_1₁(X)), N) -> if_fib_2_in_1_ga₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
if_fib_2_in_1_ga₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> if_fib_2_in_2_ga₄(X, N, N1, fib_2_in_ga₂(X, N2))
if_fib_2_in_2_ga₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
add_3_in_gga₃(0_0, 0_0, 0_0) -> add_3_out_gga₃(0_0, 0_0, 0_0)
add_3_in_gga₃(s_1₁(X), Y, s_1₁(N)) -> if_add_3_in_1_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
add_3_in_gga₃(X, s_1₁(Y), s_1₁(N)) -> if_add_3_in_2_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
if_add_3_in_2_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(X, s_1₁(Y), s_1₁(N))
if_add_3_in_1_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(s_1₁(X), Y, s_1₁(N))
if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_out_gga₃(N1, N2, N)) -> fib_2_out_ga₂(s_1₁(s_1₁(X)), N)

FIB_2_IN_GA₂(s_1₁(s_1₁(X)), N) -> IF_FIB_2_IN_1_GA₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
FIB_2_IN_GA₂(s_1₁(s_1₁(X)), N) -> FIB_2_IN_GA₂(s_1₁(X), N1)
IF_FIB_2_IN_1_GA₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> IF_FIB_2_IN_2_GA₄(X, N, N1, fib_2_in_ga₂(X, N2))
IF_FIB_2_IN_1_GA₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> FIB_2_IN_GA₂(X, N2)
IF_FIB_2_IN_2_GA₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> IF_FIB_2_IN_3_GA₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
IF_FIB_2_IN_2_GA₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> ADD_3_IN_GGA₃(N1, N2, N)
ADD_3_IN_GGA₃(s_1₁(X), Y, s_1₁(N)) -> IF_ADD_3_IN_1_GGA₄(X, Y, N, add_3_in_gga₃(X, Y, N))
ADD_3_IN_GGA₃(s_1₁(X), Y, s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)
ADD_3_IN_GGA₃(X, s_1₁(Y), s_1₁(N)) -> IF_ADD_3_IN_2_GGA₄(X, Y, N, add_3_in_gga₃(X, Y, N))
ADD_3_IN_GGA₃(X, s_1₁(Y), s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)

The TRS R consists of the following rules:

fib_2_in_ga₂(0_0, 0_0) -> fib_2_out_ga₂(0_0, 0_0)
fib_2_in_ga₂(s_1₁(0_0), s_1₁(0_0)) -> fib_2_out_ga₂(s_1₁(0_0), s_1₁(0_0))
fib_2_in_ga₂(s_1₁(s_1₁(X)), N) -> if_fib_2_in_1_ga₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
if_fib_2_in_1_ga₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> if_fib_2_in_2_ga₄(X, N, N1, fib_2_in_ga₂(X, N2))
if_fib_2_in_2_ga₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
add_3_in_gga₃(0_0, 0_0, 0_0) -> add_3_out_gga₃(0_0, 0_0, 0_0)
add_3_in_gga₃(s_1₁(X), Y, s_1₁(N)) -> if_add_3_in_1_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
add_3_in_gga₃(X, s_1₁(Y), s_1₁(N)) -> if_add_3_in_2_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
if_add_3_in_2_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(X, s_1₁(Y), s_1₁(N))
if_add_3_in_1_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(s_1₁(X), Y, s_1₁(N))
if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_out_gga₃(N1, N2, N)) -> fib_2_out_ga₂(s_1₁(s_1₁(X)), N)

The argument filtering Pi contains the following mapping:
fib_2_in_ga₂(x1, x2) = fib_2_in_ga₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
fib_2_out_ga₂(x1, x2) = fib_2_out_ga₁(x2)
if_fib_2_in_1_ga₃(x1, x2, x3) = if_fib_2_in_1_ga₂(x1, x3)
if_fib_2_in_2_ga₄(x1, x2, x3, x4) = if_fib_2_in_2_ga₂(x3, x4)
if_fib_2_in_3_ga₅(x1, x2, x3, x4, x5) = if_fib_2_in_3_ga₁(x5)
add_3_in_gga₃(x1, x2, x3) = add_3_in_gga₂(x1, x2)
add_3_out_gga₃(x1, x2, x3) = add_3_out_gga₁(x3)
if_add_3_in_1_gga₄(x1, x2, x3, x4) = if_add_3_in_1_gga₁(x4)
if_add_3_in_2_gga₄(x1, x2, x3, x4) = if_add_3_in_2_gga₁(x4)
IF_FIB_2_IN_1_GA₃(x1, x2, x3) = IF_FIB_2_IN_1_GA₂(x1, x3)
IF_ADD_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_ADD_3_IN_2_GGA₁(x4)
IF_ADD_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_ADD_3_IN_1_GGA₁(x4)
ADD_3_IN_GGA₃(x1, x2, x3) = ADD_3_IN_GGA₂(x1, x2)
FIB_2_IN_GA₂(x1, x2) = FIB_2_IN_GA₁(x1)
IF_FIB_2_IN_2_GA₄(x1, x2, x3, x4) = IF_FIB_2_IN_2_GA₂(x3, x4)
IF_FIB_2_IN_3_GA₅(x1, x2, x3, x4, x5) = IF_FIB_2_IN_3_GA₁(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:

FIB_2_IN_GA₂(s_1₁(s_1₁(X)), N) -> IF_FIB_2_IN_1_GA₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
FIB_2_IN_GA₂(s_1₁(s_1₁(X)), N) -> FIB_2_IN_GA₂(s_1₁(X), N1)
IF_FIB_2_IN_1_GA₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> IF_FIB_2_IN_2_GA₄(X, N, N1, fib_2_in_ga₂(X, N2))
IF_FIB_2_IN_1_GA₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> FIB_2_IN_GA₂(X, N2)
IF_FIB_2_IN_2_GA₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> IF_FIB_2_IN_3_GA₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
IF_FIB_2_IN_2_GA₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> ADD_3_IN_GGA₃(N1, N2, N)
ADD_3_IN_GGA₃(s_1₁(X), Y, s_1₁(N)) -> IF_ADD_3_IN_1_GGA₄(X, Y, N, add_3_in_gga₃(X, Y, N))
ADD_3_IN_GGA₃(s_1₁(X), Y, s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)
ADD_3_IN_GGA₃(X, s_1₁(Y), s_1₁(N)) -> IF_ADD_3_IN_2_GGA₄(X, Y, N, add_3_in_gga₃(X, Y, N))
ADD_3_IN_GGA₃(X, s_1₁(Y), s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)

The TRS R consists of the following rules:

fib_2_in_ga₂(0_0, 0_0) -> fib_2_out_ga₂(0_0, 0_0)
fib_2_in_ga₂(s_1₁(0_0), s_1₁(0_0)) -> fib_2_out_ga₂(s_1₁(0_0), s_1₁(0_0))
fib_2_in_ga₂(s_1₁(s_1₁(X)), N) -> if_fib_2_in_1_ga₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
if_fib_2_in_1_ga₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> if_fib_2_in_2_ga₄(X, N, N1, fib_2_in_ga₂(X, N2))
if_fib_2_in_2_ga₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
add_3_in_gga₃(0_0, 0_0, 0_0) -> add_3_out_gga₃(0_0, 0_0, 0_0)
add_3_in_gga₃(s_1₁(X), Y, s_1₁(N)) -> if_add_3_in_1_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
add_3_in_gga₃(X, s_1₁(Y), s_1₁(N)) -> if_add_3_in_2_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
if_add_3_in_2_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(X, s_1₁(Y), s_1₁(N))
if_add_3_in_1_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(s_1₁(X), Y, s_1₁(N))
if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_out_gga₃(N1, N2, N)) -> fib_2_out_ga₂(s_1₁(s_1₁(X)), N)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

ADD_3_IN_GGA₃(s_1₁(X), Y, s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)
ADD_3_IN_GGA₃(X, s_1₁(Y), s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)

The TRS R consists of the following rules:

fib_2_in_ga₂(0_0, 0_0) -> fib_2_out_ga₂(0_0, 0_0)
fib_2_in_ga₂(s_1₁(0_0), s_1₁(0_0)) -> fib_2_out_ga₂(s_1₁(0_0), s_1₁(0_0))
fib_2_in_ga₂(s_1₁(s_1₁(X)), N) -> if_fib_2_in_1_ga₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
if_fib_2_in_1_ga₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> if_fib_2_in_2_ga₄(X, N, N1, fib_2_in_ga₂(X, N2))
if_fib_2_in_2_ga₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
add_3_in_gga₃(0_0, 0_0, 0_0) -> add_3_out_gga₃(0_0, 0_0, 0_0)
add_3_in_gga₃(s_1₁(X), Y, s_1₁(N)) -> if_add_3_in_1_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
add_3_in_gga₃(X, s_1₁(Y), s_1₁(N)) -> if_add_3_in_2_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
if_add_3_in_2_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(X, s_1₁(Y), s_1₁(N))
if_add_3_in_1_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(s_1₁(X), Y, s_1₁(N))
if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_out_gga₃(N1, N2, N)) -> fib_2_out_ga₂(s_1₁(s_1₁(X)), N)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

ADD_3_IN_GGA₃(s_1₁(X), Y, s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)
ADD_3_IN_GGA₃(X, s_1₁(Y), s_1₁(N)) -> ADD_3_IN_GGA₃(X, Y, N)

R is empty.
The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1₁(x1)
ADD_3_IN_GGA₃(x1, x2, x3) = ADD_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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

ADD_3_IN_GGA₂(s_1₁(X), Y) -> ADD_3_IN_GGA₂(X, Y)
ADD_3_IN_GGA₂(X, s_1₁(Y)) -> ADD_3_IN_GGA₂(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 {ADD_3_IN_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:

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

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

IF_FIB_2_IN_1_GA₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> FIB_2_IN_GA₂(X, N2)
FIB_2_IN_GA₂(s_1₁(s_1₁(X)), N) -> FIB_2_IN_GA₂(s_1₁(X), N1)
FIB_2_IN_GA₂(s_1₁(s_1₁(X)), N) -> IF_FIB_2_IN_1_GA₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))

The TRS R consists of the following rules:

fib_2_in_ga₂(0_0, 0_0) -> fib_2_out_ga₂(0_0, 0_0)
fib_2_in_ga₂(s_1₁(0_0), s_1₁(0_0)) -> fib_2_out_ga₂(s_1₁(0_0), s_1₁(0_0))
fib_2_in_ga₂(s_1₁(s_1₁(X)), N) -> if_fib_2_in_1_ga₃(X, N, fib_2_in_ga₂(s_1₁(X), N1))
if_fib_2_in_1_ga₃(X, N, fib_2_out_ga₂(s_1₁(X), N1)) -> if_fib_2_in_2_ga₄(X, N, N1, fib_2_in_ga₂(X, N2))
if_fib_2_in_2_ga₄(X, N, N1, fib_2_out_ga₂(X, N2)) -> if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_in_gga₃(N1, N2, N))
add_3_in_gga₃(0_0, 0_0, 0_0) -> add_3_out_gga₃(0_0, 0_0, 0_0)
add_3_in_gga₃(s_1₁(X), Y, s_1₁(N)) -> if_add_3_in_1_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
add_3_in_gga₃(X, s_1₁(Y), s_1₁(N)) -> if_add_3_in_2_gga₄(X, Y, N, add_3_in_gga₃(X, Y, N))
if_add_3_in_2_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(X, s_1₁(Y), s_1₁(N))
if_add_3_in_1_gga₄(X, Y, N, add_3_out_gga₃(X, Y, N)) -> add_3_out_gga₃(s_1₁(X), Y, s_1₁(N))
if_fib_2_in_3_ga₅(X, N, N1, N2, add_3_out_gga₃(N1, N2, N)) -> fib_2_out_ga₂(s_1₁(s_1₁(X)), N)

The argument filtering Pi contains the following mapping:
fib_2_in_ga₂(x1, x2) = fib_2_in_ga₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
fib_2_out_ga₂(x1, x2) = fib_2_out_ga₁(x2)
if_fib_2_in_1_ga₃(x1, x2, x3) = if_fib_2_in_1_ga₂(x1, x3)
if_fib_2_in_2_ga₄(x1, x2, x3, x4) = if_fib_2_in_2_ga₂(x3, x4)
if_fib_2_in_3_ga₅(x1, x2, x3, x4, x5) = if_fib_2_in_3_ga₁(x5)
add_3_in_gga₃(x1, x2, x3) = add_3_in_gga₂(x1, x2)
add_3_out_gga₃(x1, x2, x3) = add_3_out_gga₁(x3)
if_add_3_in_1_gga₄(x1, x2, x3, x4) = if_add_3_in_1_gga₁(x4)
if_add_3_in_2_gga₄(x1, x2, x3, x4) = if_add_3_in_2_gga₁(x4)
IF_FIB_2_IN_1_GA₃(x1, x2, x3) = IF_FIB_2_IN_1_GA₂(x1, x3)
FIB_2_IN_GA₂(x1, x2) = FIB_2_IN_GA₁(x1)

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

                    ↳ QDPSizeChangeProof

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

IF_FIB_2_IN_1_GA₂(X, fib_2_out_ga₁(N1)) -> FIB_2_IN_GA₁(X)
FIB_2_IN_GA₁(s_1₁(s_1₁(X))) -> FIB_2_IN_GA₁(s_1₁(X))
FIB_2_IN_GA₁(s_1₁(s_1₁(X))) -> IF_FIB_2_IN_1_GA₂(X, fib_2_in_ga₁(s_1₁(X)))

The TRS R consists of the following rules:

fib_2_in_ga₁(0_0) -> fib_2_out_ga₁(0_0)
fib_2_in_ga₁(s_1₁(0_0)) -> fib_2_out_ga₁(s_1₁(0_0))
fib_2_in_ga₁(s_1₁(s_1₁(X))) -> if_fib_2_in_1_ga₂(X, fib_2_in_ga₁(s_1₁(X)))
if_fib_2_in_1_ga₂(X, fib_2_out_ga₁(N1)) -> if_fib_2_in_2_ga₂(N1, fib_2_in_ga₁(X))
if_fib_2_in_2_ga₂(N1, fib_2_out_ga₁(N2)) -> if_fib_2_in_3_ga₁(add_3_in_gga₂(N1, N2))
add_3_in_gga₂(0_0, 0_0) -> add_3_out_gga₁(0_0)
add_3_in_gga₂(s_1₁(X), Y) -> if_add_3_in_1_gga₁(add_3_in_gga₂(X, Y))
add_3_in_gga₂(X, s_1₁(Y)) -> if_add_3_in_2_gga₁(add_3_in_gga₂(X, Y))
if_add_3_in_2_gga₁(add_3_out_gga₁(N)) -> add_3_out_gga₁(s_1₁(N))
if_add_3_in_1_gga₁(add_3_out_gga₁(N)) -> add_3_out_gga₁(s_1₁(N))
if_fib_2_in_3_ga₁(add_3_out_gga₁(N)) -> fib_2_out_ga₁(N)

The set Q consists of the following terms:

fib_2_in_ga₁(x0)
if_fib_2_in_1_ga₂(x0, x1)
if_fib_2_in_2_ga₂(x0, x1)
add_3_in_gga₂(x0, x1)
if_add_3_in_2_gga₁(x0)
if_add_3_in_1_gga₁(x0)
if_fib_2_in_3_ga₁(x0)

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

FIB_2_IN_GA₁(s_1₁(s_1₁(X))) -> IF_FIB_2_IN_1_GA₂(X, fib_2_in_ga₁(s_1₁(X)))
The graph contains the following edges 1 > 1
FIB_2_IN_GA₁(s_1₁(s_1₁(X))) -> FIB_2_IN_GA₁(s_1₁(X))
The graph contains the following edges 1 > 1
IF_FIB_2_IN_1_GA₂(X, fib_2_out_ga₁(N1)) -> FIB_2_IN_GA₁(X)
The graph contains the following edges 1 >= 1