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

(0) Obligation:

Clauses:

h(X) :- ','(f(X), g(X)).
f(c(0, X1)) :- !.
f(c(X, Y)) :- ','(p(X, P), f(c(P, s(Y)))).
g(c(X2, 0)) :- !.
g(c(X, Y)) :- ','(p(Y, P), g(c(s(X), P))).
p(0, 0).
p(s(X), X).

Queries:

h(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

h(X) :- ','(f(X), g(X)).
f(c(0, X1)) :- true.
f(c(X, Y)) :- ','(p(X, P), f(c(P, s(Y)))).
g(c(X2, 0)) :- true.
g(c(X, Y)) :- ','(p(Y, P), g(c(s(X), P))).
p(0, 0).
p(s(X), X).

Queries:

h(g).

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

h(X) :- ','(f(X), g(X)).
f(c(0, X1)) :- true.
f(c(X, Y)) :- ','(p(X, P), f(c(P, s(Y)))).
g(c(X2, 0)) :- true.
g(c(X, Y)) :- ','(p(Y, P), g(c(s(X), P))).
p(0, 0).
p(s(X), X).
true.

Queries:

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

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x1, x2, x3)
U2_g(x1, x2)  =  U2_g(x1, x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x1, x2)
g_out_g(x1)  =  g_out_g(x1)
U7_g(x1, x2, x3)  =  U7_g(x1, x2, x3)
U8_g(x1, x2, x3)  =  U8_g(x1, x2, x3)
h_out_g(x1)  =  h_out_g(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x1, x2, x3)
U2_g(x1, x2)  =  U2_g(x1, x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x1, x2)
g_out_g(x1)  =  g_out_g(x1)
U7_g(x1, x2, x3)  =  U7_g(x1, x2, x3)
U8_g(x1, x2, x3)  =  U8_g(x1, x2, x3)
h_out_g(x1)  =  h_out_g(x1)

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

H_IN_G(X) → U1_G(X, f_in_g(X))
H_IN_G(X) → F_IN_G(X)
F_IN_G(c(0, X1)) → U3_G(X1, true_in_)
F_IN_G(c(0, X1)) → TRUE_IN_
F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
F_IN_G(c(X, Y)) → P_IN_GA(X, P)
U4_G(X, Y, p_out_ga(X, P)) → U5_G(X, Y, f_in_g(c(P, s(Y))))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
U1_G(X, f_out_g(X)) → U2_G(X, g_in_g(X))
U1_G(X, f_out_g(X)) → G_IN_G(X)
G_IN_G(c(X2, 0)) → U6_G(X2, true_in_)
G_IN_G(c(X2, 0)) → TRUE_IN_
G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
G_IN_G(c(X, Y)) → P_IN_GA(Y, P)
U7_G(X, Y, p_out_ga(Y, P)) → U8_G(X, Y, g_in_g(c(s(X), P)))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x1, x2, x3)
U2_g(x1, x2)  =  U2_g(x1, x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x1, x2)
g_out_g(x1)  =  g_out_g(x1)
U7_g(x1, x2, x3)  =  U7_g(x1, x2, x3)
U8_g(x1, x2, x3)  =  U8_g(x1, x2, x3)
h_out_g(x1)  =  h_out_g(x1)
H_IN_G(x1)  =  H_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
F_IN_G(x1)  =  F_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
TRUE_IN_  =  TRUE_IN_
U4_G(x1, x2, x3)  =  U4_G(x1, x2, x3)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U5_G(x1, x2, x3)  =  U5_G(x1, x2, x3)
U2_G(x1, x2)  =  U2_G(x1, x2)
G_IN_G(x1)  =  G_IN_G(x1)
U6_G(x1, x2)  =  U6_G(x1, x2)
U7_G(x1, x2, x3)  =  U7_G(x1, x2, x3)
U8_G(x1, x2, x3)  =  U8_G(x1, x2, x3)

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

(8) Obligation:

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

