Left Termination proof of /tmp/tmp4VvKm0/pl3.1.1.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

a₀ :- b₀.
a₀ :- e₀.
b₀ :- c₀.
c₀ :- d₀.
d₀ :- b₀.
e₀ :- f₀.
f₀ :- g₀.
g₀ :- e₀.

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

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

Pi is empty.

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:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

Pi is empty.

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

A_0_IN_ -> IF_A_0_IN_1_₁(b_0_in_)
A_0_IN_ -> B_0_IN_
B_0_IN_ -> IF_B_0_IN_1_₁(c_0_in_)
B_0_IN_ -> C_0_IN_
C_0_IN_ -> IF_C_0_IN_1_₁(d_0_in_)
C_0_IN_ -> D_0_IN_
D_0_IN_ -> IF_D_0_IN_1_₁(b_0_in_)
D_0_IN_ -> B_0_IN_
A_0_IN_ -> IF_A_0_IN_2_₁(e_0_in_)
A_0_IN_ -> E_0_IN_
E_0_IN_ -> IF_E_0_IN_1_₁(f_0_in_)
E_0_IN_ -> F_0_IN_
F_0_IN_ -> IF_F_0_IN_1_₁(g_0_in_)
F_0_IN_ -> G_0_IN_
G_0_IN_ -> IF_G_0_IN_1_₁(e_0_in_)
G_0_IN_ -> E_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

A_0_IN_ -> IF_A_0_IN_1_₁(b_0_in_)
A_0_IN_ -> B_0_IN_
B_0_IN_ -> IF_B_0_IN_1_₁(c_0_in_)
B_0_IN_ -> C_0_IN_
C_0_IN_ -> IF_C_0_IN_1_₁(d_0_in_)
C_0_IN_ -> D_0_IN_
D_0_IN_ -> IF_D_0_IN_1_₁(b_0_in_)
D_0_IN_ -> B_0_IN_
A_0_IN_ -> IF_A_0_IN_2_₁(e_0_in_)
A_0_IN_ -> E_0_IN_
E_0_IN_ -> IF_E_0_IN_1_₁(f_0_in_)
E_0_IN_ -> F_0_IN_
F_0_IN_ -> IF_F_0_IN_1_₁(g_0_in_)
F_0_IN_ -> G_0_IN_
G_0_IN_ -> IF_G_0_IN_1_₁(e_0_in_)
G_0_IN_ -> E_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

F_0_IN_ -> G_0_IN_
E_0_IN_ -> F_0_IN_
G_0_IN_ -> E_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

F_0_IN_ -> G_0_IN_
E_0_IN_ -> F_0_IN_
G_0_IN_ -> E_0_IN_

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

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

F_0_IN_ -> G_0_IN_
E_0_IN_ -> F_0_IN_
G_0_IN_ -> E_0_IN_

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {G_0_IN_, F_0_IN_, E_0_IN_}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

B_0_IN_ -> C_0_IN_
D_0_IN_ -> B_0_IN_
C_0_IN_ -> D_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

B_0_IN_ -> C_0_IN_
D_0_IN_ -> B_0_IN_
C_0_IN_ -> D_0_IN_

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

  ↳ PrologToPiTRSProof

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

B_0_IN_ -> C_0_IN_
D_0_IN_ -> B_0_IN_
C_0_IN_ -> D_0_IN_

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {C_0_IN_, B_0_IN_, D_0_IN_}.
With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

Pi is empty.

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

A_0_IN_ -> IF_A_0_IN_1_₁(b_0_in_)
A_0_IN_ -> B_0_IN_
B_0_IN_ -> IF_B_0_IN_1_₁(c_0_in_)
B_0_IN_ -> C_0_IN_
C_0_IN_ -> IF_C_0_IN_1_₁(d_0_in_)
C_0_IN_ -> D_0_IN_
D_0_IN_ -> IF_D_0_IN_1_₁(b_0_in_)
D_0_IN_ -> B_0_IN_
A_0_IN_ -> IF_A_0_IN_2_₁(e_0_in_)
A_0_IN_ -> E_0_IN_
E_0_IN_ -> IF_E_0_IN_1_₁(f_0_in_)
E_0_IN_ -> F_0_IN_
F_0_IN_ -> IF_F_0_IN_1_₁(g_0_in_)
F_0_IN_ -> G_0_IN_
G_0_IN_ -> IF_G_0_IN_1_₁(e_0_in_)
G_0_IN_ -> E_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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:

A_0_IN_ -> IF_A_0_IN_1_₁(b_0_in_)
A_0_IN_ -> B_0_IN_
B_0_IN_ -> IF_B_0_IN_1_₁(c_0_in_)
B_0_IN_ -> C_0_IN_
C_0_IN_ -> IF_C_0_IN_1_₁(d_0_in_)
C_0_IN_ -> D_0_IN_
D_0_IN_ -> IF_D_0_IN_1_₁(b_0_in_)
D_0_IN_ -> B_0_IN_
A_0_IN_ -> IF_A_0_IN_2_₁(e_0_in_)
A_0_IN_ -> E_0_IN_
E_0_IN_ -> IF_E_0_IN_1_₁(f_0_in_)
E_0_IN_ -> F_0_IN_
F_0_IN_ -> IF_F_0_IN_1_₁(g_0_in_)
F_0_IN_ -> G_0_IN_
G_0_IN_ -> IF_G_0_IN_1_₁(e_0_in_)
G_0_IN_ -> E_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

F_0_IN_ -> G_0_IN_
E_0_IN_ -> F_0_IN_
G_0_IN_ -> E_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

              ↳ PiDP

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

F_0_IN_ -> G_0_IN_
E_0_IN_ -> F_0_IN_
G_0_IN_ -> E_0_IN_

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

B_0_IN_ -> C_0_IN_
D_0_IN_ -> B_0_IN_
C_0_IN_ -> D_0_IN_

The TRS R consists of the following rules:

a_0_in_ -> if_a_0_in_1_₁(b_0_in_)
b_0_in_ -> if_b_0_in_1_₁(c_0_in_)
c_0_in_ -> if_c_0_in_1_₁(d_0_in_)
d_0_in_ -> if_d_0_in_1_₁(b_0_in_)
if_d_0_in_1_₁(b_0_out_) -> d_0_out_
if_c_0_in_1_₁(d_0_out_) -> c_0_out_
if_b_0_in_1_₁(c_0_out_) -> b_0_out_
if_a_0_in_1_₁(b_0_out_) -> a_0_out_
a_0_in_ -> if_a_0_in_2_₁(e_0_in_)
e_0_in_ -> if_e_0_in_1_₁(f_0_in_)
f_0_in_ -> if_f_0_in_1_₁(g_0_in_)
g_0_in_ -> if_g_0_in_1_₁(e_0_in_)
if_g_0_in_1_₁(e_0_out_) -> g_0_out_
if_f_0_in_1_₁(g_0_out_) -> f_0_out_
if_e_0_in_1_₁(f_0_out_) -> e_0_out_
if_a_0_in_2_₁(e_0_out_) -> a_0_out_

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

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

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

B_0_IN_ -> C_0_IN_
D_0_IN_ -> B_0_IN_
C_0_IN_ -> D_0_IN_

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains