Left Termination of the query pattern even_in_1(g) 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 PiDP
    ↳11 UsableRulesProof (⇔)
    ↳12 PiDP
    ↳13 PiDPToQDPProof (⇐)
    ↳14 QDP
    ↳15 Rewriting (⇔)
    ↳16 QDP
    ↳17 UsableRulesProof (⇔)
    ↳18 QDP
    ↳19 QReductionProof (⇔)
    ↳20 QDP
    ↳21 NonTerminationProof (⇔)
    ↳22 FALSE
  ↳23 PrologToPiTRSProof (⇐)
    ↳24 PiTRS
    ↳25 DependencyPairsProof (⇔)
    ↳26 PiDP
    ↳27 DependencyGraphProof (⇔)
    ↳28 PiDP
    ↳29 UsableRulesProof (⇔)
    ↳30 PiDP
    ↳31 PiDPToQDPProof (⇐)
    ↳32 QDP
    ↳33 Rewriting (⇔)
    ↳34 QDP
    ↳35 UsableRulesProof (⇔)
    ↳36 QDP
    ↳37 QReductionProof (⇔)
    ↳38 QDP
    ↳39 NonTerminationProof (⇔)
    ↳40 FALSE

(0) Obligation:

Clauses:

even(0) :- !.
even(N) :- ','(p(N, P), odd(P)).
odd(s(0)) :- !.
odd(s(N)) :- even(P).
p(0, 0).
p(s(X), X).

Queries:

even(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

even(0) :- true.
even(N) :- ','(p(N, P), odd(P)).
odd(s(0)) :- true.
odd(s(N)) :- even(P).
p(0, 0).
p(s(X), X).

Queries:

even(g).

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

even(0) :- true.
even(N) :- ','(p(N, P), odd(P)).
odd(s(0)) :- true.
odd(s(N)) :- even(P).
p(0, 0).
p(s(X), X).
true.

Queries:

even(g).

(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:
even_in: (b) (f)
odd_in: (b) (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g
U2_g(x1, x2)  =  U2_g(x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g
U5_g(x1, x2)  =  U5_g(x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g
U2_g(x1, x2)  =  U2_g(x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g
U5_g(x1, x2)  =  U5_g(x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)

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

EVEN_IN_G(0) → U1_G(true_in_)
EVEN_IN_G(0) → TRUE_IN_
EVEN_IN_G(N) → U2_G(N, p_in_ga(N, P))
EVEN_IN_G(N) → P_IN_GA(N, P)
U2_G(N, p_out_ga(N, P)) → U3_G(N, odd_in_g(P))
U2_G(N, p_out_ga(N, P)) → ODD_IN_G(P)
ODD_IN_G(s(0)) → U4_G(true_in_)
ODD_IN_G(s(0)) → TRUE_IN_
ODD_IN_G(s(N)) → U5_G(N, even_in_a(P))
ODD_IN_G(s(N)) → EVEN_IN_A(P)
EVEN_IN_A(0) → U1_A(true_in_)
EVEN_IN_A(0) → TRUE_IN_
EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
EVEN_IN_A(N) → P_IN_AA(N, P)
U2_A(N, p_out_aa(N, P)) → U3_A(N, odd_in_a(P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(0)) → U4_A(true_in_)
ODD_IN_A(s(0)) → TRUE_IN_
ODD_IN_A(s(N)) → U5_A(N, even_in_a(P))
ODD_IN_A(s(N)) → EVEN_IN_A(P)

The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g
U2_g(x1, x2)  =  U2_g(x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g
U5_g(x1, x2)  =  U5_g(x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)
EVEN_IN_G(x1)  =  EVEN_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x2)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U3_G(x1, x2)  =  U3_G(x2)
ODD_IN_G(x1)  =  ODD_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
U5_G(x1, x2)  =  U5_G(x2)
EVEN_IN_A(x1)  =  EVEN_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
P_IN_AA(x1, x2)  =  P_IN_AA
U3_A(x1, x2)  =  U3_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A
U4_A(x1)  =  U4_A(x1)
U5_A(x1, x2)  =  U5_A(x2)

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

(8) Obligation:

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

EVEN_IN_G(0) → U1_G(true_in_)
EVEN_IN_G(0) → TRUE_IN_
EVEN_IN_G(N) → U2_G(N, p_in_ga(N, P))
EVEN_IN_G(N) → P_IN_GA(N, P)
U2_G(N, p_out_ga(N, P)) → U3_G(N, odd_in_g(P))
U2_G(N, p_out_ga(N, P)) → ODD_IN_G(P)
ODD_IN_G(s(0)) → U4_G(true_in_)
ODD_IN_G(s(0)) → TRUE_IN_
ODD_IN_G(s(N)) → U5_G(N, even_in_a(P))
ODD_IN_G(s(N)) → EVEN_IN_A(P)
EVEN_IN_A(0) → U1_A(true_in_)
EVEN_IN_A(0) → TRUE_IN_
EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
EVEN_IN_A(N) → P_IN_AA(N, P)
U2_A(N, p_out_aa(N, P)) → U3_A(N, odd_in_a(P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(0)) → U4_A(true_in_)
ODD_IN_A(s(0)) → TRUE_IN_
ODD_IN_A(s(N)) → U5_A(N, even_in_a(P))
ODD_IN_A(s(N)) → EVEN_IN_A(P)

The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g
U2_g(x1, x2)  =  U2_g(x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g
U5_g(x1, x2)  =  U5_g(x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)
EVEN_IN_G(x1)  =  EVEN_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x2)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U3_G(x1, x2)  =  U3_G(x2)
ODD_IN_G(x1)  =  ODD_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
U5_G(x1, x2)  =  U5_G(x2)
EVEN_IN_A(x1)  =  EVEN_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
P_IN_AA(x1, x2)  =  P_IN_AA
U3_A(x1, x2)  =  U3_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A
U4_A(x1)  =  U4_A(x1)
U5_A(x1, x2)  =  U5_A(x2)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 17 less nodes.

(10) Obligation:

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

EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(N)) → EVEN_IN_A(P)

The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g
U2_g(x1, x2)  =  U2_g(x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g
U5_g(x1, x2)  =  U5_g(x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)
EVEN_IN_A(x1)  =  EVEN_IN_A
U2_A(x1, x2)  =  U2_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A

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

(11) UsableRulesProof (EQUIVALENT transformation)

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

(12) Obligation:

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

EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(N)) → EVEN_IN_A(P)

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:
0  =  0
s(x1)  =  s(x1)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
EVEN_IN_A(x1)  =  EVEN_IN_A
U2_A(x1, x2)  =  U2_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A

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

(13) PiDPToQDPProof (SOUND transformation)

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

(14) Obligation:

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

EVEN_IN_A → U2_A(p_in_aa)
U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A

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.

(15) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule EVEN_IN_A → U2_A(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

EVEN_IN_A → U2_A(p_out_aa)

(16) Obligation:

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

U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A
EVEN_IN_A → U2_A(p_out_aa)

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.

(17) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(18) Obligation:

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

U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A
EVEN_IN_A → U2_A(p_out_aa)

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

p_in_aa

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

(19) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

p_in_aa

(20) Obligation:

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

U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A
EVEN_IN_A → U2_A(p_out_aa)

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

(21) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ODD_IN_A evaluates to t =ODD_IN_A

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



Rewriting sequence

ODD_IN_A → EVEN_IN_A
with rule ODD_IN_A → EVEN_IN_A at position [] and matcher [ ]

EVEN_IN_A → U2_A(p_out_aa)
with rule EVEN_IN_A → U2_A(p_out_aa) at position [] and matcher [ ]

U2_A(p_out_aa) → ODD_IN_A
with rule U2_A(p_out_aa) → ODD_IN_A

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(22) FALSE

(23) PrologToPiTRSProof (SOUND transformation)

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

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(24) Obligation:

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

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)

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

EVEN_IN_G(0) → U1_G(true_in_)
EVEN_IN_G(0) → TRUE_IN_
EVEN_IN_G(N) → U2_G(N, p_in_ga(N, P))
EVEN_IN_G(N) → P_IN_GA(N, P)
U2_G(N, p_out_ga(N, P)) → U3_G(N, odd_in_g(P))
U2_G(N, p_out_ga(N, P)) → ODD_IN_G(P)
ODD_IN_G(s(0)) → U4_G(true_in_)
ODD_IN_G(s(0)) → TRUE_IN_
ODD_IN_G(s(N)) → U5_G(N, even_in_a(P))
ODD_IN_G(s(N)) → EVEN_IN_A(P)
EVEN_IN_A(0) → U1_A(true_in_)
EVEN_IN_A(0) → TRUE_IN_
EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
EVEN_IN_A(N) → P_IN_AA(N, P)
U2_A(N, p_out_aa(N, P)) → U3_A(N, odd_in_a(P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(0)) → U4_A(true_in_)
ODD_IN_A(s(0)) → TRUE_IN_
ODD_IN_A(s(N)) → U5_A(N, even_in_a(P))
ODD_IN_A(s(N)) → EVEN_IN_A(P)

The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)
EVEN_IN_G(x1)  =  EVEN_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
ODD_IN_G(x1)  =  ODD_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
EVEN_IN_A(x1)  =  EVEN_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
P_IN_AA(x1, x2)  =  P_IN_AA
U3_A(x1, x2)  =  U3_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A
U4_A(x1)  =  U4_A(x1)
U5_A(x1, x2)  =  U5_A(x2)

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

(26) Obligation:

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

EVEN_IN_G(0) → U1_G(true_in_)
EVEN_IN_G(0) → TRUE_IN_
EVEN_IN_G(N) → U2_G(N, p_in_ga(N, P))
EVEN_IN_G(N) → P_IN_GA(N, P)
U2_G(N, p_out_ga(N, P)) → U3_G(N, odd_in_g(P))
U2_G(N, p_out_ga(N, P)) → ODD_IN_G(P)
ODD_IN_G(s(0)) → U4_G(true_in_)
ODD_IN_G(s(0)) → TRUE_IN_
ODD_IN_G(s(N)) → U5_G(N, even_in_a(P))
ODD_IN_G(s(N)) → EVEN_IN_A(P)
EVEN_IN_A(0) → U1_A(true_in_)
EVEN_IN_A(0) → TRUE_IN_
EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
EVEN_IN_A(N) → P_IN_AA(N, P)
U2_A(N, p_out_aa(N, P)) → U3_A(N, odd_in_a(P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(0)) → U4_A(true_in_)
ODD_IN_A(s(0)) → TRUE_IN_
ODD_IN_A(s(N)) → U5_A(N, even_in_a(P))
ODD_IN_A(s(N)) → EVEN_IN_A(P)

The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)
EVEN_IN_G(x1)  =  EVEN_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
ODD_IN_G(x1)  =  ODD_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
EVEN_IN_A(x1)  =  EVEN_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
P_IN_AA(x1, x2)  =  P_IN_AA
U3_A(x1, x2)  =  U3_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A
U4_A(x1)  =  U4_A(x1)
U5_A(x1, x2)  =  U5_A(x2)

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

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 17 less nodes.

(28) Obligation:

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

EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(N)) → EVEN_IN_A(P)

The TRS R consists of the following rules:

even_in_g(0) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → even_out_g(0)
even_in_g(N) → U2_g(N, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(N, p_out_ga(N, P)) → U3_g(N, odd_in_g(P))
odd_in_g(s(0)) → U4_g(true_in_)
U4_g(true_out_) → odd_out_g(s(0))
odd_in_g(s(N)) → U5_g(N, even_in_a(P))
even_in_a(0) → U1_a(true_in_)
U1_a(true_out_) → even_out_a(0)
even_in_a(N) → U2_a(N, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U2_a(N, p_out_aa(N, P)) → U3_a(N, odd_in_a(P))
odd_in_a(s(0)) → U4_a(true_in_)
U4_a(true_out_) → odd_out_a(s(0))
odd_in_a(s(N)) → U5_a(N, even_in_a(P))
U5_a(N, even_out_a(P)) → odd_out_a(s(N))
U3_a(N, odd_out_a(P)) → even_out_a(N)
U5_g(N, even_out_a(P)) → odd_out_g(s(N))
U3_g(N, odd_out_g(P)) → even_out_g(N)

The argument filtering Pi contains the following mapping:
even_in_g(x1)  =  even_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
even_out_g(x1)  =  even_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
odd_in_g(x1)  =  odd_in_g(x1)
U4_g(x1)  =  U4_g(x1)
odd_out_g(x1)  =  odd_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
even_in_a(x1)  =  even_in_a
U1_a(x1)  =  U1_a(x1)
even_out_a(x1)  =  even_out_a
U2_a(x1, x2)  =  U2_a(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U3_a(x1, x2)  =  U3_a(x2)
odd_in_a(x1)  =  odd_in_a
U4_a(x1)  =  U4_a(x1)
odd_out_a(x1)  =  odd_out_a
U5_a(x1, x2)  =  U5_a(x2)
EVEN_IN_A(x1)  =  EVEN_IN_A
U2_A(x1, x2)  =  U2_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

EVEN_IN_A(N) → U2_A(N, p_in_aa(N, P))
U2_A(N, p_out_aa(N, P)) → ODD_IN_A(P)
ODD_IN_A(s(N)) → EVEN_IN_A(P)

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:
0  =  0
s(x1)  =  s(x1)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
EVEN_IN_A(x1)  =  EVEN_IN_A
U2_A(x1, x2)  =  U2_A(x2)
ODD_IN_A(x1)  =  ODD_IN_A

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

EVEN_IN_A → U2_A(p_in_aa)
U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A

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.

(33) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule EVEN_IN_A → U2_A(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

EVEN_IN_A → U2_A(p_out_aa)

(34) Obligation:

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

U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A
EVEN_IN_A → U2_A(p_out_aa)

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.

(35) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(36) Obligation:

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

U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A
EVEN_IN_A → U2_A(p_out_aa)

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

p_in_aa

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

(37) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

p_in_aa

(38) Obligation:

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

U2_A(p_out_aa) → ODD_IN_A
ODD_IN_A → EVEN_IN_A
EVEN_IN_A → U2_A(p_out_aa)

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

(39) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ODD_IN_A evaluates to t =ODD_IN_A

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



Rewriting sequence

ODD_IN_A → EVEN_IN_A
with rule ODD_IN_A → EVEN_IN_A at position [] and matcher [ ]

EVEN_IN_A → U2_A(p_out_aa)
with rule EVEN_IN_A → U2_A(p_out_aa) at position [] and matcher [ ]

U2_A(p_out_aa) → ODD_IN_A
with rule U2_A(p_out_aa) → ODD_IN_A

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(40) FALSE