H_IN_G(X) → U1_G(X, f_in_g(X))
H_IN_G(X) → F_IN_G(X)
F_IN_G(c(0, X1)) → U3_G(X1, true_in_)
F_IN_G(c(0, X1)) → TRUE_IN_
F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
F_IN_G(c(X, Y)) → P_IN_GA(X, P)
U4_G(X, Y, p_out_ga(X, P)) → U5_G(X, Y, f_in_g(c(P, s(Y))))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
U1_G(X, f_out_g(X)) → U2_G(X, g_in_g(X))
U1_G(X, f_out_g(X)) → G_IN_G(X)
G_IN_G(c(X2, 0)) → U6_G(X2, true_in_)
G_IN_G(c(X2, 0)) → TRUE_IN_
G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
G_IN_G(c(X, Y)) → P_IN_GA(Y, P)
U7_G(X, Y, p_out_ga(Y, P)) → U8_G(X, Y, g_in_g(c(s(X), P)))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x1, x2, x3)
U2_g(x1, x2)  =  U2_g(x1, x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x1, x2)
g_out_g(x1)  =  g_out_g(x1)
U7_g(x1, x2, x3)  =  U7_g(x1, x2, x3)
U8_g(x1, x2, x3)  =  U8_g(x1, x2, x3)
h_out_g(x1)  =  h_out_g(x1)
H_IN_G(x1)  =  H_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
F_IN_G(x1)  =  F_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
TRUE_IN_  =  TRUE_IN_
U4_G(x1, x2, x3)  =  U4_G(x1, x2, x3)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U5_G(x1, x2, x3)  =  U5_G(x1, x2, x3)
U2_G(x1, x2)  =  U2_G(x1, x2)
G_IN_G(x1)  =  G_IN_G(x1)
U6_G(x1, x2)  =  U6_G(x1, x2)
U7_G(x1, x2, x3)  =  U7_G(x1, x2, x3)
U8_G(x1, x2, x3)  =  U8_G(x1, x2, x3)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Complex Obligation (AND)

(11) Obligation:

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

G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x1, x2, x3)
U2_g(x1, x2)  =  U2_g(x1, x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x1, x2)
g_out_g(x1)  =  g_out_g(x1)
U7_g(x1, x2, x3)  =  U7_g(x1, x2, x3)
U8_g(x1, x2, x3)  =  U8_g(x1, x2, x3)
h_out_g(x1)  =  h_out_g(x1)
G_IN_G(x1)  =  G_IN_G(x1)
U7_G(x1, x2, x3)  =  U7_G(x1, x2, x3)

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:

G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

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)

The argument filtering Pi contains the following mapping:
c(x1, x2)  =  c(x1, x2)
0  =  0
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
G_IN_G(x1)  =  G_IN_G(x1)
U7_G(x1, x2, x3)  =  U7_G(x1, x2, x3)

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:

G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(16) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(z0), z2)) → U7_G(s(z0), z2, p_in_ga(z2))

(17) Obligation:

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

U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))
G_IN_G(c(s(z0), z2)) → U7_G(s(z0), z2, p_in_ga(z2))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(18) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y)) at position [2] we obtained the following new rules [LPAR04]:

G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, s(x0), p_out_ga(s(x0), x0))

(19) Obligation:

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

U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, 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)

The set Q consists of the following terms:

p_in_ga(x0)

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

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

(21) Obligation:

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

U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, s(x0), p_out_ga(s(x0), x0))

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

p_in_ga(x0)

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

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

(23) Obligation:

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

U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, s(x0), p_out_ga(s(x0), x0))

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

(24) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P)) we obtained the following new rules [LPAR04]:

U7_G(z0, 0, p_out_ga(0, 0)) → G_IN_G(c(s(z0), 0))
U7_G(z0, s(z1), p_out_ga(s(z1), z1)) → G_IN_G(c(s(z0), z1))

(25) Obligation:

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

G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, s(x0), p_out_ga(s(x0), x0))
U7_G(z0, 0, p_out_ga(0, 0)) → G_IN_G(c(s(z0), 0))
U7_G(z0, s(z1), p_out_ga(s(z1), z1)) → G_IN_G(c(s(z0), z1))

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

(26) DependencyGraphProof (EQUIVALENT transformation)

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

(27) Complex Obligation (AND)

(28) Obligation:

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

U7_G(z0, 0, p_out_ga(0, 0)) → G_IN_G(c(s(z0), 0))
G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0))

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

(29) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(z0), 0)) → U7_G(s(z0), 0, p_out_ga(0, 0))

(30) Obligation:

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

U7_G(z0, 0, p_out_ga(0, 0)) → G_IN_G(c(s(z0), 0))
G_IN_G(c(s(z0), 0)) → U7_G(s(z0), 0, p_out_ga(0, 0))

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

(31) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(y0, 0)) → U7_G(y0, 0, p_out_ga(0, 0)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(z0), 0)) → U7_G(s(z0), 0, p_out_ga(0, 0))

(32) Obligation:

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

U7_G(z0, 0, p_out_ga(0, 0)) → G_IN_G(c(s(z0), 0))
G_IN_G(c(s(z0), 0)) → U7_G(s(z0), 0, p_out_ga(0, 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 U7_G(z0, 0, p_out_ga(0, 0)) → G_IN_G(c(s(z0), 0)) we obtained the following new rules [LPAR04]:

U7_G(s(z0), 0, p_out_ga(0, 0)) → G_IN_G(c(s(s(z0)), 0))

(34) Obligation:

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

G_IN_G(c(s(z0), 0)) → U7_G(s(z0), 0, p_out_ga(0, 0))
U7_G(s(z0), 0, p_out_ga(0, 0)) → G_IN_G(c(s(s(z0)), 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 G_IN_G(c(s(z0), 0)) → U7_G(s(z0), 0, p_out_ga(0, 0)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(s(z0)), 0)) → U7_G(s(s(z0)), 0, p_out_ga(0, 0))

(36) Obligation:

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

U7_G(s(z0), 0, p_out_ga(0, 0)) → G_IN_G(c(s(s(z0)), 0))
G_IN_G(c(s(s(z0)), 0)) → U7_G(s(s(z0)), 0, p_out_ga(0, 0))

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 = G_IN_G(c(s(s(z0')), 0)) evaluates to t =G_IN_G(c(s(s(s(z0'))), 0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [z0' / s(z0')]
• Semiunifier: [ ]

---

Rewriting sequence

G_IN_G(c(s(s(z0')), 0)) → U7_G(s(s(z0')), 0, p_out_ga(0, 0))
with rule G_IN_G(c(s(s(z0'')), 0)) → U7_G(s(s(z0'')), 0, p_out_ga(0, 0)) at position [] and matcher [z0'' / z0']

U7_G(s(s(z0')), 0, p_out_ga(0, 0)) → G_IN_G(c(s(s(s(z0'))), 0))
with rule U7_G(s(z0), 0, p_out_ga(0, 0)) → G_IN_G(c(s(s(z0)), 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) Obligation:

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

G_IN_G(c(y0, s(x0))) → U7_G(y0, s(x0), p_out_ga(s(x0), x0))
U7_G(z0, s(z1), p_out_ga(s(z1), z1)) → G_IN_G(c(s(z0), z1))

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

(40) MRRProof (EQUIVALENT transformation)

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

G_IN_G(c(y0, s(x0))) → U7_G(y0, s(x0), p_out_ga(s(x0), x0))
U7_G(z0, s(z1), p_out_ga(s(z1), z1)) → G_IN_G(c(s(z0), z1))

Used ordering: Polynomial interpretation [POLO]:

POL(G_IN_G(x₁)) = 2·x₁   
POL(U7_G(x₁, x₂, x₃)) = 2·x₁ + 2·x₂ + x₃   
POL(c(x₁, x₂)) = x₁ + 2·x₂   
POL(p_out_ga(x₁, x₂)) = x₁ + x₂   
POL(s(x₁)) = 1 + x₁   

(41) Obligation:

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

(42) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(43) TRUE

(44) Obligation:

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

F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x1, x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x1, x2, x3)
U2_g(x1, x2)  =  U2_g(x1, x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x1, x2)
g_out_g(x1)  =  g_out_g(x1)
U7_g(x1, x2, x3)  =  U7_g(x1, x2, x3)
U8_g(x1, x2, x3)  =  U8_g(x1, x2, x3)
h_out_g(x1)  =  h_out_g(x1)
F_IN_G(x1)  =  F_IN_G(x1)
U4_G(x1, x2, x3)  =  U4_G(x1, x2, x3)

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:

F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))

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)

The argument filtering Pi contains the following mapping:
c(x1, x2)  =  c(x1, x2)
0  =  0
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
F_IN_G(x1)  =  F_IN_G(x1)
U4_G(x1, x2, x3)  =  U4_G(x1, x2, x3)

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:

F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(49) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X)) we obtained the following new rules [LPAR04]:

F_IN_G(c(z2, s(z1))) → U4_G(z2, s(z1), p_in_ga(z2))

(50) Obligation:

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

U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(z2, s(z1))) → U4_G(z2, s(z1), p_in_ga(z2))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(51) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X)) at position [2] we obtained the following new rules [LPAR04]:

F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0))
F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, p_out_ga(s(x0), x0))

(52) Obligation:

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

U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0))
F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, 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)

The set Q consists of the following terms:

p_in_ga(x0)

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

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

(54) Obligation:

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

U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0))
F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, p_out_ga(s(x0), x0))

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

p_in_ga(x0)

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

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

(56) Obligation:

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

U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0))
F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, p_out_ga(s(x0), x0))

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

