Left Termination proof of /tmp/tmpg7vuMz/p.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

p₁(0₀).
p₁(s₁(X)) :- geq₂(X, Y), p₁(Y).
geq₂(X, X).
geq₂(s₁(X), Y) :- geq₂(X, Y).

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

p_1_in_g₁(0_0) -> p_1_out_g₁(0_0)
p_1_in_g₁(s_1₁(X)) -> if_p_1_in_1_g₂(X, geq_2_in_ga₂(X, Y))
geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)
if_p_1_in_1_g₂(X, geq_2_out_ga₂(X, Y)) -> if_p_1_in_2_g₃(X, Y, p_1_in_g₁(Y))
if_p_1_in_2_g₃(X, Y, p_1_out_g₁(Y)) -> p_1_out_g₁(s_1₁(X))

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:

p_1_in_g₁(0_0) -> p_1_out_g₁(0_0)
p_1_in_g₁(s_1₁(X)) -> if_p_1_in_1_g₂(X, geq_2_in_ga₂(X, Y))
geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)
if_p_1_in_1_g₂(X, geq_2_out_ga₂(X, Y)) -> if_p_1_in_2_g₃(X, Y, p_1_in_g₁(Y))
if_p_1_in_2_g₃(X, Y, p_1_out_g₁(Y)) -> p_1_out_g₁(s_1₁(X))

P_1_IN_G₁(s_1₁(X)) -> IF_P_1_IN_1_G₂(X, geq_2_in_ga₂(X, Y))
P_1_IN_G₁(s_1₁(X)) -> GEQ_2_IN_GA₂(X, Y)
GEQ_2_IN_GA₂(s_1₁(X), Y) -> IF_GEQ_2_IN_1_GA₃(X, Y, geq_2_in_ga₂(X, Y))
GEQ_2_IN_GA₂(s_1₁(X), Y) -> GEQ_2_IN_GA₂(X, Y)
IF_P_1_IN_1_G₂(X, geq_2_out_ga₂(X, Y)) -> IF_P_1_IN_2_G₃(X, Y, p_1_in_g₁(Y))
IF_P_1_IN_1_G₂(X, geq_2_out_ga₂(X, Y)) -> P_1_IN_G₁(Y)

The TRS R consists of the following rules:

p_1_in_g₁(0_0) -> p_1_out_g₁(0_0)
p_1_in_g₁(s_1₁(X)) -> if_p_1_in_1_g₂(X, geq_2_in_ga₂(X, Y))
geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)
if_p_1_in_1_g₂(X, geq_2_out_ga₂(X, Y)) -> if_p_1_in_2_g₃(X, Y, p_1_in_g₁(Y))
if_p_1_in_2_g₃(X, Y, p_1_out_g₁(Y)) -> p_1_out_g₁(s_1₁(X))

The argument filtering Pi contains the following mapping:
p_1_in_g₁(x1) = p_1_in_g₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
p_1_out_g₁(x1) = p_1_out_g
if_p_1_in_1_g₂(x1, x2) = if_p_1_in_1_g₁(x2)
geq_2_in_ga₂(x1, x2) = geq_2_in_ga₁(x1)
geq_2_out_ga₂(x1, x2) = geq_2_out_ga₁(x2)
if_geq_2_in_1_ga₃(x1, x2, x3) = if_geq_2_in_1_ga₁(x3)
if_p_1_in_2_g₃(x1, x2, x3) = if_p_1_in_2_g₁(x3)
IF_GEQ_2_IN_1_GA₃(x1, x2, x3) = IF_GEQ_2_IN_1_GA₁(x3)
GEQ_2_IN_GA₂(x1, x2) = GEQ_2_IN_GA₁(x1)
IF_P_1_IN_2_G₃(x1, x2, x3) = IF_P_1_IN_2_G₁(x3)
IF_P_1_IN_1_G₂(x1, x2) = IF_P_1_IN_1_G₁(x2)
P_1_IN_G₁(x1) = P_1_IN_G₁(x1)

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:

P_1_IN_G₁(s_1₁(X)) -> IF_P_1_IN_1_G₂(X, geq_2_in_ga₂(X, Y))
P_1_IN_G₁(s_1₁(X)) -> GEQ_2_IN_GA₂(X, Y)
GEQ_2_IN_GA₂(s_1₁(X), Y) -> IF_GEQ_2_IN_1_GA₃(X, Y, geq_2_in_ga₂(X, Y))
GEQ_2_IN_GA₂(s_1₁(X), Y) -> GEQ_2_IN_GA₂(X, Y)
IF_P_1_IN_1_G₂(X, geq_2_out_ga₂(X, Y)) -> IF_P_1_IN_2_G₃(X, Y, p_1_in_g₁(Y))
IF_P_1_IN_1_G₂(X, geq_2_out_ga₂(X, Y)) -> P_1_IN_G₁(Y)

The TRS R consists of the following rules:

p_1_in_g₁(0_0) -> p_1_out_g₁(0_0)
p_1_in_g₁(s_1₁(X)) -> if_p_1_in_1_g₂(X, geq_2_in_ga₂(X, Y))
geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)
if_p_1_in_1_g₂(X, geq_2_out_ga₂(X, Y)) -> if_p_1_in_2_g₃(X, Y, p_1_in_g₁(Y))
if_p_1_in_2_g₃(X, Y, p_1_out_g₁(Y)) -> p_1_out_g₁(s_1₁(X))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

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

The TRS R consists of the following rules:

p_1_in_g₁(0_0) -> p_1_out_g₁(0_0)
p_1_in_g₁(s_1₁(X)) -> if_p_1_in_1_g₂(X, geq_2_in_ga₂(X, Y))
geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)
if_p_1_in_1_g₂(X, geq_2_out_ga₂(X, Y)) -> if_p_1_in_2_g₃(X, Y, p_1_in_g₁(Y))
if_p_1_in_2_g₃(X, Y, p_1_out_g₁(Y)) -> p_1_out_g₁(s_1₁(X))

The argument filtering Pi contains the following mapping:
p_1_in_g₁(x1) = p_1_in_g₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
p_1_out_g₁(x1) = p_1_out_g
if_p_1_in_1_g₂(x1, x2) = if_p_1_in_1_g₁(x2)
geq_2_in_ga₂(x1, x2) = geq_2_in_ga₁(x1)
geq_2_out_ga₂(x1, x2) = geq_2_out_ga₁(x2)
if_geq_2_in_1_ga₃(x1, x2, x3) = if_geq_2_in_1_ga₁(x3)
if_p_1_in_2_g₃(x1, x2, x3) = if_p_1_in_2_g₁(x3)
GEQ_2_IN_GA₂(x1, x2) = GEQ_2_IN_GA₁(x1)

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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

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

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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

GEQ_2_IN_GA₁(s_1₁(X)) -> GEQ_2_IN_GA₁(X)

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

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

IF_P_1_IN_1_G₂(X, geq_2_out_ga₂(X, Y)) -> P_1_IN_G₁(Y)
P_1_IN_G₁(s_1₁(X)) -> IF_P_1_IN_1_G₂(X, geq_2_in_ga₂(X, Y))

The TRS R consists of the following rules:

p_1_in_g₁(0_0) -> p_1_out_g₁(0_0)
p_1_in_g₁(s_1₁(X)) -> if_p_1_in_1_g₂(X, geq_2_in_ga₂(X, Y))
geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)
if_p_1_in_1_g₂(X, geq_2_out_ga₂(X, Y)) -> if_p_1_in_2_g₃(X, Y, p_1_in_g₁(Y))
if_p_1_in_2_g₃(X, Y, p_1_out_g₁(Y)) -> p_1_out_g₁(s_1₁(X))

The argument filtering Pi contains the following mapping:
p_1_in_g₁(x1) = p_1_in_g₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
p_1_out_g₁(x1) = p_1_out_g
if_p_1_in_1_g₂(x1, x2) = if_p_1_in_1_g₁(x2)
geq_2_in_ga₂(x1, x2) = geq_2_in_ga₁(x1)
geq_2_out_ga₂(x1, x2) = geq_2_out_ga₁(x2)
if_geq_2_in_1_ga₃(x1, x2, x3) = if_geq_2_in_1_ga₁(x3)
if_p_1_in_2_g₃(x1, x2, x3) = if_p_1_in_2_g₁(x3)
IF_P_1_IN_1_G₂(x1, x2) = IF_P_1_IN_1_G₁(x2)
P_1_IN_G₁(x1) = P_1_IN_G₁(x1)

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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

IF_P_1_IN_1_G₂(X, geq_2_out_ga₂(X, Y)) -> P_1_IN_G₁(Y)
P_1_IN_G₁(s_1₁(X)) -> IF_P_1_IN_1_G₂(X, geq_2_in_ga₂(X, Y))

The TRS R consists of the following rules:

geq_2_in_ga₂(X, X) -> geq_2_out_ga₂(X, X)
geq_2_in_ga₂(s_1₁(X), Y) -> if_geq_2_in_1_ga₃(X, Y, geq_2_in_ga₂(X, Y))
if_geq_2_in_1_ga₃(X, Y, geq_2_out_ga₂(X, Y)) -> geq_2_out_ga₂(s_1₁(X), Y)

The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1₁(x1)
geq_2_in_ga₂(x1, x2) = geq_2_in_ga₁(x1)
geq_2_out_ga₂(x1, x2) = geq_2_out_ga₁(x2)
if_geq_2_in_1_ga₃(x1, x2, x3) = if_geq_2_in_1_ga₁(x3)
IF_P_1_IN_1_G₂(x1, x2) = IF_P_1_IN_1_G₁(x2)
P_1_IN_G₁(x1) = P_1_IN_G₁(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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

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

IF_P_1_IN_1_G₁(geq_2_out_ga₁(Y)) -> P_1_IN_G₁(Y)
P_1_IN_G₁(s_1₁(X)) -> IF_P_1_IN_1_G₁(geq_2_in_ga₁(X))

The TRS R consists of the following rules:

geq_2_in_ga₁(X) -> geq_2_out_ga₁(X)
geq_2_in_ga₁(s_1₁(X)) -> if_geq_2_in_1_ga₁(geq_2_in_ga₁(X))
if_geq_2_in_1_ga₁(geq_2_out_ga₁(Y)) -> geq_2_out_ga₁(Y)

The set Q consists of the following terms:

geq_2_in_ga₁(x0)
if_geq_2_in_1_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {P_1_IN_G₁, IF_P_1_IN_1_G₁}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

IF_P_1_IN_1_G₁(geq_2_out_ga₁(Y)) -> P_1_IN_G₁(Y)

Strictly oriented rules of the TRS R:

geq_2_in_ga₁(X) -> geq_2_out_ga₁(X)
geq_2_in_ga₁(s_1₁(X)) -> if_geq_2_in_1_ga₁(geq_2_in_ga₁(X))

Used ordering: POLO with Polynomial interpretation:

POL(if_geq_2_in_1_ga₁(x₁)) = x₁
POL(IF_P_1_IN_1_G₁(x₁)) = x₁
POL(geq_2_out_ga₁(x₁)) = 1 + x₁
POL(s_1₁(x₁)) = 2 + x₁
POL(geq_2_in_ga₁(x₁)) = 2 + x₁
POL(P_1_IN_G₁(x₁)) = x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

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

P_1_IN_G₁(s_1₁(X)) -> IF_P_1_IN_1_G₁(geq_2_in_ga₁(X))

The TRS R consists of the following rules:

if_geq_2_in_1_ga₁(geq_2_out_ga₁(Y)) -> geq_2_out_ga₁(Y)

The set Q consists of the following terms:

geq_2_in_ga₁(x0)
if_geq_2_in_1_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_P_1_IN_1_G₁, P_1_IN_G₁}.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.