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



PROLOG
  ↳ PrologToPiTRSProof

average3(00, 00, 00).
average3(00, s1(00), 00).
average3(00, s12 (00), s1(00)).
average3(s1(X), Y, Z) :- average3(X, s1(Y), Z).
average3(X, s13 (Y), s1(Z)) :- average3(s1(X), Y, Z).


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


average_3_in_gag3(0_0, 0_0, 0_0) -> average_3_out_gag3(0_0, 0_0, 0_0)
average_3_in_gag3(0_0, s_11(0_0), 0_0) -> average_3_out_gag3(0_0, s_11(0_0), 0_0)
average_3_in_gag3(0_0, s_11(s_11(0_0)), s_11(0_0)) -> average_3_out_gag3(0_0, s_11(s_11(0_0)), s_11(0_0))
average_3_in_gag3(s_11(X), Y, Z) -> if_average_3_in_1_gag4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
average_3_in_gag3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> if_average_3_in_2_gag4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
if_average_3_in_2_gag4(X, Y, Z, average_3_out_gag3(s_11(X), Y, Z)) -> average_3_out_gag3(X, s_11(s_11(s_11(Y))), s_11(Z))
if_average_3_in_1_gag4(X, Y, Z, average_3_out_gag3(X, s_11(Y), Z)) -> average_3_out_gag3(s_11(X), Y, Z)

