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

0 Prolog
↳1 CutEliminatorProof (⇐)
↳2 Prolog
↳3 UndefinedPredicateHandlerProof (⇐)
↳4 Prolog
  ↳5 PrologToPiTRSProof (⇐)
    ↳6 PiTRS
    ↳7 DependencyPairsProof (⇔)
    ↳8 PiDP
    ↳9 DependencyGraphProof (⇔)
    ↳10 AND
      ↳11 PiDP
        ↳12 UsableRulesProof (⇔)
        ↳13 PiDP
        ↳14 PiDPToQDPProof (⇐)
        ↳15 QDP
        ↳16 NonTerminationProof (⇔)
        ↳17 FALSE
      ↳18 PiDP
        ↳19 UsableRulesProof (⇔)
        ↳20 PiDP
        ↳21 PiDPToQDPProof (⇐)
        ↳22 QDP
        ↳23 QDPSizeChangeProof (⇔)
        ↳24 TRUE
  ↳25 PrologToPiTRSProof (⇐)
    ↳26 PiTRS
    ↳27 DependencyPairsProof (⇔)
    ↳28 PiDP
    ↳29 DependencyGraphProof (⇔)
    ↳30 AND
      ↳31 PiDP
        ↳32 UsableRulesProof (⇔)
        ↳33 PiDP
        ↳34 PiDPToQDPProof (⇐)
        ↳35 QDP
        ↳36 NonTerminationProof (⇔)
        ↳37 FALSE
      ↳38 PiDP
        ↳39 UsableRulesProof (⇔)
        ↳40 PiDP
        ↳41 PiDPToQDPProof (⇐)
        ↳42 QDP
        ↳43 QDPSizeChangeProof (⇔)
        ↳44 TRUE

(0) Obligation:

Clauses:

goal :- ','(lte(X, s(s(s(s(0))))), even(X)).
lte(0, Y) :- !.
lte(X, s(Y)) :- ','(p(X, P), lte(P, Y)).
even(0).
even(s(s(X))) :- even(X).
p(0, 0).
p(s(X), X).

Queries:

goal().

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

goal :- ','(lte(X, s(s(s(s(0))))), even(X)).
lte(0, Y) :- true.
lte(X, s(Y)) :- ','(p(X, P), lte(P, Y)).
even(0).
even(s(s(X))) :- even(X).
p(0, 0).
p(s(X), X).

Queries:

goal().

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

goal :- ','(lte(X, s(s(s(s(0))))), even(X)).
lte(0, Y) :- true.
lte(X, s(Y)) :- ','(p(X, P), lte(P, Y)).
even(0).
even(s(s(X))) :- even(X).
p(0, 0).
p(s(X), X).
true.

Queries:

goal().

(5) PrologToPiTRSProof (SOUND transformation)

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

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_

(7) 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:

GOAL_IN_ → U1_1(lte_in_ag(X, s(s(s(s(0))))))
GOAL_IN_ → LTE_IN_AG(X, s(s(s(s(0)))))
LTE_IN_AG(0, Y) → U3_AG(Y, true_in_)
LTE_IN_AG(0, Y) → TRUE_IN_
LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
LTE_IN_AG(X, s(Y)) → P_IN_AA(X, P)
U4_AG(X, Y, p_out_aa(X, P)) → U5_AG(X, Y, lte_in_ag(P, Y))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → U2_1(even_in_a(X))
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → EVEN_IN_A(X)
EVEN_IN_A(s(s(X))) → U6_A(X, even_in_a(X))
EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
GOAL_IN_  =  GOAL_IN_
U1_1(x1)  =  U1_1(x1)
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U3_AG(x1, x2)  =  U3_AG(x2)
TRUE_IN_  =  TRUE_IN_
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U5_AG(x1, x2, x3)  =  U5_AG(x3)
U2_1(x1)  =  U2_1(x1)
EVEN_IN_A(x1)  =  EVEN_IN_A
U6_A(x1, x2)  =  U6_A(x2)

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

(8) Obligation:

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