(57) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y))) we obtained the following new rules [LPAR04]:

U4_G(0, z0, p_out_ga(0, 0)) → F_IN_G(c(0, s(z0)))
U4_G(s(z0), z1, p_out_ga(s(z0), z0)) → F_IN_G(c(z0, s(z1)))

(58) Obligation:

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

F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0))
F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, p_out_ga(s(x0), x0))
U4_G(0, z0, p_out_ga(0, 0)) → F_IN_G(c(0, s(z0)))
U4_G(s(z0), z1, p_out_ga(s(z0), z0)) → F_IN_G(c(z0, s(z1)))

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

(59) DependencyGraphProof (EQUIVALENT transformation)

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

(60) Complex Obligation (AND)

(61) Obligation:

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

U4_G(0, z0, p_out_ga(0, 0)) → F_IN_G(c(0, s(z0)))
F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0))

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

(62) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0)) we obtained the following new rules [LPAR04]:

F_IN_G(c(0, s(z0))) → U4_G(0, s(z0), p_out_ga(0, 0))

(63) Obligation:

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

U4_G(0, z0, p_out_ga(0, 0)) → F_IN_G(c(0, s(z0)))
F_IN_G(c(0, s(z0))) → U4_G(0, s(z0), p_out_ga(0, 0))

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

(64) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(0, y1)) → U4_G(0, y1, p_out_ga(0, 0)) we obtained the following new rules [LPAR04]:

F_IN_G(c(0, s(z0))) → U4_G(0, s(z0), p_out_ga(0, 0))

(65) Obligation:

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

U4_G(0, z0, p_out_ga(0, 0)) → F_IN_G(c(0, s(z0)))
F_IN_G(c(0, s(z0))) → U4_G(0, s(z0), p_out_ga(0, 0))

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

(66) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(0, z0, p_out_ga(0, 0)) → F_IN_G(c(0, s(z0))) we obtained the following new rules [LPAR04]:

U4_G(0, s(z0), p_out_ga(0, 0)) → F_IN_G(c(0, s(s(z0))))

(67) Obligation:

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

F_IN_G(c(0, s(z0))) → U4_G(0, s(z0), p_out_ga(0, 0))
U4_G(0, s(z0), p_out_ga(0, 0)) → F_IN_G(c(0, s(s(z0))))

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

(68) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(0, s(z0))) → U4_G(0, s(z0), p_out_ga(0, 0)) we obtained the following new rules [LPAR04]:

F_IN_G(c(0, s(s(z0)))) → U4_G(0, s(s(z0)), p_out_ga(0, 0))

(69) Obligation:

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

U4_G(0, s(z0), p_out_ga(0, 0)) → F_IN_G(c(0, s(s(z0))))
F_IN_G(c(0, s(s(z0)))) → U4_G(0, s(s(z0)), p_out_ga(0, 0))

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

(70) 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 = F_IN_G(c(0, s(s(z0')))) evaluates to t =F_IN_G(c(0, s(s(s(z0')))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [z0' / s(z0')]
• Semiunifier: [ ]

---

Rewriting sequence

F_IN_G(c(0, s(s(z0')))) → U4_G(0, s(s(z0')), p_out_ga(0, 0))
with rule F_IN_G(c(0, s(s(z0'')))) → U4_G(0, s(s(z0'')), p_out_ga(0, 0)) at position [] and matcher [z0'' / z0']

U4_G(0, s(s(z0')), p_out_ga(0, 0)) → F_IN_G(c(0, s(s(s(z0')))))
with rule U4_G(0, s(z0), p_out_ga(0, 0)) → F_IN_G(c(0, s(s(z0))))

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.

(71) FALSE

(72) Obligation:

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

F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, p_out_ga(s(x0), x0))
U4_G(s(z0), z1, p_out_ga(s(z0), z0)) → F_IN_G(c(z0, s(z1)))

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

(73) MRRProof (EQUIVALENT transformation)

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

F_IN_G(c(s(x0), y1)) → U4_G(s(x0), y1, p_out_ga(s(x0), x0))
U4_G(s(z0), z1, p_out_ga(s(z0), z0)) → F_IN_G(c(z0, s(z1)))

Used ordering: Polynomial interpretation [POLO]:

POL(F_IN_G(x₁)) = 1 + 2·x₁   
POL(U4_G(x₁, x₂, x₃)) = 2 + x₁ + 2·x₂ + x₃   
POL(c(x₁, x₂)) = 1 + 2·x₁ + x₂   
POL(p_out_ga(x₁, x₂)) = 2 + x₁ + 2·x₂   
POL(s(x₁)) = 2 + x₁   