The argument filtering Pi contains the following mapping:
average_3_in_gag3(x1, x2, x3)  =  average_3_in_gag2(x1, x3)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
average_3_out_gag3(x1, x2, x3)  =  average_3_out_gag1(x2)
if_average_3_in_1_gag4(x1, x2, x3, x4)  =  if_average_3_in_1_gag1(x4)
if_average_3_in_2_gag4(x1, x2, x3, x4)  =  if_average_3_in_2_gag1(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:

average_3_in_gag3(0_0, 0_0, 0_0) -> average_3_out_gag3(0_0, 0_0, 0_0)
average_3_in_gag3(0_0, s_11(0_0), 0_0) -> average_3_out_gag3(0_0, s_11(0_0), 0_0)
average_3_in_gag3(0_0, s_11(s_11(0_0)), s_11(0_0)) -> average_3_out_gag3(0_0, s_11(s_11(0_0)), s_11(0_0))
average_3_in_gag3(s_11(X), Y, Z) -> if_average_3_in_1_gag4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
average_3_in_gag3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> if_average_3_in_2_gag4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
if_average_3_in_2_gag4(X, Y, Z, average_3_out_gag3(s_11(X), Y, Z)) -> average_3_out_gag3(X, s_11(s_11(s_11(Y))), s_11(Z))
if_average_3_in_1_gag4(X, Y, Z, average_3_out_gag3(X, s_11(Y), Z)) -> average_3_out_gag3(s_11(X), Y, Z)

The argument filtering Pi contains the following mapping:
average_3_in_gag3(x1, x2, x3)  =  average_3_in_gag2(x1, x3)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
average_3_out_gag3(x1, x2, x3)  =  average_3_out_gag1(x2)
if_average_3_in_1_gag4(x1, x2, x3, x4)  =  if_average_3_in_1_gag1(x4)
if_average_3_in_2_gag4(x1, x2, x3, x4)  =  if_average_3_in_2_gag1(x4)


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

AVERAGE_3_IN_GAG3(s_11(X), Y, Z) -> IF_AVERAGE_3_IN_1_GAG4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
AVERAGE_3_IN_GAG3(s_11(X), Y, Z) -> AVERAGE_3_IN_GAG3(X, s_11(Y), Z)
AVERAGE_3_IN_GAG3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> IF_AVERAGE_3_IN_2_GAG4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
AVERAGE_3_IN_GAG3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> AVERAGE_3_IN_GAG3(s_11(X), Y, Z)

The TRS R consists of the following rules:

average_3_in_gag3(0_0, 0_0, 0_0) -> average_3_out_gag3(0_0, 0_0, 0_0)
average_3_in_gag3(0_0, s_11(0_0), 0_0) -> average_3_out_gag3(0_0, s_11(0_0), 0_0)
average_3_in_gag3(0_0, s_11(s_11(0_0)), s_11(0_0)) -> average_3_out_gag3(0_0, s_11(s_11(0_0)), s_11(0_0))
average_3_in_gag3(s_11(X), Y, Z) -> if_average_3_in_1_gag4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
average_3_in_gag3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> if_average_3_in_2_gag4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
if_average_3_in_2_gag4(X, Y, Z, average_3_out_gag3(s_11(X), Y, Z)) -> average_3_out_gag3(X, s_11(s_11(s_11(Y))), s_11(Z))
if_average_3_in_1_gag4(X, Y, Z, average_3_out_gag3(X, s_11(Y), Z)) -> average_3_out_gag3(s_11(X), Y, Z)

The argument filtering Pi contains the following mapping:
average_3_in_gag3(x1, x2, x3)  =  average_3_in_gag2(x1, x3)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
average_3_out_gag3(x1, x2, x3)  =  average_3_out_gag1(x2)
if_average_3_in_1_gag4(x1, x2, x3, x4)  =  if_average_3_in_1_gag1(x4)
if_average_3_in_2_gag4(x1, x2, x3, x4)  =  if_average_3_in_2_gag1(x4)
IF_AVERAGE_3_IN_1_GAG4(x1, x2, x3, x4)  =  IF_AVERAGE_3_IN_1_GAG1(x4)
IF_AVERAGE_3_IN_2_GAG4(x1, x2, x3, x4)  =  IF_AVERAGE_3_IN_2_GAG1(x4)
AVERAGE_3_IN_GAG3(x1, x2, x3)  =  AVERAGE_3_IN_GAG2(x1, x3)

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:

AVERAGE_3_IN_GAG3(s_11(X), Y, Z) -> IF_AVERAGE_3_IN_1_GAG4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
AVERAGE_3_IN_GAG3(s_11(X), Y, Z) -> AVERAGE_3_IN_GAG3(X, s_11(Y), Z)
AVERAGE_3_IN_GAG3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> IF_AVERAGE_3_IN_2_GAG4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
AVERAGE_3_IN_GAG3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> AVERAGE_3_IN_GAG3(s_11(X), Y, Z)

The TRS R consists of the following rules:

average_3_in_gag3(0_0, 0_0, 0_0) -> average_3_out_gag3(0_0, 0_0, 0_0)
average_3_in_gag3(0_0, s_11(0_0), 0_0) -> average_3_out_gag3(0_0, s_11(0_0), 0_0)
average_3_in_gag3(0_0, s_11(s_11(0_0)), s_11(0_0)) -> average_3_out_gag3(0_0, s_11(s_11(0_0)), s_11(0_0))
average_3_in_gag3(s_11(X), Y, Z) -> if_average_3_in_1_gag4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
average_3_in_gag3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> if_average_3_in_2_gag4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
if_average_3_in_2_gag4(X, Y, Z, average_3_out_gag3(s_11(X), Y, Z)) -> average_3_out_gag3(X, s_11(s_11(s_11(Y))), s_11(Z))
if_average_3_in_1_gag4(X, Y, Z, average_3_out_gag3(X, s_11(Y), Z)) -> average_3_out_gag3(s_11(X), Y, Z)

The argument filtering Pi contains the following mapping:
average_3_in_gag3(x1, x2, x3)  =  average_3_in_gag2(x1, x3)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
average_3_out_gag3(x1, x2, x3)  =  average_3_out_gag1(x2)
if_average_3_in_1_gag4(x1, x2, x3, x4)  =  if_average_3_in_1_gag1(x4)
if_average_3_in_2_gag4(x1, x2, x3, x4)  =  if_average_3_in_2_gag1(x4)
IF_AVERAGE_3_IN_1_GAG4(x1, x2, x3, x4)  =  IF_AVERAGE_3_IN_1_GAG1(x4)
IF_AVERAGE_3_IN_2_GAG4(x1, x2, x3, x4)  =  IF_AVERAGE_3_IN_2_GAG1(x4)
AVERAGE_3_IN_GAG3(x1, x2, x3)  =  AVERAGE_3_IN_GAG2(x1, x3)

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:

AVERAGE_3_IN_GAG3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> AVERAGE_3_IN_GAG3(s_11(X), Y, Z)
AVERAGE_3_IN_GAG3(s_11(X), Y, Z) -> AVERAGE_3_IN_GAG3(X, s_11(Y), Z)

The TRS R consists of the following rules:

average_3_in_gag3(0_0, 0_0, 0_0) -> average_3_out_gag3(0_0, 0_0, 0_0)
average_3_in_gag3(0_0, s_11(0_0), 0_0) -> average_3_out_gag3(0_0, s_11(0_0), 0_0)
average_3_in_gag3(0_0, s_11(s_11(0_0)), s_11(0_0)) -> average_3_out_gag3(0_0, s_11(s_11(0_0)), s_11(0_0))
average_3_in_gag3(s_11(X), Y, Z) -> if_average_3_in_1_gag4(X, Y, Z, average_3_in_gag3(X, s_11(Y), Z))
average_3_in_gag3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> if_average_3_in_2_gag4(X, Y, Z, average_3_in_gag3(s_11(X), Y, Z))
if_average_3_in_2_gag4(X, Y, Z, average_3_out_gag3(s_11(X), Y, Z)) -> average_3_out_gag3(X, s_11(s_11(s_11(Y))), s_11(Z))
if_average_3_in_1_gag4(X, Y, Z, average_3_out_gag3(X, s_11(Y), Z)) -> average_3_out_gag3(s_11(X), Y, Z)

The argument filtering Pi contains the following mapping:
average_3_in_gag3(x1, x2, x3)  =  average_3_in_gag2(x1, x3)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
average_3_out_gag3(x1, x2, x3)  =  average_3_out_gag1(x2)
if_average_3_in_1_gag4(x1, x2, x3, x4)  =  if_average_3_in_1_gag1(x4)
if_average_3_in_2_gag4(x1, x2, x3, x4)  =  if_average_3_in_2_gag1(x4)
AVERAGE_3_IN_GAG3(x1, x2, x3)  =  AVERAGE_3_IN_GAG2(x1, x3)

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:

AVERAGE_3_IN_GAG3(X, s_11(s_11(s_11(Y))), s_11(Z)) -> AVERAGE_3_IN_GAG3(s_11(X), Y, Z)
AVERAGE_3_IN_GAG3(s_11(X), Y, Z) -> AVERAGE_3_IN_GAG3(X, s_11(Y), Z)

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
AVERAGE_3_IN_GAG3(x1, x2, x3)  =  AVERAGE_3_IN_GAG2(x1, x3)

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
                      ↳ QDPSizeChangeProof

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

AVERAGE_3_IN_GAG2(X, s_11(Z)) -> AVERAGE_3_IN_GAG2(s_11(X), Z)
AVERAGE_3_IN_GAG2(s_11(X), Z) -> AVERAGE_3_IN_GAG2(X, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {AVERAGE_3_IN_GAG2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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