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

0 Prolog
↳1 CutEliminatorProof (⇐)
↳2 Prolog
  ↳3 PrologToPiTRSProof (⇐)
    ↳4 PiTRS
    ↳5 DependencyPairsProof (⇔)
    ↳6 PiDP
    ↳7 DependencyGraphProof (⇔)
    ↳8 PiDP
    ↳9 UsableRulesProof (⇔)
    ↳10 PiDP
    ↳11 PiDPToQDPProof (⇐)
    ↳12 QDP
    ↳13 UsableRulesReductionPairsProof (⇔)
    ↳14 QDP
    ↳15 MRRProof (⇔)
    ↳16 QDP
    ↳17 UsableRulesProof (⇔)
    ↳18 QDP
    ↳19 QReductionProof (⇔)
    ↳20 QDP
    ↳21 Rewriting (⇔)
    ↳22 QDP
    ↳23 UsableRulesProof (⇔)
    ↳24 QDP
    ↳25 QReductionProof (⇔)
    ↳26 QDP
    ↳27 Narrowing (⇐)
    ↳28 QDP
    ↳29 UsableRulesProof (⇔)
    ↳30 QDP
    ↳31 QReductionProof (⇔)
    ↳32 QDP
    ↳33 Instantiation (⇔)
    ↳34 QDP
    ↳35 Instantiation (⇔)
    ↳36 QDP
    ↳37 NonTerminationProof (⇔)
    ↳38 FALSE
  ↳39 PrologToPiTRSProof (⇐)
    ↳40 PiTRS
    ↳41 DependencyPairsProof (⇔)
    ↳42 PiDP
    ↳43 DependencyGraphProof (⇔)
    ↳44 PiDP
    ↳45 UsableRulesProof (⇔)
    ↳46 PiDP
    ↳47 PiDPToQDPProof (⇐)
    ↳48 QDP
    ↳49 Narrowing (⇐)
    ↳50 QDP
    ↳51 UsableRulesProof (⇔)
    ↳52 QDP
    ↳53 QReductionProof (⇔)
    ↳54 QDP
    ↳55 Narrowing (⇐)
    ↳56 QDP
    ↳57 DependencyGraphProof (⇔)
    ↳58 QDP
    ↳59 UsableRulesProof (⇔)
    ↳60 QDP
    ↳61 QReductionProof (⇔)
    ↳62 QDP
    ↳63 Instantiation (⇔)
    ↳64 QDP
      ↳65 QDPOrderProof (⇔)
        ↳66 QDP
        ↳67 DependencyGraphProof (⇔)
        ↳68 QDP
          ↳69 Instantiation (⇔)
            ↳70 QDP
          ↳71 Instantiation (⇔)
            ↳72 QDP
            ↳73 NonTerminationProof (⇔)
            ↳74 FALSE
      ↳75 QDPOrderProof (⇔)
        ↳76 QDP

(0) Obligation:

Clauses:

q(X) :- ','(not_zero(X), ','(p(X, Y), q(Y))).
p(0, 0).
p(s(X), X).
zero(0).
not_zero(X) :- ','(zero(X), ','(!, failure(a))).
not_zero(X1).
failure(b).

Queries:

q(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

q(X) :- ','(not_zero(X), ','(p(X, Y), q(Y))).
p(0, 0).
p(s(X), X).
zero(0).
not_zero(X) :- ','(zero(X), failure(a)).
not_zero(X1).
failure(b).

Queries:

q(g).

(3) PrologToPiTRSProof (SOUND transformation)

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

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g
U5_g(x1, x2)  =  U5_g(x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g
U5_g(x1, x2)  =  U5_g(x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g

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

Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
Q_IN_G(X) → NOT_ZERO_IN_G(X)
NOT_ZERO_IN_G(X) → U4_G(X, zero_in_g(X))
NOT_ZERO_IN_G(X) → ZERO_IN_G(X)
U4_G(X, zero_out_g(X)) → U5_G(X, failure_in_g(a))
U4_G(X, zero_out_g(X)) → FAILURE_IN_G(a)
U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U1_G(X, not_zero_out_g(X)) → P_IN_GA(X, Y)
U2_G(X, p_out_ga(X, Y)) → U3_G(X, q_in_g(Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)

The TRS R consists of the following rules:

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g
U5_g(x1, x2)  =  U5_g(x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
NOT_ZERO_IN_G(x1)  =  NOT_ZERO_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x2)
ZERO_IN_G(x1)  =  ZERO_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x2)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x2)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U3_G(x1, x2)  =  U3_G(x2)

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

(6) Obligation:

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

Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
Q_IN_G(X) → NOT_ZERO_IN_G(X)
NOT_ZERO_IN_G(X) → U4_G(X, zero_in_g(X))
NOT_ZERO_IN_G(X) → ZERO_IN_G(X)
U4_G(X, zero_out_g(X)) → U5_G(X, failure_in_g(a))
U4_G(X, zero_out_g(X)) → FAILURE_IN_G(a)
U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U1_G(X, not_zero_out_g(X)) → P_IN_GA(X, Y)
U2_G(X, p_out_ga(X, Y)) → U3_G(X, q_in_g(Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)

The TRS R consists of the following rules:

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g
U5_g(x1, x2)  =  U5_g(x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
NOT_ZERO_IN_G(x1)  =  NOT_ZERO_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x2)
ZERO_IN_G(x1)  =  ZERO_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x2)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x2)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U3_G(x1, x2)  =  U3_G(x2)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g
U5_g(x1, x2)  =  U5_g(x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x2)

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

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
zero_in_g(0) → zero_out_g(0)

The argument filtering Pi contains the following mapping:
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g
U5_g(x1, x2)  =  U5_g(x2)
failure_in_g(x1)  =  failure_in_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_out_g
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x2)

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)
p_in_ga(s(X)) → p_out_ga(X)
not_zero_in_g(X) → U4_g(zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g
U4_g(zero_out_g) → U5_g(failure_in_g(a))
zero_in_g(0) → zero_out_g

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0)
zero_in_g(x0)

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