(74) Obligation:

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

(75) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(76) TRUE

(77) PrologToPiTRSProof (SOUND transformation)

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

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g
U4_g(x1, x2, x3)  =  U4_g(x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x3)
U2_g(x1, x2)  =  U2_g(x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x2)
g_out_g(x1)  =  g_out_g
U7_g(x1, x2, x3)  =  U7_g(x1, x3)
U8_g(x1, x2, x3)  =  U8_g(x3)
h_out_g(x1)  =  h_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(78) Obligation:

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

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g
U4_g(x1, x2, x3)  =  U4_g(x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x3)
U2_g(x1, x2)  =  U2_g(x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x2)
g_out_g(x1)  =  g_out_g
U7_g(x1, x2, x3)  =  U7_g(x1, x3)
U8_g(x1, x2, x3)  =  U8_g(x3)
h_out_g(x1)  =  h_out_g

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

H_IN_G(X) → U1_G(X, f_in_g(X))
H_IN_G(X) → F_IN_G(X)
F_IN_G(c(0, X1)) → U3_G(X1, true_in_)
F_IN_G(c(0, X1)) → TRUE_IN_
F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
F_IN_G(c(X, Y)) → P_IN_GA(X, P)
U4_G(X, Y, p_out_ga(X, P)) → U5_G(X, Y, f_in_g(c(P, s(Y))))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
U1_G(X, f_out_g(X)) → U2_G(X, g_in_g(X))
U1_G(X, f_out_g(X)) → G_IN_G(X)
G_IN_G(c(X2, 0)) → U6_G(X2, true_in_)
G_IN_G(c(X2, 0)) → TRUE_IN_
G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
G_IN_G(c(X, Y)) → P_IN_GA(Y, P)
U7_G(X, Y, p_out_ga(Y, P)) → U8_G(X, Y, g_in_g(c(s(X), P)))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g
U4_g(x1, x2, x3)  =  U4_g(x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x3)
U2_g(x1, x2)  =  U2_g(x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x2)
g_out_g(x1)  =  g_out_g
U7_g(x1, x2, x3)  =  U7_g(x1, x3)
U8_g(x1, x2, x3)  =  U8_g(x3)
h_out_g(x1)  =  h_out_g
H_IN_G(x1)  =  H_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
F_IN_G(x1)  =  F_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x2)
TRUE_IN_  =  TRUE_IN_
U4_G(x1, x2, x3)  =  U4_G(x2, x3)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U5_G(x1, x2, x3)  =  U5_G(x3)
U2_G(x1, x2)  =  U2_G(x2)
G_IN_G(x1)  =  G_IN_G(x1)
U6_G(x1, x2)  =  U6_G(x2)
U7_G(x1, x2, x3)  =  U7_G(x1, x3)
U8_G(x1, x2, x3)  =  U8_G(x3)

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

(80) Obligation:

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

H_IN_G(X) → U1_G(X, f_in_g(X))
H_IN_G(X) → F_IN_G(X)
F_IN_G(c(0, X1)) → U3_G(X1, true_in_)
F_IN_G(c(0, X1)) → TRUE_IN_
F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
F_IN_G(c(X, Y)) → P_IN_GA(X, P)
U4_G(X, Y, p_out_ga(X, P)) → U5_G(X, Y, f_in_g(c(P, s(Y))))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))
U1_G(X, f_out_g(X)) → U2_G(X, g_in_g(X))
U1_G(X, f_out_g(X)) → G_IN_G(X)
G_IN_G(c(X2, 0)) → U6_G(X2, true_in_)
G_IN_G(c(X2, 0)) → TRUE_IN_
G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
G_IN_G(c(X, Y)) → P_IN_GA(Y, P)
U7_G(X, Y, p_out_ga(Y, P)) → U8_G(X, Y, g_in_g(c(s(X), P)))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g
U4_g(x1, x2, x3)  =  U4_g(x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x3)
U2_g(x1, x2)  =  U2_g(x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x2)
g_out_g(x1)  =  g_out_g
U7_g(x1, x2, x3)  =  U7_g(x1, x3)
U8_g(x1, x2, x3)  =  U8_g(x3)
h_out_g(x1)  =  h_out_g
H_IN_G(x1)  =  H_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
F_IN_G(x1)  =  F_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x2)
TRUE_IN_  =  TRUE_IN_
U4_G(x1, x2, x3)  =  U4_G(x2, x3)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U5_G(x1, x2, x3)  =  U5_G(x3)
U2_G(x1, x2)  =  U2_G(x2)
G_IN_G(x1)  =  G_IN_G(x1)
U6_G(x1, x2)  =  U6_G(x2)
U7_G(x1, x2, x3)  =  U7_G(x1, x3)
U8_G(x1, x2, x3)  =  U8_G(x3)

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

