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



↳ PROLOG
  ↳ PrologToPiTRSProof

countstack2(empty0, 00).
countstack2(push2(nil0, T), X) :- countstack2(T, X).
countstack2(push2(cons2(U, V), T), s1(X)) :- countstack2(push2(U, push2(V, T)), X).


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


countstack_2_in_ga2(empty_0, 0_0) -> countstack_2_out_ga2(empty_0, 0_0)
countstack_2_in_ga2(push_22(nil_0, T), X) -> if_countstack_2_in_1_ga3(T, X, countstack_2_in_ga2(T, X))
countstack_2_in_ga2(push_22(cons_22(U, V), T), s_11(X)) -> if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_out_ga2(push_22(U, push_22(V, T)), X)) -> countstack_2_out_ga2(push_22(cons_22(U, V), T), s_11(X))
if_countstack_2_in_1_ga3(T, X, countstack_2_out_ga2(T, X)) -> countstack_2_out_ga2(push_22(nil_0, T), X)

The argument filtering Pi contains the following mapping:
countstack_2_in_ga2(x1, x2)  =  countstack_2_in_ga1(x1)
empty_0  =  empty_0
0_0  =  0_0
push_22(x1, x2)  =  push_22(x1, x2)
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
s_11(x1)  =  s_11(x1)
countstack_2_out_ga2(x1, x2)  =  countstack_2_out_ga1(x2)
if_countstack_2_in_1_ga3(x1, x2, x3)  =  if_countstack_2_in_1_ga1(x3)
if_countstack_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_countstack_2_in_2_ga1(x5)

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:

countstack_2_in_ga2(empty_0, 0_0) -> countstack_2_out_ga2(empty_0, 0_0)
countstack_2_in_ga2(push_22(nil_0, T), X) -> if_countstack_2_in_1_ga3(T, X, countstack_2_in_ga2(T, X))
countstack_2_in_ga2(push_22(cons_22(U, V), T), s_11(X)) -> if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_out_ga2(push_22(U, push_22(V, T)), X)) -> countstack_2_out_ga2(push_22(cons_22(U, V), T), s_11(X))
if_countstack_2_in_1_ga3(T, X, countstack_2_out_ga2(T, X)) -> countstack_2_out_ga2(push_22(nil_0, T), X)

The argument filtering Pi contains the following mapping:
countstack_2_in_ga2(x1, x2)  =  countstack_2_in_ga1(x1)
empty_0  =  empty_0
0_0  =  0_0
push_22(x1, x2)  =  push_22(x1, x2)
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
s_11(x1)  =  s_11(x1)
countstack_2_out_ga2(x1, x2)  =  countstack_2_out_ga1(x2)
if_countstack_2_in_1_ga3(x1, x2, x3)  =  if_countstack_2_in_1_ga1(x3)
if_countstack_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_countstack_2_in_2_ga1(x5)


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

COUNTSTACK_2_IN_GA2(push_22(nil_0, T), X) -> IF_COUNTSTACK_2_IN_1_GA3(T, X, countstack_2_in_ga2(T, X))
COUNTSTACK_2_IN_GA2(push_22(nil_0, T), X) -> COUNTSTACK_2_IN_GA2(T, X)
COUNTSTACK_2_IN_GA2(push_22(cons_22(U, V), T), s_11(X)) -> IF_COUNTSTACK_2_IN_2_GA5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
COUNTSTACK_2_IN_GA2(push_22(cons_22(U, V), T), s_11(X)) -> COUNTSTACK_2_IN_GA2(push_22(U, push_22(V, T)), X)

The TRS R consists of the following rules:

countstack_2_in_ga2(empty_0, 0_0) -> countstack_2_out_ga2(empty_0, 0_0)
countstack_2_in_ga2(push_22(nil_0, T), X) -> if_countstack_2_in_1_ga3(T, X, countstack_2_in_ga2(T, X))
countstack_2_in_ga2(push_22(cons_22(U, V), T), s_11(X)) -> if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_out_ga2(push_22(U, push_22(V, T)), X)) -> countstack_2_out_ga2(push_22(cons_22(U, V), T), s_11(X))
if_countstack_2_in_1_ga3(T, X, countstack_2_out_ga2(T, X)) -> countstack_2_out_ga2(push_22(nil_0, T), X)

The argument filtering Pi contains the following mapping:
countstack_2_in_ga2(x1, x2)  =  countstack_2_in_ga1(x1)
empty_0  =  empty_0
0_0  =  0_0
push_22(x1, x2)  =  push_22(x1, x2)
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
s_11(x1)  =  s_11(x1)
countstack_2_out_ga2(x1, x2)  =  countstack_2_out_ga1(x2)
if_countstack_2_in_1_ga3(x1, x2, x3)  =  if_countstack_2_in_1_ga1(x3)
if_countstack_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_countstack_2_in_2_ga1(x5)
IF_COUNTSTACK_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_COUNTSTACK_2_IN_2_GA1(x5)
IF_COUNTSTACK_2_IN_1_GA3(x1, x2, x3)  =  IF_COUNTSTACK_2_IN_1_GA1(x3)
COUNTSTACK_2_IN_GA2(x1, x2)  =  COUNTSTACK_2_IN_GA1(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:

COUNTSTACK_2_IN_GA2(push_22(nil_0, T), X) -> IF_COUNTSTACK_2_IN_1_GA3(T, X, countstack_2_in_ga2(T, X))
COUNTSTACK_2_IN_GA2(push_22(nil_0, T), X) -> COUNTSTACK_2_IN_GA2(T, X)
COUNTSTACK_2_IN_GA2(push_22(cons_22(U, V), T), s_11(X)) -> IF_COUNTSTACK_2_IN_2_GA5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
COUNTSTACK_2_IN_GA2(push_22(cons_22(U, V), T), s_11(X)) -> COUNTSTACK_2_IN_GA2(push_22(U, push_22(V, T)), X)

The TRS R consists of the following rules:

countstack_2_in_ga2(empty_0, 0_0) -> countstack_2_out_ga2(empty_0, 0_0)
countstack_2_in_ga2(push_22(nil_0, T), X) -> if_countstack_2_in_1_ga3(T, X, countstack_2_in_ga2(T, X))
countstack_2_in_ga2(push_22(cons_22(U, V), T), s_11(X)) -> if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_out_ga2(push_22(U, push_22(V, T)), X)) -> countstack_2_out_ga2(push_22(cons_22(U, V), T), s_11(X))
if_countstack_2_in_1_ga3(T, X, countstack_2_out_ga2(T, X)) -> countstack_2_out_ga2(push_22(nil_0, T), X)

