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



PROLOG
  ↳ PrologToPiTRSProof

p1(.2(X, {}0)).
p1(.2(s12 (X), .2(Y, Xs))) :- p1(.2(X, .2(Y, Xs))), p1(.2(s14 (Y), Xs)).
p1(.2(00, Xs)) :- p1(Xs).


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


p_1_in_g1(._22(X, []_0)) -> p_1_out_g1(._22(X, []_0))
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g2(Xs, p_1_in_g1(Xs))
if_p_1_in_3_g2(Xs, p_1_out_g1(Xs)) -> p_1_out_g1(._22(0_0, Xs))
if_p_1_in_1_g4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> if_p_1_in_2_g4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g4(X, Y, Xs, p_1_out_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))) -> p_1_out_g1(._22(s_11(s_11(X)), ._22(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g1(x1)  =  p_1_in_g1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
s_11(x1)  =  s_11(x1)
0_0  =  0_0
p_1_out_g1(x1)  =  p_1_out_g
if_p_1_in_1_g4(x1, x2, x3, x4)  =  if_p_1_in_1_g3(x2, x3, x4)
if_p_1_in_3_g2(x1, x2)  =  if_p_1_in_3_g1(x2)
if_p_1_in_2_g4(x1, x2, x3, x4)  =  if_p_1_in_2_g1(x4)

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_g1(._22(X, []_0)) -> p_1_out_g1(._22(X, []_0))
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g2(Xs, p_1_in_g1(Xs))
if_p_1_in_3_g2(Xs, p_1_out_g1(Xs)) -> p_1_out_g1(._22(0_0, Xs))
if_p_1_in_1_g4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> if_p_1_in_2_g4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g4(X, Y, Xs, p_1_out_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))) -> p_1_out_g1(._22(s_11(s_11(X)), ._22(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g1(x1)  =  p_1_in_g1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
s_11(x1)  =  s_11(x1)
0_0  =  0_0
p_1_out_g1(x1)  =  p_1_out_g
if_p_1_in_1_g4(x1, x2, x3, x4)  =  if_p_1_in_1_g3(x2, x3, x4)
if_p_1_in_3_g2(x1, x2)  =  if_p_1_in_3_g1(x2)
if_p_1_in_2_g4(x1, x2, x3, x4)  =  if_p_1_in_2_g1(x4)


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

P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> IF_P_1_IN_1_G4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))
P_1_IN_G1(._22(0_0, Xs)) -> IF_P_1_IN_3_G2(Xs, p_1_in_g1(Xs))
P_1_IN_G1(._22(0_0, Xs)) -> P_1_IN_G1(Xs)
IF_P_1_IN_1_G4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> IF_P_1_IN_2_G4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
IF_P_1_IN_1_G4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> P_1_IN_G1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))

The TRS R consists of the following rules:

p_1_in_g1(._22(X, []_0)) -> p_1_out_g1(._22(X, []_0))
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g2(Xs, p_1_in_g1(Xs))
if_p_1_in_3_g2(Xs, p_1_out_g1(Xs)) -> p_1_out_g1(._22(0_0, Xs))
if_p_1_in_1_g4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> if_p_1_in_2_g4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g4(X, Y, Xs, p_1_out_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))) -> p_1_out_g1(._22(s_11(s_11(X)), ._22(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g1(x1)  =  p_1_in_g1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
s_11(x1)  =  s_11(x1)
0_0  =  0_0
p_1_out_g1(x1)  =  p_1_out_g
if_p_1_in_1_g4(x1, x2, x3, x4)  =  if_p_1_in_1_g3(x2, x3, x4)
if_p_1_in_3_g2(x1, x2)  =  if_p_1_in_3_g1(x2)
if_p_1_in_2_g4(x1, x2, x3, x4)  =  if_p_1_in_2_g1(x4)
IF_P_1_IN_2_G4(x1, x2, x3, x4)  =  IF_P_1_IN_2_G1(x4)
IF_P_1_IN_3_G2(x1, x2)  =  IF_P_1_IN_3_G1(x2)
IF_P_1_IN_1_G4(x1, x2, x3, x4)  =  IF_P_1_IN_1_G3(x2, x3, x4)
P_1_IN_G1(x1)  =  P_1_IN_G1(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_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> IF_P_1_IN_1_G4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))
P_1_IN_G1(._22(0_0, Xs)) -> IF_P_1_IN_3_G2(Xs, p_1_in_g1(Xs))
P_1_IN_G1(._22(0_0, Xs)) -> P_1_IN_G1(Xs)
IF_P_1_IN_1_G4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> IF_P_1_IN_2_G4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
IF_P_1_IN_1_G4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> P_1_IN_G1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))