(13) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

p_in_ga(s(X)) → p_out_ga(X)
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(Q_IN_G(x1)) = 2·x1   
POL(U1_G(x1, x2)) = x1 + x2   
POL(U2_G(x1)) = x1   
POL(U4_g(x1)) = x1   
POL(U5_g(x1)) = x1   
POL(a) = 0   
POL(failure_in_g(x1)) = x1   
POL(not_zero_in_g(x1)) = x1   
POL(not_zero_out_g) = 0   
POL(p_in_ga(x1)) = x1   
POL(p_out_ga(x1)) = 2·x1   
POL(s(x1)) = 1 + 2·x1   
POL(zero_in_g(x1)) = x1   
POL(zero_out_g) = 0   

(14) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

not_zero_in_g(X) → U4_g(zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g
zero_in_g(0) → zero_out_g
U4_g(zero_out_g) → U5_g(failure_in_g(a))
p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0)
zero_in_g(x0)

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

(15) 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 rules of the TRS R:

not_zero_in_g(X) → U4_g(zero_in_g(X))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(Q_IN_G(x1)) = 1 + 2·x1   
POL(U1_G(x1, x2)) = x1 + x2   
POL(U2_G(x1)) = 1 + x1   
POL(U4_g(x1)) = x1   
POL(U5_g(x1)) = x1   
POL(a) = 0   
POL(failure_in_g(x1)) = x1   
POL(not_zero_in_g(x1)) = 1 + x1   
POL(not_zero_out_g) = 1   
POL(p_in_ga(x1)) = x1   
POL(p_out_ga(x1)) = 2·x1   
POL(zero_in_g(x1)) = x1   
POL(zero_out_g) = 0   

(16) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

not_zero_in_g(X1) → not_zero_out_g
zero_in_g(0) → zero_out_g
U4_g(zero_out_g) → U5_g(failure_in_g(a))
p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0)
zero_in_g(x0)

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:

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

not_zero_in_g(X1) → not_zero_out_g
p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0)
zero_in_g(x0)

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].

U4_g(x0)
zero_in_g(x0)

(20) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

not_zero_in_g(X1) → not_zero_out_g
p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)

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

(21) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule Q_IN_G(X) → U1_G(X, not_zero_in_g(X)) at position [1] we obtained the following new rules [LPAR04]:

Q_IN_G(X) → U1_G(X, not_zero_out_g)

(22) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_out_g)

The TRS R consists of the following rules:

not_zero_in_g(X1) → not_zero_out_g
p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)

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

(23) 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.

(24) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_out_g)

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)

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

(25) 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].

not_zero_in_g(x0)

(26) Obligation:

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

U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X))
U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_out_g)

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)

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

(27) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U1_G(X, not_zero_out_g) → U2_G(p_in_ga(X)) at position [0] we obtained the following new rules [LPAR04]:

U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))

(28) Obligation:

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

U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_out_g)
U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)

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

(29) 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.

(30) Obligation:

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

U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_out_g)
U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))

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

p_in_ga(x0)

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

(31) 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_ga(x0)

(32) Obligation:

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

U2_G(p_out_ga(Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_out_g)
U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))

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

(33) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_G(p_out_ga(Y)) → Q_IN_G(Y) we obtained the following new rules [LPAR04]:

U2_G(p_out_ga(0)) → Q_IN_G(0)

(34) Obligation:

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

Q_IN_G(X) → U1_G(X, not_zero_out_g)
U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))
U2_G(p_out_ga(0)) → Q_IN_G(0)

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

(35) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule Q_IN_G(X) → U1_G(X, not_zero_out_g) we obtained the following new rules [LPAR04]:

Q_IN_G(0) → U1_G(0, not_zero_out_g)

(36) Obligation:

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

U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))
U2_G(p_out_ga(0)) → Q_IN_G(0)
Q_IN_G(0) → U1_G(0, not_zero_out_g)

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

(37) 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 = U2_G(p_out_ga(0)) evaluates to t =U2_G(p_out_ga(0))

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



Rewriting sequence

U2_G(p_out_ga(0)) → Q_IN_G(0)
with rule U2_G(p_out_ga(0)) → Q_IN_G(0) at position [] and matcher [ ]

Q_IN_G(0) → U1_G(0, not_zero_out_g)
with rule Q_IN_G(0) → U1_G(0, not_zero_out_g) at position [] and matcher [ ]

U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))
with rule U1_G(0, not_zero_out_g) → U2_G(p_out_ga(0))

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.



(38) FALSE

(39) PrologToPiTRSProof (SOUND transformation)

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

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x1, x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(40) Obligation:

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

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x1, x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g(x1)

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

Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
Q_IN_G(X) → NOT_ZERO_IN_G(X)
NOT_ZERO_IN_G(X) → U4_G(X, zero_in_g(X))
NOT_ZERO_IN_G(X) → ZERO_IN_G(X)
U4_G(X, zero_out_g(X)) → U5_G(X, failure_in_g(a))
U4_G(X, zero_out_g(X)) → FAILURE_IN_G(a)
U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U1_G(X, not_zero_out_g(X)) → P_IN_GA(X, Y)
U2_G(X, p_out_ga(X, Y)) → U3_G(X, q_in_g(Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)

The TRS R consists of the following rules:

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x1, x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g(x1)
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
NOT_ZERO_IN_G(x1)  =  NOT_ZERO_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x1, x2)
ZERO_IN_G(x1)  =  ZERO_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
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)

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

(42) Obligation:

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

Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
Q_IN_G(X) → NOT_ZERO_IN_G(X)
NOT_ZERO_IN_G(X) → U4_G(X, zero_in_g(X))
NOT_ZERO_IN_G(X) → ZERO_IN_G(X)
U4_G(X, zero_out_g(X)) → U5_G(X, failure_in_g(a))
U4_G(X, zero_out_g(X)) → FAILURE_IN_G(a)
U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U1_G(X, not_zero_out_g(X)) → P_IN_GA(X, Y)
U2_G(X, p_out_ga(X, Y)) → U3_G(X, q_in_g(Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)

The TRS R consists of the following rules:

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x1, x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g(x1)
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
NOT_ZERO_IN_G(x1)  =  NOT_ZERO_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x1, x2)
ZERO_IN_G(x1)  =  ZERO_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
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)

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

(43) DependencyGraphProof (EQUIVALENT transformation)

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

(44) Obligation:

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

U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

q_in_g(X) → U1_g(X, not_zero_in_g(X))
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U5_g(X, failure_out_g(a)) → not_zero_out_g(X)
not_zero_in_g(X1) → not_zero_out_g(X1)
U1_g(X, not_zero_out_g(X)) → U2_g(X, p_in_ga(X, Y))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_g(X, p_out_ga(X, Y)) → U3_g(X, q_in_g(Y))
U3_g(X, q_out_g(Y)) → q_out_g(X)

The argument filtering Pi contains the following mapping:
q_in_g(x1)  =  q_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x1, x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_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)
q_out_g(x1)  =  q_out_g(x1)
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x1, x2)

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:

U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X, Y))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
zero_in_g(0) → zero_out_g(0)

The argument filtering Pi contains the following mapping:
not_zero_in_g(x1)  =  not_zero_in_g(x1)
U4_g(x1, x2)  =  U4_g(x1, x2)
zero_in_g(x1)  =  zero_in_g(x1)
0  =  0
zero_out_g(x1)  =  zero_out_g(x1)
U5_g(x1, x2)  =  U5_g(x1, x2)
failure_in_g(x1)  =  failure_in_g(x1)
a  =  a
not_zero_out_g(x1)  =  not_zero_out_g(x1)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
Q_IN_G(x1)  =  Q_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x1, x2)

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:

U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
zero_in_g(0) → zero_out_g(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(49) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U1_G(X, not_zero_out_g(X)) → U2_G(X, p_in_ga(X)) at position [1] we obtained the following new rules [LPAR04]:

U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

(50) Obligation:

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

U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))
zero_in_g(0) → zero_out_g(0)

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(51) 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.

(52) Obligation:

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

U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

The TRS R consists of the following rules:

not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))

The set Q consists of the following terms:

p_in_ga(x0)
not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(53) 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_ga(x0)

(54) Obligation:

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

U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
Q_IN_G(X) → U1_G(X, not_zero_in_g(X))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

The TRS R consists of the following rules:

not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))

The set Q consists of the following terms:

not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(55) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule Q_IN_G(X) → U1_G(X, not_zero_in_g(X)) at position [1] we obtained the following new rules [LPAR04]:

Q_IN_G(x0) → U1_G(x0, U4_g(x0, zero_in_g(x0)))
Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))

(56) Obligation:

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

U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))
Q_IN_G(x0) → U1_G(x0, U4_g(x0, zero_in_g(x0)))
Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))

The TRS R consists of the following rules:

not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))

The set Q consists of the following terms:

not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(57) DependencyGraphProof (EQUIVALENT transformation)

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

(58) Obligation:

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

Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

The TRS R consists of the following rules:

not_zero_in_g(X) → U4_g(X, zero_in_g(X))
not_zero_in_g(X1) → not_zero_out_g(X1)
zero_in_g(0) → zero_out_g(0)
U4_g(X, zero_out_g(X)) → U5_g(X, failure_in_g(a))

The set Q consists of the following terms:

not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(59) 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.

(60) Obligation:

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

Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

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

not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

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

(61) 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].

not_zero_in_g(x0)
U4_g(x0, x1)
zero_in_g(x0)

(62) Obligation:

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

Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y)
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))

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

(63) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_G(X, p_out_ga(X, Y)) → Q_IN_G(Y) we obtained the following new rules [LPAR04]:

U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)
U2_G(s(z0), p_out_ga(s(z0), z0)) → Q_IN_G(z0)

(64) Obligation:

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

Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))
U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)
U2_G(s(z0), p_out_ga(s(z0), z0)) → Q_IN_G(z0)

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

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U2_G(s(z0), p_out_ga(s(z0), z0)) → Q_IN_G(z0)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(Q_IN_G(x1)) = x1   
POL(U1_G(x1, x2)) = x1   
POL(U2_G(x1, x2)) = x2   
POL(not_zero_out_g(x1)) = 0   
POL(p_out_ga(x1, x2)) = x1   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented: none

(66) Obligation:

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

Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))
U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)

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

(67) DependencyGraphProof (EQUIVALENT transformation)

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

(68) Obligation:

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

U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)
Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))

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

(69) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0)) we obtained the following new rules [LPAR04]:

Q_IN_G(0) → U1_G(0, not_zero_out_g(0))

(70) Obligation:

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

U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)
Q_IN_G(0) → U1_G(0, not_zero_out_g(0))

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

(71) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0)) we obtained the following new rules [LPAR04]:

Q_IN_G(0) → U1_G(0, not_zero_out_g(0))

(72) Obligation:

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

U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)
Q_IN_G(0) → U1_G(0, not_zero_out_g(0))

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

(73) 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 = U2_G(0, p_out_ga(0, 0)) evaluates to t =U2_G(0, p_out_ga(0, 0))

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



Rewriting sequence

U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)
with rule U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0) at position [] and matcher [ ]

Q_IN_G(0) → U1_G(0, not_zero_out_g(0))
with rule Q_IN_G(0) → U1_G(0, not_zero_out_g(0)) at position [] and matcher [ ]

U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
with rule U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))

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.



(74) FALSE

(75) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U2_G(s(z0), p_out_ga(s(z0), z0)) → Q_IN_G(z0)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(Q_IN_G(x1)) = 1 +
[1,0]
·x1

POL(U1_G(x1, x2)) = 1 +
[1,0]
·x1 +
[0,0]
·x2

POL(not_zero_out_g(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(0) =
/0\
\0/

POL(U2_G(x1, x2)) = 1 +
[1,0]
·x1 +
[0,0]
·x2

POL(p_out_ga(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(s(x1)) =
/1\
\0/
 +
/10\
\00/
·x1

The following usable rules [FROCOS05] were oriented: none

(76) Obligation:

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

Q_IN_G(x0) → U1_G(x0, not_zero_out_g(x0))
U1_G(0, not_zero_out_g(0)) → U2_G(0, p_out_ga(0, 0))
U1_G(s(x0), not_zero_out_g(s(x0))) → U2_G(s(x0), p_out_ga(s(x0), x0))
U2_G(0, p_out_ga(0, 0)) → Q_IN_G(0)

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