Left Termination proof of /tmp/tmpSDxKsR/NJ3.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

ackerman₃(0₀, N, s₁(N)).
ackerman₃(s₁(M), 0₀, Res) :- ackerman₃(M, s₁(0₀), Res).
ackerman₃(s₁(M), s₁(N), Res) :- ackerman₃(s₁(M), N, Res1), ackerman₃(M, Res1, Res).

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

ackerman_3_in_gga₃(0_0, N, s_1₁(N)) -> ackerman_3_out_gga₃(0_0, N, s_1₁(N))
ackerman_3_in_gga₃(s_1₁(M), 0_0, Res) -> if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ackerman_3_in_gga₃(s_1₁(M), s_1₁(N), Res) -> if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_out_gga₃(M, Res1, Res)) -> ackerman_3_out_gga₃(s_1₁(M), s_1₁(N), Res)
if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_out_gga₃(M, s_1₁(0_0), Res)) -> ackerman_3_out_gga₃(s_1₁(M), 0_0, Res)

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:

ackerman_3_in_gga₃(0_0, N, s_1₁(N)) -> ackerman_3_out_gga₃(0_0, N, s_1₁(N))
ackerman_3_in_gga₃(s_1₁(M), 0_0, Res) -> if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ackerman_3_in_gga₃(s_1₁(M), s_1₁(N), Res) -> if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_out_gga₃(M, Res1, Res)) -> ackerman_3_out_gga₃(s_1₁(M), s_1₁(N), Res)
if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_out_gga₃(M, s_1₁(0_0), Res)) -> ackerman_3_out_gga₃(s_1₁(M), 0_0, Res)

ACKERMAN_3_IN_GGA₃(s_1₁(M), 0_0, Res) -> IF_ACKERMAN_3_IN_1_GGA₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ACKERMAN_3_IN_GGA₃(s_1₁(M), 0_0, Res) -> ACKERMAN_3_IN_GGA₃(M, s_1₁(0_0), Res)
ACKERMAN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Res) -> IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
ACKERMAN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Res) -> ACKERMAN_3_IN_GGA₃(s_1₁(M), N, Res1)
IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> IF_ACKERMAN_3_IN_3_GGA₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> ACKERMAN_3_IN_GGA₃(M, Res1, Res)

The TRS R consists of the following rules:

ackerman_3_in_gga₃(0_0, N, s_1₁(N)) -> ackerman_3_out_gga₃(0_0, N, s_1₁(N))
ackerman_3_in_gga₃(s_1₁(M), 0_0, Res) -> if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ackerman_3_in_gga₃(s_1₁(M), s_1₁(N), Res) -> if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_out_gga₃(M, Res1, Res)) -> ackerman_3_out_gga₃(s_1₁(M), s_1₁(N), Res)
if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_out_gga₃(M, s_1₁(0_0), Res)) -> ackerman_3_out_gga₃(s_1₁(M), 0_0, Res)

The argument filtering Pi contains the following mapping:
ackerman_3_in_gga₃(x1, x2, x3) = ackerman_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
ackerman_3_out_gga₃(x1, x2, x3) = ackerman_3_out_gga₁(x3)
if_ackerman_3_in_1_gga₃(x1, x2, x3) = if_ackerman_3_in_1_gga₁(x3)
if_ackerman_3_in_2_gga₄(x1, x2, x3, x4) = if_ackerman_3_in_2_gga₂(x1, x4)
if_ackerman_3_in_3_gga₅(x1, x2, x3, x4, x5) = if_ackerman_3_in_3_gga₁(x5)
IF_ACKERMAN_3_IN_3_GGA₅(x1, x2, x3, x4, x5) = IF_ACKERMAN_3_IN_3_GGA₁(x5)
ACKERMAN_3_IN_GGA₃(x1, x2, x3) = ACKERMAN_3_IN_GGA₂(x1, x2)
IF_ACKERMAN_3_IN_1_GGA₃(x1, x2, x3) = IF_ACKERMAN_3_IN_1_GGA₁(x3)
IF_ACKERMAN_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_ACKERMAN_3_IN_2_GGA₂(x1, x4)

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:

ACKERMAN_3_IN_GGA₃(s_1₁(M), 0_0, Res) -> IF_ACKERMAN_3_IN_1_GGA₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ACKERMAN_3_IN_GGA₃(s_1₁(M), 0_0, Res) -> ACKERMAN_3_IN_GGA₃(M, s_1₁(0_0), Res)
ACKERMAN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Res) -> IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
ACKERMAN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Res) -> ACKERMAN_3_IN_GGA₃(s_1₁(M), N, Res1)
IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> IF_ACKERMAN_3_IN_3_GGA₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> ACKERMAN_3_IN_GGA₃(M, Res1, Res)

The TRS R consists of the following rules:

ackerman_3_in_gga₃(0_0, N, s_1₁(N)) -> ackerman_3_out_gga₃(0_0, N, s_1₁(N))
ackerman_3_in_gga₃(s_1₁(M), 0_0, Res) -> if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ackerman_3_in_gga₃(s_1₁(M), s_1₁(N), Res) -> if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_out_gga₃(M, Res1, Res)) -> ackerman_3_out_gga₃(s_1₁(M), s_1₁(N), Res)
if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_out_gga₃(M, s_1₁(0_0), Res)) -> ackerman_3_out_gga₃(s_1₁(M), 0_0, Res)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

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