The TRS R consists of the following rules:

p_1_in_g1(._22(X, []_0)) -> p_1_out_g1(._22(X, []_0))
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g2(Xs, p_1_in_g1(Xs))
if_p_1_in_3_g2(Xs, p_1_out_g1(Xs)) -> p_1_out_g1(._22(0_0, Xs))
if_p_1_in_1_g4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> if_p_1_in_2_g4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g4(X, Y, Xs, p_1_out_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))) -> p_1_out_g1(._22(s_11(s_11(X)), ._22(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g1(x1)  =  p_1_in_g1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
s_11(x1)  =  s_11(x1)
0_0  =  0_0
p_1_out_g1(x1)  =  p_1_out_g
if_p_1_in_1_g4(x1, x2, x3, x4)  =  if_p_1_in_1_g3(x2, x3, x4)
if_p_1_in_3_g2(x1, x2)  =  if_p_1_in_3_g1(x2)
if_p_1_in_2_g4(x1, x2, x3, x4)  =  if_p_1_in_2_g1(x4)
IF_P_1_IN_2_G4(x1, x2, x3, x4)  =  IF_P_1_IN_2_G1(x4)
IF_P_1_IN_3_G2(x1, x2)  =  IF_P_1_IN_3_G1(x2)
IF_P_1_IN_1_G4(x1, x2, x3, x4)  =  IF_P_1_IN_1_G3(x2, x3, x4)
P_1_IN_G1(x1)  =  P_1_IN_G1(x1)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
PiDP
              ↳ PiDPToQDPProof

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

P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> IF_P_1_IN_1_G4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
IF_P_1_IN_1_G4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> P_1_IN_G1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))
P_1_IN_G1(._22(0_0, Xs)) -> P_1_IN_G1(Xs)
P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g1(._22(X, []_0)) -> p_1_out_g1(._22(X, []_0))
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g4(X, Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g2(Xs, p_1_in_g1(Xs))
if_p_1_in_3_g2(Xs, p_1_out_g1(Xs)) -> p_1_out_g1(._22(0_0, Xs))
if_p_1_in_1_g4(X, Y, Xs, p_1_out_g1(._22(X, ._22(Y, Xs)))) -> if_p_1_in_2_g4(X, Y, Xs, p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g4(X, Y, Xs, p_1_out_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))) -> p_1_out_g1(._22(s_11(s_11(X)), ._22(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g1(x1)  =  p_1_in_g1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
s_11(x1)  =  s_11(x1)
0_0  =  0_0
p_1_out_g1(x1)  =  p_1_out_g
if_p_1_in_1_g4(x1, x2, x3, x4)  =  if_p_1_in_1_g3(x2, x3, x4)
if_p_1_in_3_g2(x1, x2)  =  if_p_1_in_3_g1(x2)
if_p_1_in_2_g4(x1, x2, x3, x4)  =  if_p_1_in_2_g1(x4)
IF_P_1_IN_1_G4(x1, x2, x3, x4)  =  IF_P_1_IN_1_G3(x2, x3, x4)
P_1_IN_G1(x1)  =  P_1_IN_G1(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
            ↳ PiDP
              ↳ PiDPToQDPProof
QDP
                  ↳ QDPPoloProof

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

P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> IF_P_1_IN_1_G3(Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
IF_P_1_IN_1_G3(Y, Xs, p_1_out_g) -> P_1_IN_G1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))
P_1_IN_G1(._22(0_0, Xs)) -> P_1_IN_G1(Xs)
P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g1(._22(X, []_0)) -> p_1_out_g
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g3(Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g1(p_1_in_g1(Xs))
if_p_1_in_3_g1(p_1_out_g) -> p_1_out_g
if_p_1_in_1_g3(Y, Xs, p_1_out_g) -> if_p_1_in_2_g1(p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g1(p_1_out_g) -> p_1_out_g

The set Q consists of the following terms:

p_1_in_g1(x0)
if_p_1_in_3_g1(x0)
if_p_1_in_1_g3(x0, x1, x2)
if_p_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_P_1_IN_1_G3, P_1_IN_G1}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> IF_P_1_IN_1_G3(Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
P_1_IN_G1(._22(0_0, Xs)) -> P_1_IN_G1(Xs)
The remaining Dependency Pairs were at least non-strictly be oriented.

IF_P_1_IN_1_G3(Y, Xs, p_1_out_g) -> P_1_IN_G1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))
P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))
With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:


POL(0_0) = 0   
POL(._22(x1, x2)) = 1 + x2   
POL(IF_P_1_IN_1_G3(x1, x2, x3)) = 1 + x2   
POL(if_p_1_in_2_g1(x1)) = 0   
POL(s_11(x1)) = 0   
POL(if_p_1_in_1_g3(x1, x2, x3)) = 0   
POL(if_p_1_in_3_g1(x1)) = 0   
POL([]_0) = 0   
POL(p_1_in_g1(x1)) = 0   
POL(p_1_out_g) = 0   
POL(P_1_IN_G1(x1)) = x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
QDP
                      ↳ DependencyGraphProof

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

IF_P_1_IN_1_G3(Y, Xs, p_1_out_g) -> P_1_IN_G1(._22(s_11(s_11(s_11(s_11(Y)))), Xs))
P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g1(._22(X, []_0)) -> p_1_out_g
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g3(Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g1(p_1_in_g1(Xs))
if_p_1_in_3_g1(p_1_out_g) -> p_1_out_g
if_p_1_in_1_g3(Y, Xs, p_1_out_g) -> if_p_1_in_2_g1(p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g1(p_1_out_g) -> p_1_out_g

The set Q consists of the following terms:

p_1_in_g1(x0)
if_p_1_in_3_g1(x0)
if_p_1_in_1_g3(x0, x1, x2)
if_p_1_in_2_g1(x0)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
                    ↳ QDP
                      ↳ DependencyGraphProof
QDP
                          ↳ UsableRulesProof

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

P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g1(._22(X, []_0)) -> p_1_out_g
p_1_in_g1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> if_p_1_in_1_g3(Y, Xs, p_1_in_g1(._22(X, ._22(Y, Xs))))
p_1_in_g1(._22(0_0, Xs)) -> if_p_1_in_3_g1(p_1_in_g1(Xs))
if_p_1_in_3_g1(p_1_out_g) -> p_1_out_g
if_p_1_in_1_g3(Y, Xs, p_1_out_g) -> if_p_1_in_2_g1(p_1_in_g1(._22(s_11(s_11(s_11(s_11(Y)))), Xs)))
if_p_1_in_2_g1(p_1_out_g) -> p_1_out_g

The set Q consists of the following terms:

p_1_in_g1(x0)
if_p_1_in_3_g1(x0)
if_p_1_in_1_g3(x0, x1, x2)
if_p_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {P_1_IN_G1}.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QDPSizeChangeProof

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

P_1_IN_G1(._22(s_11(s_11(X)), ._22(Y, Xs))) -> P_1_IN_G1(._22(X, ._22(Y, Xs)))

R is empty.
The set Q consists of the following terms:

p_1_in_g1(x0)
if_p_1_in_3_g1(x0)
if_p_1_in_1_g3(x0, x1, x2)
if_p_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {P_1_IN_G1}.
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_11(x1)  =  s_11(x1)
._22(x1, x2)  =  x1

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

We oriented the following set of usable rules. none