Left Termination proof of /tmp/tmpT99gBk/ag01.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

f₁(c₂(s₁(X), Y)) :- f₁(c₂(X, s₁(Y))).
g₁(c₂(X, s₁(Y))) :- g₁(c₂(s₁(X), Y)).
h₁(X) :- f₁(X), g₁(X).

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

h_1_in_g₁(X) -> if_h_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(c_2₂(s_1₁(X), Y)) -> if_f_1_in_1_g₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
if_f_1_in_1_g₃(X, Y, f_1_out_g₁(c_2₂(X, s_1₁(Y)))) -> f_1_out_g₁(c_2₂(s_1₁(X), Y))
if_h_1_in_1_g₂(X, f_1_out_g₁(X)) -> if_h_1_in_2_g₂(X, g_1_in_g₁(X))
g_1_in_g₁(c_2₂(X, s_1₁(Y))) -> if_g_1_in_1_g₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
if_g_1_in_1_g₃(X, Y, g_1_out_g₁(c_2₂(s_1₁(X), Y))) -> g_1_out_g₁(c_2₂(X, s_1₁(Y)))
if_h_1_in_2_g₂(X, g_1_out_g₁(X)) -> h_1_out_g₁(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:

h_1_in_g₁(X) -> if_h_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(c_2₂(s_1₁(X), Y)) -> if_f_1_in_1_g₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
if_f_1_in_1_g₃(X, Y, f_1_out_g₁(c_2₂(X, s_1₁(Y)))) -> f_1_out_g₁(c_2₂(s_1₁(X), Y))
if_h_1_in_1_g₂(X, f_1_out_g₁(X)) -> if_h_1_in_2_g₂(X, g_1_in_g₁(X))
g_1_in_g₁(c_2₂(X, s_1₁(Y))) -> if_g_1_in_1_g₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
if_g_1_in_1_g₃(X, Y, g_1_out_g₁(c_2₂(s_1₁(X), Y))) -> g_1_out_g₁(c_2₂(X, s_1₁(Y)))
if_h_1_in_2_g₂(X, g_1_out_g₁(X)) -> h_1_out_g₁(X)

H_1_IN_G₁(X) -> IF_H_1_IN_1_G₂(X, f_1_in_g₁(X))
H_1_IN_G₁(X) -> F_1_IN_G₁(X)
F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> IF_F_1_IN_1_G₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> F_1_IN_G₁(c_2₂(X, s_1₁(Y)))
IF_H_1_IN_1_G₂(X, f_1_out_g₁(X)) -> IF_H_1_IN_2_G₂(X, g_1_in_g₁(X))
IF_H_1_IN_1_G₂(X, f_1_out_g₁(X)) -> G_1_IN_G₁(X)
G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> IF_G_1_IN_1_G₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> G_1_IN_G₁(c_2₂(s_1₁(X), Y))

The TRS R consists of the following rules:

h_1_in_g₁(X) -> if_h_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(c_2₂(s_1₁(X), Y)) -> if_f_1_in_1_g₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
if_f_1_in_1_g₃(X, Y, f_1_out_g₁(c_2₂(X, s_1₁(Y)))) -> f_1_out_g₁(c_2₂(s_1₁(X), Y))
if_h_1_in_1_g₂(X, f_1_out_g₁(X)) -> if_h_1_in_2_g₂(X, g_1_in_g₁(X))
g_1_in_g₁(c_2₂(X, s_1₁(Y))) -> if_g_1_in_1_g₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
if_g_1_in_1_g₃(X, Y, g_1_out_g₁(c_2₂(s_1₁(X), Y))) -> g_1_out_g₁(c_2₂(X, s_1₁(Y)))
if_h_1_in_2_g₂(X, g_1_out_g₁(X)) -> h_1_out_g₁(X)

The argument filtering Pi contains the following mapping:
h_1_in_g₁(x1) = h_1_in_g₁(x1)
c_2₂(x1, x2) = c_2₂(x1, x2)
s_1₁(x1) = s_1₁(x1)
if_h_1_in_1_g₂(x1, x2) = if_h_1_in_1_g₂(x1, x2)
f_1_in_g₁(x1) = f_1_in_g₁(x1)
if_f_1_in_1_g₃(x1, x2, x3) = if_f_1_in_1_g₁(x3)
f_1_out_g₁(x1) = f_1_out_g
if_h_1_in_2_g₂(x1, x2) = if_h_1_in_2_g₁(x2)
g_1_in_g₁(x1) = g_1_in_g₁(x1)
if_g_1_in_1_g₃(x1, x2, x3) = if_g_1_in_1_g₁(x3)
g_1_out_g₁(x1) = g_1_out_g
h_1_out_g₁(x1) = h_1_out_g
F_1_IN_G₁(x1) = F_1_IN_G₁(x1)
IF_H_1_IN_1_G₂(x1, x2) = IF_H_1_IN_1_G₂(x1, x2)
IF_G_1_IN_1_G₃(x1, x2, x3) = IF_G_1_IN_1_G₁(x3)
IF_H_1_IN_2_G₂(x1, x2) = IF_H_1_IN_2_G₁(x2)
G_1_IN_G₁(x1) = G_1_IN_G₁(x1)
IF_F_1_IN_1_G₃(x1, x2, x3) = IF_F_1_IN_1_G₁(x3)
H_1_IN_G₁(x1) = H_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:

H_1_IN_G₁(X) -> IF_H_1_IN_1_G₂(X, f_1_in_g₁(X))
H_1_IN_G₁(X) -> F_1_IN_G₁(X)
F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> IF_F_1_IN_1_G₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> F_1_IN_G₁(c_2₂(X, s_1₁(Y)))
IF_H_1_IN_1_G₂(X, f_1_out_g₁(X)) -> IF_H_1_IN_2_G₂(X, g_1_in_g₁(X))
IF_H_1_IN_1_G₂(X, f_1_out_g₁(X)) -> G_1_IN_G₁(X)
G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> IF_G_1_IN_1_G₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> G_1_IN_G₁(c_2₂(s_1₁(X), Y))

The TRS R consists of the following rules:

h_1_in_g₁(X) -> if_h_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(c_2₂(s_1₁(X), Y)) -> if_f_1_in_1_g₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
if_f_1_in_1_g₃(X, Y, f_1_out_g₁(c_2₂(X, s_1₁(Y)))) -> f_1_out_g₁(c_2₂(s_1₁(X), Y))
if_h_1_in_1_g₂(X, f_1_out_g₁(X)) -> if_h_1_in_2_g₂(X, g_1_in_g₁(X))
g_1_in_g₁(c_2₂(X, s_1₁(Y))) -> if_g_1_in_1_g₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
if_g_1_in_1_g₃(X, Y, g_1_out_g₁(c_2₂(s_1₁(X), Y))) -> g_1_out_g₁(c_2₂(X, s_1₁(Y)))
if_h_1_in_2_g₂(X, g_1_out_g₁(X)) -> h_1_out_g₁(X)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> G_1_IN_G₁(c_2₂(s_1₁(X), Y))

The TRS R consists of the following rules:

h_1_in_g₁(X) -> if_h_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(c_2₂(s_1₁(X), Y)) -> if_f_1_in_1_g₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
if_f_1_in_1_g₃(X, Y, f_1_out_g₁(c_2₂(X, s_1₁(Y)))) -> f_1_out_g₁(c_2₂(s_1₁(X), Y))
if_h_1_in_1_g₂(X, f_1_out_g₁(X)) -> if_h_1_in_2_g₂(X, g_1_in_g₁(X))
g_1_in_g₁(c_2₂(X, s_1₁(Y))) -> if_g_1_in_1_g₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
if_g_1_in_1_g₃(X, Y, g_1_out_g₁(c_2₂(s_1₁(X), Y))) -> g_1_out_g₁(c_2₂(X, s_1₁(Y)))
if_h_1_in_2_g₂(X, g_1_out_g₁(X)) -> h_1_out_g₁(X)

The argument filtering Pi contains the following mapping:
h_1_in_g₁(x1) = h_1_in_g₁(x1)
c_2₂(x1, x2) = c_2₂(x1, x2)
s_1₁(x1) = s_1₁(x1)
if_h_1_in_1_g₂(x1, x2) = if_h_1_in_1_g₂(x1, x2)
f_1_in_g₁(x1) = f_1_in_g₁(x1)
if_f_1_in_1_g₃(x1, x2, x3) = if_f_1_in_1_g₁(x3)
f_1_out_g₁(x1) = f_1_out_g
if_h_1_in_2_g₂(x1, x2) = if_h_1_in_2_g₁(x2)
g_1_in_g₁(x1) = g_1_in_g₁(x1)
if_g_1_in_1_g₃(x1, x2, x3) = if_g_1_in_1_g₁(x3)
g_1_out_g₁(x1) = g_1_out_g
h_1_out_g₁(x1) = h_1_out_g
G_1_IN_G₁(x1) = G_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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> G_1_IN_G₁(c_2₂(s_1₁(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

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

G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> G_1_IN_G₁(c_2₂(s_1₁(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 {G_1_IN_G₁}.
We used the following order and afs together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
s_1₁(x1) = s_1₁(x1)
c_2₂(x1, x2) = x2

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

G_1_IN_G₁(c_2₂(X, s_1₁(Y))) -> G_1_IN_G₁(c_2₂(s_1₁(X), Y)) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1

We oriented the following set of usable rules. none

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> F_1_IN_G₁(c_2₂(X, s_1₁(Y)))

The TRS R consists of the following rules:

h_1_in_g₁(X) -> if_h_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(c_2₂(s_1₁(X), Y)) -> if_f_1_in_1_g₃(X, Y, f_1_in_g₁(c_2₂(X, s_1₁(Y))))
if_f_1_in_1_g₃(X, Y, f_1_out_g₁(c_2₂(X, s_1₁(Y)))) -> f_1_out_g₁(c_2₂(s_1₁(X), Y))
if_h_1_in_1_g₂(X, f_1_out_g₁(X)) -> if_h_1_in_2_g₂(X, g_1_in_g₁(X))
g_1_in_g₁(c_2₂(X, s_1₁(Y))) -> if_g_1_in_1_g₃(X, Y, g_1_in_g₁(c_2₂(s_1₁(X), Y)))
if_g_1_in_1_g₃(X, Y, g_1_out_g₁(c_2₂(s_1₁(X), Y))) -> g_1_out_g₁(c_2₂(X, s_1₁(Y)))
if_h_1_in_2_g₂(X, g_1_out_g₁(X)) -> h_1_out_g₁(X)

The argument filtering Pi contains the following mapping:
h_1_in_g₁(x1) = h_1_in_g₁(x1)
c_2₂(x1, x2) = c_2₂(x1, x2)
s_1₁(x1) = s_1₁(x1)
if_h_1_in_1_g₂(x1, x2) = if_h_1_in_1_g₂(x1, x2)
f_1_in_g₁(x1) = f_1_in_g₁(x1)
if_f_1_in_1_g₃(x1, x2, x3) = if_f_1_in_1_g₁(x3)
f_1_out_g₁(x1) = f_1_out_g
if_h_1_in_2_g₂(x1, x2) = if_h_1_in_2_g₁(x2)
g_1_in_g₁(x1) = g_1_in_g₁(x1)
if_g_1_in_1_g₃(x1, x2, x3) = if_g_1_in_1_g₁(x3)
g_1_out_g₁(x1) = g_1_out_g
h_1_out_g₁(x1) = h_1_out_g
F_1_IN_G₁(x1) = F_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:

F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> F_1_IN_G₁(c_2₂(X, s_1₁(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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

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

F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> F_1_IN_G₁(c_2₂(X, s_1₁(Y)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {F_1_IN_G₁}.
We used the following order and afs together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
s_1₁(x1) = s_1₁(x1)
c_2₂(x1, x2) = x1

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

F_1_IN_G₁(c_2₂(s_1₁(X), Y)) -> F_1_IN_G₁(c_2₂(X, s_1₁(Y))) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1

We oriented the following set of usable rules. none