ACKERMAN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Res) -> ACKERMAN_3_IN_GGA₃(s_1₁(M), N, Res1)
ACKERMAN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Res) -> IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
ACKERMAN_3_IN_GGA₃(s_1₁(M), 0_0, Res) -> ACKERMAN_3_IN_GGA₃(M, s_1₁(0_0), Res)
IF_ACKERMAN_3_IN_2_GGA₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> ACKERMAN_3_IN_GGA₃(M, Res1, Res)

The TRS R consists of the following rules:

ackerman_3_in_gga₃(0_0, N, s_1₁(N)) -> ackerman_3_out_gga₃(0_0, N, s_1₁(N))
ackerman_3_in_gga₃(s_1₁(M), 0_0, Res) -> if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_in_gga₃(M, s_1₁(0_0), Res))
ackerman_3_in_gga₃(s_1₁(M), s_1₁(N), Res) -> if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_in_gga₃(s_1₁(M), N, Res1))
if_ackerman_3_in_2_gga₄(M, N, Res, ackerman_3_out_gga₃(s_1₁(M), N, Res1)) -> if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_in_gga₃(M, Res1, Res))
if_ackerman_3_in_3_gga₅(M, N, Res, Res1, ackerman_3_out_gga₃(M, Res1, Res)) -> ackerman_3_out_gga₃(s_1₁(M), s_1₁(N), Res)
if_ackerman_3_in_1_gga₃(M, Res, ackerman_3_out_gga₃(M, s_1₁(0_0), Res)) -> ackerman_3_out_gga₃(s_1₁(M), 0_0, Res)

The argument filtering Pi contains the following mapping:
ackerman_3_in_gga₃(x1, x2, x3) = ackerman_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
ackerman_3_out_gga₃(x1, x2, x3) = ackerman_3_out_gga₁(x3)
if_ackerman_3_in_1_gga₃(x1, x2, x3) = if_ackerman_3_in_1_gga₁(x3)
if_ackerman_3_in_2_gga₄(x1, x2, x3, x4) = if_ackerman_3_in_2_gga₂(x1, x4)
if_ackerman_3_in_3_gga₅(x1, x2, x3, x4, x5) = if_ackerman_3_in_3_gga₁(x5)
ACKERMAN_3_IN_GGA₃(x1, x2, x3) = ACKERMAN_3_IN_GGA₂(x1, x2)
IF_ACKERMAN_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_ACKERMAN_3_IN_2_GGA₂(x1, 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

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPSizeChangeProof

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

ACKERMAN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> ACKERMAN_3_IN_GGA₂(s_1₁(M), N)
ACKERMAN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> IF_ACKERMAN_3_IN_2_GGA₂(M, ackerman_3_in_gga₂(s_1₁(M), N))
ACKERMAN_3_IN_GGA₂(s_1₁(M), 0_0) -> ACKERMAN_3_IN_GGA₂(M, s_1₁(0_0))
IF_ACKERMAN_3_IN_2_GGA₂(M, ackerman_3_out_gga₁(Res1)) -> ACKERMAN_3_IN_GGA₂(M, Res1)

The TRS R consists of the following rules:

ackerman_3_in_gga₂(0_0, N) -> ackerman_3_out_gga₁(s_1₁(N))
ackerman_3_in_gga₂(s_1₁(M), 0_0) -> if_ackerman_3_in_1_gga₁(ackerman_3_in_gga₂(M, s_1₁(0_0)))
ackerman_3_in_gga₂(s_1₁(M), s_1₁(N)) -> if_ackerman_3_in_2_gga₂(M, ackerman_3_in_gga₂(s_1₁(M), N))
if_ackerman_3_in_2_gga₂(M, ackerman_3_out_gga₁(Res1)) -> if_ackerman_3_in_3_gga₁(ackerman_3_in_gga₂(M, Res1))
if_ackerman_3_in_3_gga₁(ackerman_3_out_gga₁(Res)) -> ackerman_3_out_gga₁(Res)
if_ackerman_3_in_1_gga₁(ackerman_3_out_gga₁(Res)) -> ackerman_3_out_gga₁(Res)

The set Q consists of the following terms:

ackerman_3_in_gga₂(x0, x1)
if_ackerman_3_in_2_gga₂(x0, x1)
if_ackerman_3_in_3_gga₁(x0)
if_ackerman_3_in_1_gga₁(x0)

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

ACKERMAN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> IF_ACKERMAN_3_IN_2_GGA₂(M, ackerman_3_in_gga₂(s_1₁(M), N))
The graph contains the following edges 1 > 1
IF_ACKERMAN_3_IN_2_GGA₂(M, ackerman_3_out_gga₁(Res1)) -> ACKERMAN_3_IN_GGA₂(M, Res1)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMAN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> ACKERMAN_3_IN_GGA₂(s_1₁(M), N)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMAN_3_IN_GGA₂(s_1₁(M), 0_0) -> ACKERMAN_3_IN_GGA₂(M, s_1₁(0_0))
The graph contains the following edges 1 > 1