GOAL_IN_ → U1_1(lte_in_ag(X, s(s(s(s(0))))))
GOAL_IN_ → LTE_IN_AG(X, s(s(s(s(0)))))
LTE_IN_AG(0, Y) → U3_AG(Y, true_in_)
LTE_IN_AG(0, Y) → TRUE_IN_
LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
LTE_IN_AG(X, s(Y)) → P_IN_AA(X, P)
U4_AG(X, Y, p_out_aa(X, P)) → U5_AG(X, Y, lte_in_ag(P, Y))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → U2_1(even_in_a(X))
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → EVEN_IN_A(X)
EVEN_IN_A(s(s(X))) → U6_A(X, even_in_a(X))
EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
GOAL_IN_  =  GOAL_IN_
U1_1(x1)  =  U1_1(x1)
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U3_AG(x1, x2)  =  U3_AG(x2)
TRUE_IN_  =  TRUE_IN_
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U5_AG(x1, x2, x3)  =  U5_AG(x3)
U2_1(x1)  =  U2_1(x1)
EVEN_IN_A(x1)  =  EVEN_IN_A
U6_A(x1, x2)  =  U6_A(x2)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Complex Obligation (AND)

(11) Obligation:

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

EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
EVEN_IN_A(x1)  =  EVEN_IN_A

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

(12) UsableRulesProof (EQUIVALENT transformation)

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

(13) Obligation:

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

EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
EVEN_IN_A(x1)  =  EVEN_IN_A

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

(14) PiDPToQDPProof (SOUND transformation)

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

(15) Obligation:

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

EVEN_IN_A → EVEN_IN_A

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

(16) 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 = EVEN_IN_A evaluates to t =EVEN_IN_A

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



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from EVEN_IN_A to EVEN_IN_A.



(17) FALSE

(18) Obligation:

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

LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)

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

(19) UsableRulesProof (EQUIVALENT transformation)

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

(20) Obligation:

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

LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
0  =  0
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)

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

(21) PiDPToQDPProof (SOUND transformation)

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

(22) Obligation:

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

LTE_IN_AG(s(Y)) → U4_AG(Y, p_in_aa)
U4_AG(Y, p_out_aa) → LTE_IN_AG(Y)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(23) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • U4_AG(Y, p_out_aa) → LTE_IN_AG(Y)
    The graph contains the following edges 1 >= 1

  • LTE_IN_AG(s(Y)) → U4_AG(Y, p_in_aa)
    The graph contains the following edges 1 > 1

(24) TRUE

(25) PrologToPiTRSProof (SOUND transformation)

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

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag(x2)
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x2, x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(26) Obligation:

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

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag(x2)
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x2, x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_

(27) 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:

GOAL_IN_ → U1_1(lte_in_ag(X, s(s(s(s(0))))))
GOAL_IN_ → LTE_IN_AG(X, s(s(s(s(0)))))
LTE_IN_AG(0, Y) → U3_AG(Y, true_in_)
LTE_IN_AG(0, Y) → TRUE_IN_
LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
LTE_IN_AG(X, s(Y)) → P_IN_AA(X, P)
U4_AG(X, Y, p_out_aa(X, P)) → U5_AG(X, Y, lte_in_ag(P, Y))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → U2_1(even_in_a(X))
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → EVEN_IN_A(X)
EVEN_IN_A(s(s(X))) → U6_A(X, even_in_a(X))
EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag(x2)
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x2, x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
GOAL_IN_  =  GOAL_IN_
U1_1(x1)  =  U1_1(x1)
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U3_AG(x1, x2)  =  U3_AG(x1, x2)
TRUE_IN_  =  TRUE_IN_
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U5_AG(x1, x2, x3)  =  U5_AG(x2, x3)
U2_1(x1)  =  U2_1(x1)
EVEN_IN_A(x1)  =  EVEN_IN_A
U6_A(x1, x2)  =  U6_A(x2)

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

(28) Obligation:

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

