(0) Obligation:
Clauses:
q(X, Y) :- m(X, Y, Z).
m(X, 0, X).
m(0, Y, 0) :- !.
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
Queries:
q(g,g).
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
q(X, Y) :- m(X, Y, Z).
m(X, 0, X).
m(0, Y, 0) :- true.
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
Queries:
q(g,g).
(3) UndefinedPredicateHandlerProof (SOUND transformation)
Added facts for all undefined predicates [PROLOG].
(4) Obligation:
Clauses:
q(X, Y) :- m(X, Y, Z).
m(X, 0, X).
m(0, Y, 0) :- true.
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
true.
Queries:
q(g,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:
q_in: (b,b)
m_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2) =
U2_gga(
x1,
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
q_out_gg(
x1,
x2) =
q_out_gg(
x1,
x2)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(6) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2) =
U2_gga(
x1,
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
q_out_gg(
x1,
x2) =
q_out_gg(
x1,
x2)
(7) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
Q_IN_GG(X, Y) → U1_GG(X, Y, m_in_gga(X, Y, Z))
Q_IN_GG(X, Y) → M_IN_GGA(X, Y, Z)
M_IN_GGA(0, Y, 0) → U2_GGA(Y, true_in_)
M_IN_GGA(0, Y, 0) → TRUE_IN_
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
M_IN_GGA(X, Y, Z) → P_IN_GA(X, A)
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → P_IN_GA(Y, B)
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → U5_GGA(X, Y, Z, m_in_gga(A, B, Z))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2) =
U2_gga(
x1,
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
q_out_gg(
x1,
x2) =
q_out_gg(
x1,
x2)
Q_IN_GG(
x1,
x2) =
Q_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x1,
x2,
x3)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2) =
U2_GGA(
x1,
x2)
TRUE_IN_ =
TRUE_IN_
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x4,
x5)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
Q_IN_GG(X, Y) → U1_GG(X, Y, m_in_gga(X, Y, Z))
Q_IN_GG(X, Y) → M_IN_GGA(X, Y, Z)
M_IN_GGA(0, Y, 0) → U2_GGA(Y, true_in_)
M_IN_GGA(0, Y, 0) → TRUE_IN_
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
M_IN_GGA(X, Y, Z) → P_IN_GA(X, A)
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → P_IN_GA(Y, B)
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → U5_GGA(X, Y, Z, m_in_gga(A, B, Z))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2) =
U2_gga(
x1,
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
q_out_gg(
x1,
x2) =
q_out_gg(
x1,
x2)
Q_IN_GG(
x1,
x2) =
Q_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x1,
x2,
x3)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2) =
U2_GGA(
x1,
x2)
TRUE_IN_ =
TRUE_IN_
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x4,
x5)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 7 less nodes.
(10) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2) =
U2_gga(
x1,
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
q_out_gg(
x1,
x2) =
q_out_gg(
x1,
x2)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x4,
x5)
We have to consider all (P,R,Pi)-chains
(11) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(12) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
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:
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)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x4,
x5)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y) → U3_GGA(X, Y, p_in_ga(X))
U3_GGA(X, Y, p_out_ga(X, A)) → U4_GGA(X, Y, A, p_in_ga(Y))
U4_GGA(X, Y, A, p_out_ga(Y, B)) → M_IN_GGA(A, B)
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.
(15) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
M_IN_GGA(
X,
Y) →
U3_GGA(
X,
Y,
p_in_ga(
X)) at position [2] we obtained the following new rules [LPAR04]:
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, Y, p_out_ga(X, A)) → U4_GGA(X, Y, A, p_in_ga(Y))
U4_GGA(X, Y, A, p_out_ga(Y, B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(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.
(17) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U3_GGA(
X,
Y,
p_out_ga(
X,
A)) →
U4_GGA(
X,
Y,
A,
p_in_ga(
Y)) at position [3] we obtained the following new rules [LPAR04]:
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(x0), p_out_ga(y0, y2)) → U4_GGA(y0, s(x0), y2, p_out_ga(s(x0), x0))
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(X, Y, A, p_out_ga(Y, B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(x0), p_out_ga(y0, y2)) → U4_GGA(y0, s(x0), y2, 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.
(19) 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.
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(X, Y, A, p_out_ga(Y, B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(x0), p_out_ga(y0, y2)) → U4_GGA(y0, s(x0), y2, 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.
(21) 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)
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(X, Y, A, p_out_ga(Y, B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(x0), p_out_ga(y0, y2)) → U4_GGA(y0, s(x0), y2, p_out_ga(s(x0), x0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(23) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
X,
Y,
A,
p_out_ga(
Y,
B)) →
M_IN_GGA(
A,
B) we obtained the following new rules [LPAR04]:
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(z1), z2, p_out_ga(s(z1), z1)) → M_IN_GGA(z2, z1)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(x0), p_out_ga(y0, y2)) → U4_GGA(y0, s(x0), y2, p_out_ga(s(x0), x0))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(z1), z2, p_out_ga(s(z1), z1)) → M_IN_GGA(z2, z1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(25) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
y0,
0,
p_out_ga(
y0,
y2)) →
U4_GGA(
y0,
0,
y2,
p_out_ga(
0,
0)) we obtained the following new rules [LPAR04]:
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(y0, s(x0), p_out_ga(y0, y2)) → U4_GGA(y0, s(x0), y2, p_out_ga(s(x0), x0))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(z1), z2, p_out_ga(s(z1), z1)) → M_IN_GGA(z2, z1)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(27) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
y0,
s(
x0),
p_out_ga(
y0,
y2)) →
U4_GGA(
y0,
s(
x0),
y2,
p_out_ga(
s(
x0),
x0)) we obtained the following new rules [LPAR04]:
U3_GGA(0, s(x1), p_out_ga(0, 0)) → U4_GGA(0, s(x1), 0, p_out_ga(s(x1), x1))
U3_GGA(s(z0), s(x1), p_out_ga(s(z0), z0)) → U4_GGA(s(z0), s(x1), z0, p_out_ga(s(x1), x1))
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(z1), z2, p_out_ga(s(z1), z1)) → M_IN_GGA(z2, z1)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
U3_GGA(0, s(x1), p_out_ga(0, 0)) → U4_GGA(0, s(x1), 0, p_out_ga(s(x1), x1))
U3_GGA(s(z0), s(x1), p_out_ga(s(z0), z0)) → U4_GGA(s(z0), s(x1), z0, p_out_ga(s(x1), x1))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(29) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
z0,
0,
z1,
p_out_ga(
0,
0)) →
M_IN_GGA(
z1,
0) we obtained the following new rules [LPAR04]:
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(z0), 0, z0, p_out_ga(0, 0)) → M_IN_GGA(z0, 0)
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U4_GGA(z0, s(z1), z2, p_out_ga(s(z1), z1)) → M_IN_GGA(z2, z1)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
U3_GGA(0, s(x1), p_out_ga(0, 0)) → U4_GGA(0, s(x1), 0, p_out_ga(s(x1), x1))
U3_GGA(s(z0), s(x1), p_out_ga(s(z0), z0)) → U4_GGA(s(z0), s(x1), z0, p_out_ga(s(x1), x1))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(z0), 0, z0, p_out_ga(0, 0)) → M_IN_GGA(z0, 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
U4_GGA(
z0,
s(
z1),
z2,
p_out_ga(
s(
z1),
z1)) →
M_IN_GGA(
z2,
z1) we obtained the following new rules [LPAR04]:
U4_GGA(0, s(z0), 0, p_out_ga(s(z0), z0)) → M_IN_GGA(0, z0)
U4_GGA(s(z0), s(z1), z0, p_out_ga(s(z1), z1)) → M_IN_GGA(z0, z1)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
U3_GGA(0, s(x1), p_out_ga(0, 0)) → U4_GGA(0, s(x1), 0, p_out_ga(s(x1), x1))
U3_GGA(s(z0), s(x1), p_out_ga(s(z0), z0)) → U4_GGA(s(z0), s(x1), z0, p_out_ga(s(x1), x1))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(z0), 0, z0, p_out_ga(0, 0)) → M_IN_GGA(z0, 0)
U4_GGA(0, s(z0), 0, p_out_ga(s(z0), z0)) → M_IN_GGA(0, z0)
U4_GGA(s(z0), s(z1), z0, p_out_ga(s(z1), z1)) → M_IN_GGA(z0, z1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(33) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(34) Complex Obligation (AND)
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
U3_GGA(0, s(x1), p_out_ga(0, 0)) → U4_GGA(0, s(x1), 0, p_out_ga(s(x1), x1))
U4_GGA(0, s(z0), 0, p_out_ga(s(z0), z0)) → M_IN_GGA(0, z0)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(36) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U3_GGA(0, s(x1), p_out_ga(0, 0)) → U4_GGA(0, s(x1), 0, p_out_ga(s(x1), x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
| POL(U3_GGA(x1, x2, x3)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(p_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(U4_GGA(x1, x2, x3, x4)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
| POL(M_IN_GGA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
none
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
U4_GGA(0, s(z0), 0, p_out_ga(s(z0), z0)) → M_IN_GGA(0, z0)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(38) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
M_IN_GGA(0, y1) → U3_GGA(0, y1, p_out_ga(0, 0))
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(40) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
M_IN_GGA(
0,
y1) →
U3_GGA(
0,
y1,
p_out_ga(
0,
0)) we obtained the following new rules [LPAR04]:
M_IN_GGA(0, 0) → U3_GGA(0, 0, p_out_ga(0, 0))
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
M_IN_GGA(0, 0) → U3_GGA(0, 0, p_out_ga(0, 0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(42) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
M_IN_GGA(
0,
y1) →
U3_GGA(
0,
y1,
p_out_ga(
0,
0)) we obtained the following new rules [LPAR04]:
M_IN_GGA(0, 0) → U3_GGA(0, 0, p_out_ga(0, 0))
(43) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
M_IN_GGA(0, 0) → U3_GGA(0, 0, p_out_ga(0, 0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(44) 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 =
M_IN_GGA(
0,
0) evaluates to t =
M_IN_GGA(
0,
0)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceM_IN_GGA(0, 0) →
U3_GGA(
0,
0,
p_out_ga(
0,
0))
with rule
M_IN_GGA(
0,
0) →
U3_GGA(
0,
0,
p_out_ga(
0,
0)) at position [] and matcher [ ]
U3_GGA(0, 0, p_out_ga(0, 0)) →
U4_GGA(
0,
0,
0,
p_out_ga(
0,
0))
with rule
U3_GGA(
0,
0,
p_out_ga(
0,
0)) →
U4_GGA(
0,
0,
0,
p_out_ga(
0,
0)) at position [] and matcher [ ]
U4_GGA(0, 0, 0, p_out_ga(0, 0)) →
M_IN_GGA(
0,
0)
with rule
U4_GGA(
0,
0,
0,
p_out_ga(
0,
0)) →
M_IN_GGA(
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.
(45) FALSE
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
U4_GGA(s(z0), 0, z0, p_out_ga(0, 0)) → M_IN_GGA(z0, 0)
U3_GGA(s(z0), s(x1), p_out_ga(s(z0), z0)) → U4_GGA(s(z0), s(x1), z0, p_out_ga(s(x1), x1))
U4_GGA(s(z0), s(z1), z0, p_out_ga(s(z1), z1)) → M_IN_GGA(z0, z1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(47) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- M_IN_GGA(s(x0), y1) → U3_GGA(s(x0), y1, p_out_ga(s(x0), x0))
The graph contains the following edges 1 >= 1, 2 >= 2
- U4_GGA(s(z0), 0, z0, p_out_ga(0, 0)) → M_IN_GGA(z0, 0)
The graph contains the following edges 1 > 1, 3 >= 1, 2 >= 2, 4 > 2
- U4_GGA(s(z0), s(z1), z0, p_out_ga(s(z1), z1)) → M_IN_GGA(z0, z1)
The graph contains the following edges 1 > 1, 3 >= 1, 2 > 2, 4 > 2
- U3_GGA(s(z0), 0, p_out_ga(s(z0), z0)) → U4_GGA(s(z0), 0, z0, p_out_ga(0, 0))
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2, 1 > 3, 3 > 3
- U3_GGA(s(z0), s(x1), p_out_ga(s(z0), z0)) → U4_GGA(s(z0), s(x1), z0, p_out_ga(s(x1), x1))
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2, 1 > 3, 3 > 3
(48) TRUE
(49) 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,b)
m_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2) =
U2_gga(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gg(
x1,
x2) =
q_out_gg
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(50) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2) =
U2_gga(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gg(
x1,
x2) =
q_out_gg
(51) 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_GG(X, Y) → U1_GG(X, Y, m_in_gga(X, Y, Z))
Q_IN_GG(X, Y) → M_IN_GGA(X, Y, Z)
M_IN_GGA(0, Y, 0) → U2_GGA(Y, true_in_)
M_IN_GGA(0, Y, 0) → TRUE_IN_
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
M_IN_GGA(X, Y, Z) → P_IN_GA(X, A)
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → P_IN_GA(Y, B)
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → U5_GGA(X, Y, Z, m_in_gga(A, B, Z))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2) =
U2_gga(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gg(
x1,
x2) =
q_out_gg
Q_IN_GG(
x1,
x2) =
Q_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x3)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2) =
U2_GGA(
x2)
TRUE_IN_ =
TRUE_IN_
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x4,
x5)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x4)
We have to consider all (P,R,Pi)-chains
(52) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
Q_IN_GG(X, Y) → U1_GG(X, Y, m_in_gga(X, Y, Z))
Q_IN_GG(X, Y) → M_IN_GGA(X, Y, Z)
M_IN_GGA(0, Y, 0) → U2_GGA(Y, true_in_)
M_IN_GGA(0, Y, 0) → TRUE_IN_
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
M_IN_GGA(X, Y, Z) → P_IN_GA(X, A)
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → P_IN_GA(Y, B)
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → U5_GGA(X, Y, Z, m_in_gga(A, B, Z))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2) =
U2_gga(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gg(
x1,
x2) =
q_out_gg
Q_IN_GG(
x1,
x2) =
Q_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x3)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2) =
U2_GGA(
x2)
TRUE_IN_ =
TRUE_IN_
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x4,
x5)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x4)
We have to consider all (P,R,Pi)-chains
(53) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 7 less nodes.
(54) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
The TRS R consists of the following rules:
q_in_gg(X, Y) → U1_gg(X, Y, m_in_gga(X, Y, Z))
m_in_gga(X, 0, X) → m_out_gga(X, 0, X)
m_in_gga(0, Y, 0) → U2_gga(Y, true_in_)
true_in_ → true_out_
U2_gga(Y, true_out_) → m_out_gga(0, Y, 0)
m_in_gga(X, Y, Z) → U3_gga(X, Y, Z, p_in_ga(X, A))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U3_gga(X, Y, Z, p_out_ga(X, A)) → U4_gga(X, Y, Z, A, p_in_ga(Y, B))
U4_gga(X, Y, Z, A, p_out_ga(Y, B)) → U5_gga(X, Y, Z, m_in_gga(A, B, Z))
U5_gga(X, Y, Z, m_out_gga(A, B, Z)) → m_out_gga(X, Y, Z)
U1_gg(X, Y, m_out_gga(X, Y, Z)) → q_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
q_in_gg(
x1,
x2) =
q_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x3)
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2) =
U2_gga(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x2,
x4)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
s(
x1) =
s(
x1)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gg(
x1,
x2) =
q_out_gg
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x4,
x5)
We have to consider all (P,R,Pi)-chains
(55) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(56) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, p_in_ga(X, A))
U3_GGA(X, Y, Z, p_out_ga(X, A)) → U4_GGA(X, Y, Z, A, p_in_ga(Y, B))
U4_GGA(X, Y, Z, A, p_out_ga(Y, B)) → M_IN_GGA(A, B, Z)
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:
0 =
0
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
s(
x1) =
s(
x1)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x4,
x5)
We have to consider all (P,R,Pi)-chains
(57) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y) → U3_GGA(Y, p_in_ga(X))
U3_GGA(Y, p_out_ga(A)) → U4_GGA(A, p_in_ga(Y))
U4_GGA(A, p_out_ga(B)) → M_IN_GGA(A, B)
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.
(59) 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(M_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U3_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U4_GGA(x1, x2)) = 2·x1 + 2·x2
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 2·x1
POL(s(x1)) = 2·x1
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, Y) → U3_GGA(Y, p_in_ga(X))
U3_GGA(Y, p_out_ga(A)) → U4_GGA(A, p_in_ga(Y))
U4_GGA(A, p_out_ga(B)) → M_IN_GGA(A, B)
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.
(61) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
M_IN_GGA(
X,
Y) →
U3_GGA(
Y,
p_in_ga(
X)) at position [1] we obtained the following new rules [LPAR04]:
M_IN_GGA(0, y1) → U3_GGA(y1, p_out_ga(0))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(Y, p_out_ga(A)) → U4_GGA(A, p_in_ga(Y))
U4_GGA(A, p_out_ga(B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(y1, 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.
(63) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U3_GGA(
Y,
p_out_ga(
A)) →
U4_GGA(
A,
p_in_ga(
Y)) at position [1] we obtained the following new rules [LPAR04]:
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(A, p_out_ga(B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(y1, p_out_ga(0))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, 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.
(65) 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.
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(A, p_out_ga(B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(y1, p_out_ga(0))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, 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.
(67) 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)
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(A, p_out_ga(B)) → M_IN_GGA(A, B)
M_IN_GGA(0, y1) → U3_GGA(y1, p_out_ga(0))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(69) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
A,
p_out_ga(
B)) →
M_IN_GGA(
A,
B) we obtained the following new rules [LPAR04]:
U4_GGA(z0, p_out_ga(0)) → M_IN_GGA(z0, 0)
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(y1, p_out_ga(0))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
U4_GGA(z0, p_out_ga(0)) → M_IN_GGA(z0, 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
M_IN_GGA(
0,
y1) →
U3_GGA(
y1,
p_out_ga(
0)) we obtained the following new rules [LPAR04]:
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
U4_GGA(z0, p_out_ga(0)) → M_IN_GGA(z0, 0)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(73) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
0,
p_out_ga(
y1)) →
U4_GGA(
y1,
p_out_ga(
0)) we obtained the following new rules [LPAR04]:
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(z0, p_out_ga(0)) → M_IN_GGA(z0, 0)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(75) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
z0,
p_out_ga(
0)) →
M_IN_GGA(
z0,
0) we obtained the following new rules [LPAR04]:
U4_GGA(0, p_out_ga(0)) → M_IN_GGA(0, 0)
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
U4_GGA(0, p_out_ga(0)) → M_IN_GGA(0, 0)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(77) 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 =
U3_GGA(
0,
p_out_ga(
0)) evaluates to t =
U3_GGA(
0,
p_out_ga(
0))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequenceU3_GGA(0, p_out_ga(0)) →
U4_GGA(
0,
p_out_ga(
0))
with rule
U3_GGA(
0,
p_out_ga(
0)) →
U4_GGA(
0,
p_out_ga(
0)) at position [] and matcher [ ]
U4_GGA(0, p_out_ga(0)) →
M_IN_GGA(
0,
0)
with rule
U4_GGA(
0,
p_out_ga(
0)) →
M_IN_GGA(
0,
0) at position [] and matcher [ ]
M_IN_GGA(0, 0) →
U3_GGA(
0,
p_out_ga(
0))
with rule
M_IN_GGA(
0,
0) →
U3_GGA(
0,
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.
(78) FALSE