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

0 Prolog
  ↳1 PrologToPiTRSProof (⇐)
    ↳2 PiTRS
    ↳3 DependencyPairsProof (⇔)
    ↳4 PiDP
    ↳5 DependencyGraphProof (⇔)
    ↳6 AND
      ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 MRRProof (⇔)
        ↳13 QDP
        ↳14 DependencyGraphProof (⇔)
        ↳15 TRUE
      ↳16 PiDP
        ↳17 UsableRulesProof (⇔)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇐)
        ↳20 QDP
          ↳21 Instantiation (⇔)
            ↳22 QDP
          ↳23 Instantiation (⇔)
            ↳24 QDP
            ↳25 Instantiation (⇔)
            ↳26 QDP
            ↳27 NonTerminationProof (⇔)
            ↳28 FALSE
  ↳29 PrologToPiTRSProof (⇐)
    ↳30 PiTRS
    ↳31 DependencyPairsProof (⇔)
    ↳32 PiDP
    ↳33 DependencyGraphProof (⇔)
    ↳34 AND
      ↳35 PiDP
        ↳36 UsableRulesProof (⇔)
        ↳37 PiDP
        ↳38 PiDPToQDPProof (⇔)
        ↳39 QDP
        ↳40 MRRProof (⇔)
        ↳41 QDP
        ↳42 DependencyGraphProof (⇔)
        ↳43 TRUE
      ↳44 PiDP
        ↳45 UsableRulesProof (⇔)
        ↳46 PiDP
        ↳47 PiDPToQDPProof (⇐)
        ↳48 QDP
          ↳49 Instantiation (⇔)
            ↳50 QDP
          ↳51 Instantiation (⇔)
            ↳52 QDP
            ↳53 Instantiation (⇔)
            ↳54 QDP
            ↳55 NonTerminationProof (⇔)
            ↳56 FALSE

(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, s(0), Y).
log2(s(s(X)), Half, Acc, Y) :- log2(X, s(Half), Acc, Y).
log2(X, s(s(Half)), Acc, Y) :- ','(small(X), log2(Half, s(0), s(Acc), Y)).
log2(X, Half, Y, Y) :- ','(small(X), small(Half)).
small(0).
small(s(0)).

Queries:

log2(a,g).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
log2_in: (f,b)
log2_in: (f,b,b,b) (b,b,b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x3)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x5)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
SMALL_IN_A(x1)  =  SMALL_IN_A
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x5)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x5)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x2, x4)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x4)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x4)

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

(4) Obligation:

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

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x3)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x5)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
SMALL_IN_A(x1)  =  SMALL_IN_A
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x5)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x5)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x2, x4)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x4)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 18 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)

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

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)

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

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(Half, Acc, Y, small_in_g(X))
U3_GGGG(Half, Acc, Y, small_out_g) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g
small_in_g(s(0)) → small_out_g

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.

(12) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

Strictly oriented rules of the TRS R:

small_in_g(s(0)) → small_out_g

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(LOG2_IN_GGGG(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(U3_GGGG(x1, x2, x3, x4)) = 2 + x1 + x2 + x3 + x4   
POL(s(x1)) = 1 + x1   
POL(small_in_g(x1)) = x1   
POL(small_out_g) = 0   

(13) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(Half, Acc, Y, small_in_g(X))
U3_GGGG(Half, Acc, Y, small_out_g) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.

(14) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(15) TRUE

(16) Obligation:

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

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

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

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

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

LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y)

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

(21) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y) we obtained the following new rules [LPAR04]:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

(22) Obligation:

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

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

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

(23) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y) we obtained the following new rules [LPAR04]:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

(24) Obligation:

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

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

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

(25) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2) we obtained the following new rules [LPAR04]:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

(26) Obligation:

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

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

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

(27) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = LOG2_IN_AGGG(s(s(z0)), z1, z2) evaluates to t =LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [z0 / s(z0)]
  • Semiunifier: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG2_IN_AGGG(s(s(z0)), z1, z2) to LOG2_IN_AGGG(s(s(s(z0))), z1, z2).



(28) FALSE

(29) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
log2_in: (f,b)
log2_in: (f,b,b,b) (b,b,b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(30) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)

(31) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
SMALL_IN_A(x1)  =  SMALL_IN_A
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x2, x3, x4, x5)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x1, x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x1, x2, x3, x4, x5)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x1, x2, x3, x4, x5)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x1, x2, x3, x4)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x1, x2, x3, x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x3, x4)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x2, x3, x4)

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

(32) Obligation:

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

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
SMALL_IN_A(x1)  =  SMALL_IN_A
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x2, x3, x4, x5)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x1, x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x1, x2, x3, x4, x5)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x1, x2, x3, x4, x5)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x1, x2, x3, x4)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x1, x2, x3, x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x3, x4)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x2, x3, x4)

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

(33) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 18 less nodes.

(34) Complex Obligation (AND)

(35) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x1, x2, x3, x4, x5)

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

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

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

(38) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

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

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.

(40) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(LOG2_IN_GGGG(x1, x2, x3, x4)) = 2·x1 + 2·x2 + x3 + x4   
POL(U3_GGGG(x1, x2, x3, x4, x5)) = 1 + x1 + 2·x2 + x3 + x4 + x5   
POL(s(x1)) = 1 + x1   
POL(small_in_g(x1)) = 2 + x1   
POL(small_out_g(x1)) = 2 + x1   

(41) Obligation:

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

U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.

(42) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(43) TRUE

(44) Obligation:

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

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

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

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

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

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

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

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

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

LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y)

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

(49) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y) we obtained the following new rules [LPAR04]:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

(50) Obligation:

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

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

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

(51) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y) we obtained the following new rules [LPAR04]:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

(52) Obligation:

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

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

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

(53) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2) we obtained the following new rules [LPAR04]:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

(54) Obligation:

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

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

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

(55) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = LOG2_IN_AGGG(s(s(z0)), z1, z2) evaluates to t =LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [z0 / s(z0)]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG2_IN_AGGG(s(s(z0)), z1, z2) to LOG2_IN_AGGG(s(s(s(z0))), z1, z2).



(56) FALSE