GOAL_IN_ → U1_1(lte_in_ag(X, s(s(s(s(0))))))
GOAL_IN_ → LTE_IN_AG(X, s(s(s(s(0)))))
LTE_IN_AG(0, Y) → U3_AG(Y, true_in_)
LTE_IN_AG(0, Y) → TRUE_IN_
LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
LTE_IN_AG(X, s(Y)) → P_IN_AA(X, P)
U4_AG(X, Y, p_out_aa(X, P)) → U5_AG(X, Y, lte_in_ag(P, Y))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → U2_1(even_in_a(X))
U1_1(lte_out_ag(X, s(s(s(s(0)))))) → EVEN_IN_A(X)
EVEN_IN_A(s(s(X))) → U6_A(X, even_in_a(X))
EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag(x2)
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x2, x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
GOAL_IN_  =  GOAL_IN_
U1_1(x1)  =  U1_1(x1)
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U3_AG(x1, x2)  =  U3_AG(x1, x2)
TRUE_IN_  =  TRUE_IN_
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U5_AG(x1, x2, x3)  =  U5_AG(x2, x3)
U2_1(x1)  =  U2_1(x1)
EVEN_IN_A(x1)  =  EVEN_IN_A
U6_A(x1, x2)  =  U6_A(x2)

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

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(30) Complex Obligation (AND)

(31) Obligation:

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

EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag(x2)
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x2, x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
EVEN_IN_A(x1)  =  EVEN_IN_A

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

(32) UsableRulesProof (EQUIVALENT transformation)

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

(33) Obligation:

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

EVEN_IN_A(s(s(X))) → EVEN_IN_A(X)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
EVEN_IN_A(x1)  =  EVEN_IN_A

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

(34) PiDPToQDPProof (SOUND transformation)

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

(35) Obligation:

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

EVEN_IN_A → EVEN_IN_A

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

(36) 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 = EVEN_IN_A evaluates to t =EVEN_IN_A

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



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from EVEN_IN_A to EVEN_IN_A.



(37) FALSE

(38) Obligation:

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

LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)

The TRS R consists of the following rules:

goal_in_ → U1_(lte_in_ag(X, s(s(s(s(0))))))
lte_in_ag(0, Y) → U3_ag(Y, true_in_)
true_in_ → true_out_
U3_ag(Y, true_out_) → lte_out_ag(0, Y)
lte_in_ag(X, s(Y)) → U4_ag(X, Y, p_in_aa(X, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U4_ag(X, Y, p_out_aa(X, P)) → U5_ag(X, Y, lte_in_ag(P, Y))
U5_ag(X, Y, lte_out_ag(P, Y)) → lte_out_ag(X, s(Y))
U1_(lte_out_ag(X, s(s(s(s(0)))))) → U2_(even_in_a(X))
even_in_a(0) → even_out_a(0)
even_in_a(s(s(X))) → U6_a(X, even_in_a(X))
U6_a(X, even_out_a(X)) → even_out_a(s(s(X)))
U2_(even_out_a(X)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
lte_in_ag(x1, x2)  =  lte_in_ag(x2)
U3_ag(x1, x2)  =  U3_ag(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
lte_out_ag(x1, x2)  =  lte_out_ag(x2)
s(x1)  =  s(x1)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U5_ag(x1, x2, x3)  =  U5_ag(x2, x3)
0  =  0
U2_(x1)  =  U2_(x1)
even_in_a(x1)  =  even_in_a
even_out_a(x1)  =  even_out_a(x1)
U6_a(x1, x2)  =  U6_a(x2)
goal_out_  =  goal_out_
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)

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

(39) UsableRulesProof (EQUIVALENT transformation)

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

(40) Obligation:

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

LTE_IN_AG(X, s(Y)) → U4_AG(X, Y, p_in_aa(X, P))
U4_AG(X, Y, p_out_aa(X, P)) → LTE_IN_AG(P, Y)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
0  =  0
LTE_IN_AG(x1, x2)  =  LTE_IN_AG(x2)
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)

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

(41) PiDPToQDPProof (SOUND transformation)

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

(42) Obligation:

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

LTE_IN_AG(s(Y)) → U4_AG(Y, p_in_aa)
U4_AG(Y, p_out_aa) → LTE_IN_AG(Y)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(43) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • U4_AG(Y, p_out_aa) → LTE_IN_AG(Y)
    The graph contains the following edges 1 >= 1

  • LTE_IN_AG(s(Y)) → U4_AG(Y, p_in_aa)
    The graph contains the following edges 1 > 1

(44) TRUE