(81) DependencyGraphProof (EQUIVALENT transformation)

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

(82) Complex Obligation (AND)

(83) Obligation:

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

G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g
U4_g(x1, x2, x3)  =  U4_g(x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x3)
U2_g(x1, x2)  =  U2_g(x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x2)
g_out_g(x1)  =  g_out_g
U7_g(x1, x2, x3)  =  U7_g(x1, x3)
U8_g(x1, x2, x3)  =  U8_g(x3)
h_out_g(x1)  =  h_out_g
G_IN_G(x1)  =  G_IN_G(x1)
U7_G(x1, x2, x3)  =  U7_G(x1, x3)

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

(84) UsableRulesProof (EQUIVALENT transformation)

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

(85) Obligation:

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

G_IN_G(c(X, Y)) → U7_G(X, Y, p_in_ga(Y, P))
U7_G(X, Y, p_out_ga(Y, P)) → G_IN_G(c(s(X), P))

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)

The argument filtering Pi contains the following mapping:
c(x1, x2)  =  c(x1, x2)
0  =  0
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
G_IN_G(x1)  =  G_IN_G(x1)
U7_G(x1, x2, x3)  =  U7_G(x1, x3)

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

(86) PiDPToQDPProof (SOUND transformation)

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

(87) Obligation:

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

G_IN_G(c(X, Y)) → U7_G(X, p_in_ga(Y))
U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(88) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(X, Y)) → U7_G(X, p_in_ga(Y)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(z0), z1)) → U7_G(s(z0), p_in_ga(z1))

(89) Obligation:

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

U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P))
G_IN_G(c(s(z0), z1)) → U7_G(s(z0), p_in_ga(z1))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(90) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule G_IN_G(c(X, Y)) → U7_G(X, p_in_ga(Y)) at position [1] we obtained the following new rules [LPAR04]:

G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, p_out_ga(x0))

(91) Obligation:

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

U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, p_out_ga(x0))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

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

(93) Obligation:

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

U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, p_out_ga(x0))

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

p_in_ga(x0)

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

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

(95) Obligation:

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

U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))
G_IN_G(c(y0, s(x0))) → U7_G(y0, p_out_ga(x0))

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

(96) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

G_IN_G(c(y0, s(x0))) → U7_G(y0, p_out_ga(x0))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U7_G(x1, x2)) =

1

+

[ 0, 0 ]

·

x1

+

[ 1, 1 ]

·

x2

POL(p_out_ga(x1)) =

/ 0 \ \ 0 /

+

/ 1 1 \ \ 1 1 /

·

x1

POL(G_IN_G(x1)) =

0

+

[ 1, 0 ]

·

x1

POL(c(x1, x2)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 1 1 \ \ 0 0 /

·

x2

POL(s(x1)) =

/ 1 \ \ 0 /

+

/ 1 1 \ \ 1 1 /

·

x1

POL(0) =

/ 0 \ \ 0 /

The following usable rules [FROCOS05] were oriented: none

(97) Obligation:

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

U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P))
G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))

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

(98) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P)) we obtained the following new rules [LPAR04]:

U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0))

(99) Obligation:

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

G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))
U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0))

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

(100) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_G(X, p_out_ga(P)) → G_IN_G(c(s(X), P)) we obtained the following new rules [LPAR04]:

U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0))

(101) Obligation:

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

G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0))
U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0))

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

(102) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(z0), 0)) → U7_G(s(z0), p_out_ga(0))

(103) Obligation:

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

U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0))
G_IN_G(c(s(z0), 0)) → U7_G(s(z0), p_out_ga(0))

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

(104) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(y0, 0)) → U7_G(y0, p_out_ga(0)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(z0), 0)) → U7_G(s(z0), p_out_ga(0))

(105) Obligation:

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

U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0))
G_IN_G(c(s(z0), 0)) → U7_G(s(z0), p_out_ga(0))

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

(106) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_G(z0, p_out_ga(0)) → G_IN_G(c(s(z0), 0)) we obtained the following new rules [LPAR04]:

U7_G(s(z0), p_out_ga(0)) → G_IN_G(c(s(s(z0)), 0))

(107) Obligation:

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

G_IN_G(c(s(z0), 0)) → U7_G(s(z0), p_out_ga(0))
U7_G(s(z0), p_out_ga(0)) → G_IN_G(c(s(s(z0)), 0))

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

