Left Termination proof of /tmp/tmpBLhynp/incomplete2.pl

Left Termination of the query pattern f(b) w.r.t. the given Prolog program could not be shown:

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

f₁(X) :- g₁(s₁³(X)).
f₁(s₁(X)) :- f₁(X).
g₁(s₁⁴(X)) :- f₁(X).

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

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

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:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

F_1_IN_G₁(X) -> IF_F_1_IN_1_G₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> IF_G_1_IN_1_G₂(X, f_1_in_g₁(X))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(s_1₁(X)) -> IF_F_1_IN_2_G₂(X, f_1_in_g₁(X))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

The argument filtering Pi contains the following mapping:
f_1_in_g₁(x1) = f_1_in_g₁(x1)
s_1₁(x1) = s_1₁(x1)
if_f_1_in_1_g₂(x1, x2) = if_f_1_in_1_g₁(x2)
g_1_in_g₁(x1) = g_1_in_g₁(x1)
if_g_1_in_1_g₂(x1, x2) = if_g_1_in_1_g₁(x2)
if_f_1_in_2_g₂(x1, x2) = if_f_1_in_2_g₁(x2)
f_1_out_g₁(x1) = f_1_out_g
g_1_out_g₁(x1) = g_1_out_g
F_1_IN_G₁(x1) = F_1_IN_G₁(x1)
IF_G_1_IN_1_G₂(x1, x2) = IF_G_1_IN_1_G₁(x2)
G_1_IN_G₁(x1) = G_1_IN_G₁(x1)
IF_F_1_IN_1_G₂(x1, x2) = IF_F_1_IN_1_G₁(x2)
IF_F_1_IN_2_G₂(x1, x2) = IF_F_1_IN_2_G₁(x2)

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:

F_1_IN_G₁(X) -> IF_F_1_IN_1_G₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> IF_G_1_IN_1_G₂(X, f_1_in_g₁(X))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(s_1₁(X)) -> IF_F_1_IN_2_G₂(X, f_1_in_g₁(X))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

The argument filtering Pi contains the following mapping:
f_1_in_g₁(x1) = f_1_in_g₁(x1)
s_1₁(x1) = s_1₁(x1)
if_f_1_in_1_g₂(x1, x2) = if_f_1_in_1_g₁(x2)
g_1_in_g₁(x1) = g_1_in_g₁(x1)
if_g_1_in_1_g₂(x1, x2) = if_g_1_in_1_g₁(x2)
if_f_1_in_2_g₂(x1, x2) = if_f_1_in_2_g₁(x2)
f_1_out_g₁(x1) = f_1_out_g
g_1_out_g₁(x1) = g_1_out_g
F_1_IN_G₁(x1) = F_1_IN_G₁(x1)
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

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

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

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

  ↳ PrologToPiTRSProof

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

G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

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₁, G_1_IN_G₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
f₁: (b)
g₁: (b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

Pi is empty.

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:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

Pi is empty.

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

F_1_IN_G₁(X) -> IF_F_1_IN_1_G₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> IF_G_1_IN_1_G₂(X, f_1_in_g₁(X))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(s_1₁(X)) -> IF_F_1_IN_2_G₂(X, f_1_in_g₁(X))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

Pi is empty.
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:

F_1_IN_G₁(X) -> IF_F_1_IN_1_G₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> IF_G_1_IN_1_G₂(X, f_1_in_g₁(X))
G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(s_1₁(X)) -> IF_F_1_IN_2_G₂(X, f_1_in_g₁(X))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

Pi is empty.
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 3 less nodes.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

The TRS R consists of the following rules:

f_1_in_g₁(X) -> if_f_1_in_1_g₂(X, g_1_in_g₁(s_1₁(s_1₁(s_1₁(X)))))
g_1_in_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> if_g_1_in_1_g₂(X, f_1_in_g₁(X))
f_1_in_g₁(s_1₁(X)) -> if_f_1_in_2_g₂(X, f_1_in_g₁(X))
if_f_1_in_2_g₂(X, f_1_out_g₁(X)) -> f_1_out_g₁(s_1₁(X))
if_g_1_in_1_g₂(X, f_1_out_g₁(X)) -> g_1_out_g₁(s_1₁(s_1₁(s_1₁(s_1₁(X)))))
if_f_1_in_1_g₂(X, g_1_out_g₁(s_1₁(s_1₁(s_1₁(X))))) -> f_1_out_g₁(X)

Pi is empty.
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

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

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

G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

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

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

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

G_1_IN_G₁(s_1₁(s_1₁(s_1₁(s_1₁(X))))) -> F_1_IN_G₁(X)
F_1_IN_G₁(X) -> G_1_IN_G₁(s_1₁(s_1₁(s_1₁(X))))
F_1_IN_G₁(s_1₁(X)) -> F_1_IN_G₁(X)

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₁, G_1_IN_G₁}.