The argument filtering Pi contains the following mapping:
countstack_2_in_ga2(x1, x2)  =  countstack_2_in_ga1(x1)
empty_0  =  empty_0
0_0  =  0_0
push_22(x1, x2)  =  push_22(x1, x2)
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
s_11(x1)  =  s_11(x1)
countstack_2_out_ga2(x1, x2)  =  countstack_2_out_ga1(x2)
if_countstack_2_in_1_ga3(x1, x2, x3)  =  if_countstack_2_in_1_ga1(x3)
if_countstack_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_countstack_2_in_2_ga1(x5)
IF_COUNTSTACK_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_COUNTSTACK_2_IN_2_GA1(x5)
IF_COUNTSTACK_2_IN_1_GA3(x1, x2, x3)  =  IF_COUNTSTACK_2_IN_1_GA1(x3)
COUNTSTACK_2_IN_GA2(x1, x2)  =  COUNTSTACK_2_IN_GA1(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
              ↳ UsableRulesProof

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

COUNTSTACK_2_IN_GA2(push_22(cons_22(U, V), T), s_11(X)) -> COUNTSTACK_2_IN_GA2(push_22(U, push_22(V, T)), X)
COUNTSTACK_2_IN_GA2(push_22(nil_0, T), X) -> COUNTSTACK_2_IN_GA2(T, X)

The TRS R consists of the following rules:

countstack_2_in_ga2(empty_0, 0_0) -> countstack_2_out_ga2(empty_0, 0_0)
countstack_2_in_ga2(push_22(nil_0, T), X) -> if_countstack_2_in_1_ga3(T, X, countstack_2_in_ga2(T, X))
countstack_2_in_ga2(push_22(cons_22(U, V), T), s_11(X)) -> if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_in_ga2(push_22(U, push_22(V, T)), X))
if_countstack_2_in_2_ga5(U, V, T, X, countstack_2_out_ga2(push_22(U, push_22(V, T)), X)) -> countstack_2_out_ga2(push_22(cons_22(U, V), T), s_11(X))
if_countstack_2_in_1_ga3(T, X, countstack_2_out_ga2(T, X)) -> countstack_2_out_ga2(push_22(nil_0, T), X)

The argument filtering Pi contains the following mapping:
countstack_2_in_ga2(x1, x2)  =  countstack_2_in_ga1(x1)
empty_0  =  empty_0
0_0  =  0_0
push_22(x1, x2)  =  push_22(x1, x2)
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
s_11(x1)  =  s_11(x1)
countstack_2_out_ga2(x1, x2)  =  countstack_2_out_ga1(x2)
if_countstack_2_in_1_ga3(x1, x2, x3)  =  if_countstack_2_in_1_ga1(x3)
if_countstack_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_countstack_2_in_2_ga1(x5)
COUNTSTACK_2_IN_GA2(x1, x2)  =  COUNTSTACK_2_IN_GA1(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

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

COUNTSTACK_2_IN_GA2(push_22(cons_22(U, V), T), s_11(X)) -> COUNTSTACK_2_IN_GA2(push_22(U, push_22(V, T)), X)
COUNTSTACK_2_IN_GA2(push_22(nil_0, T), X) -> COUNTSTACK_2_IN_GA2(T, X)

R is empty.
The argument filtering Pi contains the following mapping:
push_22(x1, x2)  =  push_22(x1, x2)
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
s_11(x1)  =  s_11(x1)
COUNTSTACK_2_IN_GA2(x1, x2)  =  COUNTSTACK_2_IN_GA1(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
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ RuleRemovalProof

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

COUNTSTACK_2_IN_GA1(push_22(cons_22(U, V), T)) -> COUNTSTACK_2_IN_GA1(push_22(U, push_22(V, T)))
COUNTSTACK_2_IN_GA1(push_22(nil_0, T)) -> COUNTSTACK_2_IN_GA1(T)

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

COUNTSTACK_2_IN_GA1(push_22(cons_22(U, V), T)) -> COUNTSTACK_2_IN_GA1(push_22(U, push_22(V, T)))
COUNTSTACK_2_IN_GA1(push_22(nil_0, T)) -> COUNTSTACK_2_IN_GA1(T)


Used ordering: POLO with Polynomial interpretation:

POL(nil_0) = 0   
POL(push_22(x1, x2)) = 1 + x1 + x2   
POL(COUNTSTACK_2_IN_GA1(x1)) = 1 + x1   
POL(cons_22(x1, x2)) = 2 + x1 + x2   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ RuleRemovalProof
                        ↳ QDP
                          ↳ PisEmptyProof

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are empty set.
The TRS P is empty. Hence, there is no (P,Q,R) chain.