(108) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G_IN_G(c(s(z0), 0)) → U7_G(s(z0), p_out_ga(0)) we obtained the following new rules [LPAR04]:

G_IN_G(c(s(s(z0)), 0)) → U7_G(s(s(z0)), p_out_ga(0))

(109) Obligation:

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

U7_G(s(z0), p_out_ga(0)) → G_IN_G(c(s(s(z0)), 0))
G_IN_G(c(s(s(z0)), 0)) → U7_G(s(s(z0)), p_out_ga(0))

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

(110) 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 = G_IN_G(c(s(s(z0')), 0)) evaluates to t =G_IN_G(c(s(s(s(z0'))), 0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [z0' / s(z0')]
• Semiunifier: [ ]

---

Rewriting sequence

G_IN_G(c(s(s(z0')), 0)) → U7_G(s(s(z0')), p_out_ga(0))
with rule G_IN_G(c(s(s(z0'')), 0)) → U7_G(s(s(z0'')), p_out_ga(0)) at position [] and matcher [z0'' / z0']

U7_G(s(s(z0')), p_out_ga(0)) → G_IN_G(c(s(s(s(z0'))), 0))
with rule U7_G(s(z0), p_out_ga(0)) → G_IN_G(c(s(s(z0)), 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.

(111) FALSE

(112) Obligation:

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

F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))

The TRS R consists of the following rules:

h_in_g(X) → U1_g(X, f_in_g(X))
f_in_g(c(0, X1)) → U3_g(X1, true_in_)
true_in_ → true_out_
U3_g(X1, true_out_) → f_out_g(c(0, X1))
f_in_g(c(X, Y)) → U4_g(X, Y, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_g(X, Y, p_out_ga(X, P)) → U5_g(X, Y, f_in_g(c(P, s(Y))))
U5_g(X, Y, f_out_g(c(P, s(Y)))) → f_out_g(c(X, Y))
U1_g(X, f_out_g(X)) → U2_g(X, g_in_g(X))
g_in_g(c(X2, 0)) → U6_g(X2, true_in_)
U6_g(X2, true_out_) → g_out_g(c(X2, 0))
g_in_g(c(X, Y)) → U7_g(X, Y, p_in_ga(Y, P))
U7_g(X, Y, p_out_ga(Y, P)) → U8_g(X, Y, g_in_g(c(s(X), P)))
U8_g(X, Y, g_out_g(c(s(X), P))) → g_out_g(c(X, Y))
U2_g(X, g_out_g(X)) → h_out_g(X)

The argument filtering Pi contains the following mapping:
h_in_g(x1)  =  h_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
f_in_g(x1)  =  f_in_g(x1)
c(x1, x2)  =  c(x1, x2)
0  =  0
U3_g(x1, x2)  =  U3_g(x2)
true_in_  =  true_in_
true_out_  =  true_out_
f_out_g(x1)  =  f_out_g
U4_g(x1, x2, x3)  =  U4_g(x2, x3)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U5_g(x1, x2, x3)  =  U5_g(x3)
U2_g(x1, x2)  =  U2_g(x2)
g_in_g(x1)  =  g_in_g(x1)
U6_g(x1, x2)  =  U6_g(x2)
g_out_g(x1)  =  g_out_g
U7_g(x1, x2, x3)  =  U7_g(x1, x3)
U8_g(x1, x2, x3)  =  U8_g(x3)
h_out_g(x1)  =  h_out_g
F_IN_G(x1)  =  F_IN_G(x1)
U4_G(x1, x2, x3)  =  U4_G(x2, x3)

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

(113) UsableRulesProof (EQUIVALENT transformation)

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

(114) Obligation:

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

F_IN_G(c(X, Y)) → U4_G(X, Y, p_in_ga(X, P))
U4_G(X, Y, p_out_ga(X, P)) → F_IN_G(c(P, s(Y)))

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)

The argument filtering Pi contains the following mapping:
c(x1, x2)  =  c(x1, x2)
0  =  0
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
F_IN_G(x1)  =  F_IN_G(x1)
U4_G(x1, x2, x3)  =  U4_G(x2, x3)

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

(115) PiDPToQDPProof (SOUND transformation)

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

(116) Obligation:

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

F_IN_G(c(X, Y)) → U4_G(Y, p_in_ga(X))
U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y)))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(117) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(X, Y)) → U4_G(Y, p_in_ga(X)) we obtained the following new rules [LPAR04]:

F_IN_G(c(z1, s(z0))) → U4_G(s(z0), p_in_ga(z1))

(118) Obligation:

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

U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(z1, s(z0))) → U4_G(s(z0), p_in_ga(z1))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

(119) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule F_IN_G(c(X, Y)) → U4_G(Y, p_in_ga(X)) at position [1] we obtained the following new rules [LPAR04]:

F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))
F_IN_G(c(s(x0), y1)) → U4_G(y1, p_out_ga(x0))

(120) Obligation:

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

U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))
F_IN_G(c(s(x0), y1)) → U4_G(y1, p_out_ga(x0))

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)

The set Q consists of the following terms:

p_in_ga(x0)

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

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

(122) Obligation:

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

U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))
F_IN_G(c(s(x0), y1)) → U4_G(y1, p_out_ga(x0))

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

p_in_ga(x0)

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

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

(124) Obligation:

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

U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))
F_IN_G(c(s(x0), y1)) → U4_G(y1, p_out_ga(x0))

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

(125) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

F_IN_G(c(s(x0), y1)) → U4_G(y1, p_out_ga(x0))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U4_G(x1, x2)) =

1

+

[ 0, 0 ]

·

x1

+

[ 1, 1 ]

·

x2

POL(p_out_ga(x1)) =

/ 0 \ \ 0 /

+

/ 1 1 \ \ 1 1 /

·

x1

POL(F_IN_G(x1)) =

0

+

[ 1, 0 ]

·

x1

POL(c(x1, x2)) =

/ 1 \ \ 0 /

+

/ 1 1 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 0 /

·

x2

POL(s(x1)) =

/ 1 \ \ 0 /

+

/ 1 1 \ \ 1 1 /

·

x1

POL(0) =

/ 0 \ \ 0 /

The following usable rules [FROCOS05] were oriented: none

(126) Obligation:

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

U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y)))
F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))

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

(127) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y))) we obtained the following new rules [LPAR04]:

U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0)))

(128) Obligation:

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

F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))
U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0)))

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

(129) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(Y, p_out_ga(P)) → F_IN_G(c(P, s(Y))) we obtained the following new rules [LPAR04]:

U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0)))

(130) Obligation:

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

F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0))
U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0)))

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

(131) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0)) we obtained the following new rules [LPAR04]:

F_IN_G(c(0, s(z0))) → U4_G(s(z0), p_out_ga(0))

(132) Obligation:

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

U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0)))
F_IN_G(c(0, s(z0))) → U4_G(s(z0), p_out_ga(0))

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

(133) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(0, y1)) → U4_G(y1, p_out_ga(0)) we obtained the following new rules [LPAR04]:

F_IN_G(c(0, s(z0))) → U4_G(s(z0), p_out_ga(0))

(134) Obligation:

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

U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0)))
F_IN_G(c(0, s(z0))) → U4_G(s(z0), p_out_ga(0))

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

(135) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(z0, p_out_ga(0)) → F_IN_G(c(0, s(z0))) we obtained the following new rules [LPAR04]:

U4_G(s(z0), p_out_ga(0)) → F_IN_G(c(0, s(s(z0))))

(136) Obligation:

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

F_IN_G(c(0, s(z0))) → U4_G(s(z0), p_out_ga(0))
U4_G(s(z0), p_out_ga(0)) → F_IN_G(c(0, s(s(z0))))

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

(137) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F_IN_G(c(0, s(z0))) → U4_G(s(z0), p_out_ga(0)) we obtained the following new rules [LPAR04]:

F_IN_G(c(0, s(s(z0)))) → U4_G(s(s(z0)), p_out_ga(0))

(138) Obligation:

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

U4_G(s(z0), p_out_ga(0)) → F_IN_G(c(0, s(s(z0))))
F_IN_G(c(0, s(s(z0)))) → U4_G(s(s(z0)), p_out_ga(0))

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

(139) 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 = F_IN_G(c(0, s(s(z0')))) evaluates to t =F_IN_G(c(0, s(s(s(z0')))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [z0' / s(z0')]

---

Rewriting sequence

F_IN_G(c(0, s(s(z0')))) → U4_G(s(s(z0')), p_out_ga(0))
with rule F_IN_G(c(0, s(s(z0'')))) → U4_G(s(s(z0'')), p_out_ga(0)) at position [] and matcher [z0'' / z0']

U4_G(s(s(z0')), p_out_ga(0)) → F_IN_G(c(0, s(s(s(z0')))))
with rule U4_G(s(z0), p_out_ga(0)) → F_IN_G(c(0, s(s(z0))))

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.

(140) FALSE