(0) Obligation:
Clauses:
m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
=(X, X).
Queries:
m(g,g,a).
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
m(X, 0, Z) :- =(Z, X).
m(0, Y, Z) :- =(Z, 0).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
=(X, X).
Queries:
m(g,g,a).
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
m_in: (b,b,f)
p_in: (b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x1,
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x1,
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, 0, Z) → U1_GGA(X, Z, =_in_ag(Z, X))
M_IN_GGA(X, 0, Z) → =_IN_AG(Z, X)
M_IN_GGA(0, Y, Z) → U2_GGA(Y, Z, =_in_ag(Z, 0))
M_IN_GGA(0, Y, Z) → =_IN_AG(Z, 0)
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)
P_IN_GA(s(s(X)), s(Y)) → U6_GA(X, Y, p_in_ga(s(X), Y))
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
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:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x1,
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x1,
x3)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x1,
x3)
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
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, 0, Z) → U1_GGA(X, Z, =_in_ag(Z, X))
M_IN_GGA(X, 0, Z) → =_IN_AG(Z, X)
M_IN_GGA(0, Y, Z) → U2_GGA(Y, Z, =_in_ag(Z, 0))
M_IN_GGA(0, Y, Z) → =_IN_AG(Z, 0)
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)
P_IN_GA(s(s(X)), s(Y)) → U6_GA(X, Y, p_in_ga(s(X), Y))
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
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:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x1,
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x1,
x3)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x1,
x3)
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
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
The TRS R consists of the following rules:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x1,
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_GA(s(s(X))) → P_IN_GA(s(X))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) 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:
- P_IN_GA(s(s(X))) → P_IN_GA(s(X))
The graph contains the following edges 1 > 1
(15) TRUE
(16) 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:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x1,
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
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
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(18) 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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x1,
x3)
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
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(20) 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(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(21) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
(22) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(23) 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(0), p_out_ga(y0, y2)) → U4_GGA(y0, s(0), y2, p_out_ga(s(0), 0))
U3_GGA(y0, s(s(x0)), p_out_ga(y0, y2)) → U4_GGA(y0, s(s(x0)), y2, U6_ga(x0, p_in_ga(s(x0))))
(24) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(0), p_out_ga(y0, y2)) → U4_GGA(y0, s(0), y2, p_out_ga(s(0), 0))
U3_GGA(y0, s(s(x0)), p_out_ga(y0, y2)) → U4_GGA(y0, s(s(x0)), y2, U6_ga(x0, p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(25) 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.
(26) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(0), p_out_ga(y0, y2)) → U4_GGA(y0, s(0), y2, p_out_ga(s(0), 0))
U3_GGA(y0, s(s(x0)), p_out_ga(y0, y2)) → U4_GGA(y0, s(s(x0)), y2, U6_ga(x0, p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(27) 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(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
(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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(y0, 0, p_out_ga(y0, y2)) → U4_GGA(y0, 0, y2, p_out_ga(0, 0))
U3_GGA(y0, s(0), p_out_ga(y0, y2)) → U4_GGA(y0, s(0), y2, p_out_ga(s(0), 0))
U3_GGA(y0, s(s(x0)), p_out_ga(y0, y2)) → U4_GGA(y0, s(s(x0)), y2, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(29) 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(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(y0, s(0), p_out_ga(y0, y2)) → U4_GGA(y0, s(0), y2, p_out_ga(s(0), 0))
U3_GGA(y0, s(s(x0)), p_out_ga(y0, y2)) → U4_GGA(y0, s(s(x0)), y2, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(31) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
y0,
s(
0),
p_out_ga(
y0,
y2)) →
U4_GGA(
y0,
s(
0),
y2,
p_out_ga(
s(
0),
0)) we obtained the following new rules [LPAR04]:
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(0), s(0), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
(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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(y0, s(s(x0)), p_out_ga(y0, y2)) → U4_GGA(y0, s(s(x0)), y2, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(0), s(0), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(33) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
y0,
s(
s(
x0)),
p_out_ga(
y0,
y2)) →
U4_GGA(
y0,
s(
s(
x0)),
y2,
U6_ga(
x0,
p_in_ga(
s(
x0)))) we obtained the following new rules [LPAR04]:
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(0), s(s(x1)), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
(34) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(z0, 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(0), s(0), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(0), s(s(x1)), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(35) 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(0), 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
(36) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(z0, s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(0), s(0), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(0), s(s(x1)), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(0), 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(37) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
z0,
s(
0),
z1,
p_out_ga(
s(
0),
0)) →
M_IN_GGA(
z1,
0) we obtained the following new rules [LPAR04]:
U4_GGA(0, s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
(38) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(z0, s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(0), s(0), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(0), s(s(x1)), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(0), 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(0, s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(39) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
z0,
s(
s(
z1)),
z2,
p_out_ga(
s(
s(
z1)),
x3)) →
M_IN_GGA(
z2,
x3) we obtained the following new rules [LPAR04]:
U4_GGA(0, s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
U4_GGA(s(0), s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
U4_GGA(s(s(z0)), s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
(40) 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(0), y1) → U3_GGA(s(0), y1, p_out_ga(s(0), 0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
U3_GGA(s(0), 0, p_out_ga(s(0), 0)) → U4_GGA(s(0), 0, 0, p_out_ga(0, 0))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(0), s(0), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0))
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(0), s(s(x1)), p_out_ga(s(0), 0)) → U4_GGA(s(0), s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(0), 0, 0, p_out_ga(0, 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U4_GGA(0, s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U4_GGA(s(0), s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U4_GGA(s(s(z0)), s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U4_GGA(0, s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
U4_GGA(s(0), s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
U4_GGA(s(s(z0)), s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(41) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 7 less nodes.
(42) Complex Obligation (AND)
(43) 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(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U4_GGA(0, s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(44) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] 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))
M_IN_GGA(0, s(0)) → U3_GGA(0, s(0), p_out_ga(0, 0))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(0, s(s(y_0)), p_out_ga(0, 0))
(45) 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)
U3_GGA(0, s(0), p_out_ga(0, 0)) → U4_GGA(0, s(0), 0, p_out_ga(s(0), 0))
U4_GGA(0, s(0), 0, p_out_ga(s(0), 0)) → M_IN_GGA(0, 0)
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
M_IN_GGA(0, 0) → U3_GGA(0, 0, p_out_ga(0, 0))
M_IN_GGA(0, s(0)) → U3_GGA(0, s(0), p_out_ga(0, 0))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(0, s(s(y_0)), p_out_ga(0, 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(46) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 3 less nodes.
(47) Complex Obligation (AND)
(48) 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, 0) → U3_GGA(0, 0, p_out_ga(0, 0))
U3_GGA(0, 0, p_out_ga(0, 0)) → U4_GGA(0, 0, 0, p_out_ga(0, 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(49) 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.
(50) 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, 0) → U3_GGA(0, 0, 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.
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(51) 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)
U6_ga(x0, x1)
(52) 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, 0) → U3_GGA(0, 0, 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.
(53) 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.
(54) FALSE
(55) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, s(s(y_0))) → U3_GGA(0, s(s(y_0)), p_out_ga(0, 0))
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, s(s(z0)), 0, p_out_ga(s(s(z0)), x3)) → M_IN_GGA(0, x3)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(56) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U4_GGA(
0,
s(
s(
z0)),
0,
p_out_ga(
s(
s(
z0)),
x3)) →
M_IN_GGA(
0,
x3) we obtained the following new rules [LPAR04]:
U4_GGA(0, s(s(x0)), 0, p_out_ga(s(s(x0)), s(s(y_0)))) → M_IN_GGA(0, s(s(y_0)))
(57) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, s(s(y_0))) → U3_GGA(0, s(s(y_0)), p_out_ga(0, 0))
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(0, s(s(x0)), 0, p_out_ga(s(s(x0)), s(s(y_0)))) → M_IN_GGA(0, s(s(y_0)))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(58) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U3_GGA(0, s(s(x1)), p_out_ga(0, 0)) → U4_GGA(0, s(s(x1)), 0, U6_ga(x1, p_in_ga(s(x1))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
| POL(M_IN_GGA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
| 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(U6_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, s(s(y_0))) → U3_GGA(0, s(s(y_0)), p_out_ga(0, 0))
U4_GGA(0, s(s(x0)), 0, p_out_ga(s(s(x0)), s(s(y_0)))) → M_IN_GGA(0, s(s(y_0)))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(60) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(61) TRUE
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), y1) → U3_GGA(s(s(x0)), y1, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
U4_GGA(s(s(z0)), s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(s(s(z0)), s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(63) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
M_IN_GGA(
s(
s(
x0)),
y1) →
U3_GGA(
s(
s(
x0)),
y1,
U6_ga(
x0,
p_in_ga(
s(
x0)))) we obtained the following new rules [LPAR04]:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(s(s(x0)), 0, U6_ga(x0, p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(0)) → U3_GGA(s(s(x0)), s(0), U6_ga(x0, p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_1))) → U3_GGA(s(s(x0)), s(s(y_1)), U6_ga(x0, p_in_ga(s(x0))))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
U3_GGA(s(s(z0)), s(0), p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), s(0), x1, p_out_ga(s(0), 0))
U4_GGA(s(s(z0)), s(0), z1, p_out_ga(s(0), 0)) → M_IN_GGA(z1, 0)
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(s(s(z0)), s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
M_IN_GGA(s(s(x0)), 0) → U3_GGA(s(s(x0)), 0, U6_ga(x0, p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(0)) → U3_GGA(s(s(x0)), s(0), U6_ga(x0, p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_1))) → U3_GGA(s(s(x0)), s(s(y_1)), U6_ga(x0, p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(65) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 3 less nodes.
(66) Complex Obligation (AND)
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(s(s(z0)), 0, z1, p_out_ga(0, 0)) → M_IN_GGA(z1, 0)
M_IN_GGA(s(s(x0)), 0) → U3_GGA(s(s(x0)), 0, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(68) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U4_GGA(
s(
s(
z0)),
0,
z1,
p_out_ga(
0,
0)) →
M_IN_GGA(
z1,
0) we obtained the following new rules [LPAR04]:
U4_GGA(s(s(x0)), 0, s(s(y_0)), p_out_ga(0, 0)) → M_IN_GGA(s(s(y_0)), 0)
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(s(s(x0)), 0, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(z0)), 0, p_out_ga(s(s(z0)), x1)) → U4_GGA(s(s(z0)), 0, x1, p_out_ga(0, 0))
U4_GGA(s(s(x0)), 0, s(s(y_0)), p_out_ga(0, 0)) → M_IN_GGA(s(s(y_0)), 0)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(70) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U3_GGA(
s(
s(
z0)),
0,
p_out_ga(
s(
s(
z0)),
x1)) →
U4_GGA(
s(
s(
z0)),
0,
x1,
p_out_ga(
0,
0)) we obtained the following new rules [LPAR04]:
U3_GGA(s(s(x0)), 0, p_out_ga(s(s(x0)), s(s(y_1)))) → U4_GGA(s(s(x0)), 0, s(s(y_1)), p_out_ga(0, 0))
(71) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(s(s(x0)), 0, U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(s(s(x0)), 0, s(s(y_0)), p_out_ga(0, 0)) → M_IN_GGA(s(s(y_0)), 0)
U3_GGA(s(s(x0)), 0, p_out_ga(s(s(x0)), s(s(y_1)))) → U4_GGA(s(s(x0)), 0, s(s(y_1)), p_out_ga(0, 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(72) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U4_GGA(s(s(x0)), 0, s(s(y_0)), p_out_ga(0, 0)) → M_IN_GGA(s(s(y_0)), 0)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(M_IN_GGA(x1, x2)) = x1
POL(U3_GGA(x1, x2, x3)) = x3
POL(U4_GGA(x1, x2, x3, x4)) = x3 + x4
POL(U6_ga(x1, x2)) = 1 + x2
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1, x2)) = 1 + x2
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
(73) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(s(s(x0)), 0, U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(x0)), 0, p_out_ga(s(s(x0)), s(s(y_1)))) → U4_GGA(s(s(x0)), 0, s(s(y_1)), p_out_ga(0, 0))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(74) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(75) TRUE
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), s(s(y_1))) → U3_GGA(s(s(x0)), s(s(y_1)), U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(s(s(z0)), s(s(z1)), z2, p_out_ga(s(s(z1)), x3)) → M_IN_GGA(z2, x3)
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(77) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U4_GGA(
s(
s(
z0)),
s(
s(
z1)),
z2,
p_out_ga(
s(
s(
z1)),
x3)) →
M_IN_GGA(
z2,
x3) we obtained the following new rules [LPAR04]:
U4_GGA(s(s(x0)), s(s(x1)), s(s(y_0)), p_out_ga(s(s(x1)), s(s(y_1)))) → M_IN_GGA(s(s(y_0)), s(s(y_1)))
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), s(s(y_1))) → U3_GGA(s(s(x0)), s(s(y_1)), U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(z0)), s(s(x1)), p_out_ga(s(s(z0)), x2)) → U4_GGA(s(s(z0)), s(s(x1)), x2, U6_ga(x1, p_in_ga(s(x1))))
U4_GGA(s(s(x0)), s(s(x1)), s(s(y_0)), p_out_ga(s(s(x1)), s(s(y_1)))) → M_IN_GGA(s(s(y_0)), s(s(y_1)))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(79) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U3_GGA(
s(
s(
z0)),
s(
s(
x1)),
p_out_ga(
s(
s(
z0)),
x2)) →
U4_GGA(
s(
s(
z0)),
s(
s(
x1)),
x2,
U6_ga(
x1,
p_in_ga(
s(
x1)))) we obtained the following new rules [LPAR04]:
U3_GGA(s(s(x0)), s(s(x1)), p_out_ga(s(s(x0)), s(s(y_2)))) → U4_GGA(s(s(x0)), s(s(x1)), s(s(y_2)), U6_ga(x1, p_in_ga(s(x1))))
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), s(s(y_1))) → U3_GGA(s(s(x0)), s(s(y_1)), U6_ga(x0, p_in_ga(s(x0))))
U4_GGA(s(s(x0)), s(s(x1)), s(s(y_0)), p_out_ga(s(s(x1)), s(s(y_1)))) → M_IN_GGA(s(s(y_0)), s(s(y_1)))
U3_GGA(s(s(x0)), s(s(x1)), p_out_ga(s(s(x0)), s(s(y_2)))) → U4_GGA(s(s(x0)), s(s(x1)), s(s(y_2)), U6_ga(x1, p_in_ga(s(x1))))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(81) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U4_GGA(s(s(x0)), s(s(x1)), s(s(y_0)), p_out_ga(s(s(x1)), s(s(y_1)))) → M_IN_GGA(s(s(y_0)), s(s(y_1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
| POL(M_IN_GGA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
| POL(U3_GGA(x1, x2, x3)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(U6_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(U4_GGA(x1, x2, x3, x4)) = | 1 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
| POL(p_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), s(s(y_1))) → U3_GGA(s(s(x0)), s(s(y_1)), U6_ga(x0, p_in_ga(s(x0))))
U3_GGA(s(s(x0)), s(s(x1)), p_out_ga(s(s(x0)), s(s(y_2)))) → U4_GGA(s(s(x0)), s(s(x1)), s(s(y_2)), U6_ga(x1, p_in_ga(s(x1))))
The TRS R consists of the following rules:
p_in_ga(s(0)) → p_out_ga(s(0), 0)
p_in_ga(s(s(X))) → U6_ga(X, p_in_ga(s(X)))
U6_ga(X, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(83) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(84) TRUE
(85) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
m_in: (b,b,f)
p_in: (b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(86) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
(87) 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:
M_IN_GGA(X, 0, Z) → U1_GGA(X, Z, =_in_ag(Z, X))
M_IN_GGA(X, 0, Z) → =_IN_AG(Z, X)
M_IN_GGA(0, Y, Z) → U2_GGA(Y, Z, =_in_ag(Z, 0))
M_IN_GGA(0, Y, Z) → =_IN_AG(Z, 0)
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)
P_IN_GA(s(s(X)), s(Y)) → U6_GA(X, Y, p_in_ga(s(X), Y))
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
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:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x3)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x3)
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
(88) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
M_IN_GGA(X, 0, Z) → U1_GGA(X, Z, =_in_ag(Z, X))
M_IN_GGA(X, 0, Z) → =_IN_AG(Z, X)
M_IN_GGA(0, Y, Z) → U2_GGA(Y, Z, =_in_ag(Z, 0))
M_IN_GGA(0, Y, Z) → =_IN_AG(Z, 0)
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)
P_IN_GA(s(s(X)), s(Y)) → U6_GA(X, Y, p_in_ga(s(X), Y))
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
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:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
M_IN_GGA(
x1,
x2,
x3) =
M_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x3)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x2,
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x3)
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
(89) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.
(90) Complex Obligation (AND)
(91) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
The TRS R consists of the following rules:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(92) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(93) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_GA(s(s(X)), s(Y)) → P_IN_GA(s(X), Y)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(94) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(95) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_GA(s(s(X))) → P_IN_GA(s(X))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(96) 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:
- P_IN_GA(s(s(X))) → P_IN_GA(s(X))
The graph contains the following edges 1 > 1
(97) TRUE
(98) 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:
m_in_gga(X, 0, Z) → U1_gga(X, Z, =_in_ag(Z, X))
=_in_ag(X, X) → =_out_ag(X, X)
U1_gga(X, Z, =_out_ag(Z, X)) → m_out_gga(X, 0, Z)
m_in_gga(0, Y, Z) → U2_gga(Y, Z, =_in_ag(Z, 0))
U2_gga(Y, Z, =_out_ag(Z, 0)) → m_out_gga(0, Y, Z)
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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
The argument filtering Pi contains the following mapping:
m_in_gga(
x1,
x2,
x3) =
m_in_gga(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
m_out_gga(
x1,
x2,
x3) =
m_out_gga(
x3)
U2_gga(
x1,
x2,
x3) =
U2_gga(
x3)
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
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
(99) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(100) 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(0), 0) → p_out_ga(s(0), 0)
p_in_ga(s(s(X)), s(Y)) → U6_ga(X, Y, p_in_ga(s(X), Y))
U6_ga(X, Y, p_out_ga(s(X), Y)) → p_out_ga(s(s(X)), s(Y))
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)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
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
(101) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(102) 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(0)) → p_out_ga(0)
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(103) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
p_in_ga(s(0)) → p_out_ga(0)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(M_IN_GGA(x1, x2)) = x1 + x2
POL(U3_GGA(x1, x2)) = x1 + x2
POL(U4_GGA(x1, x2)) = x1 + x2
POL(U6_ga(x1)) = 1 + x1
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = x1
POL(s(x1)) = 1 + x1
(104) 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(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(105) 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))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(y1, U6_ga(p_in_ga(s(x0))))
(106) 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))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(y1, U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0)
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(107) 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))
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
(108) 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))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(y1, U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0)
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(109) 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.
(110) 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))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(y1, U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(111) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U4_GGA(
A,
p_out_ga(
B)) →
M_IN_GGA(
A,
B) we obtained the following new rules [LPAR04]:
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
(112) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(0, y1) → U3_GGA(y1, p_out_ga(0))
M_IN_GGA(s(s(x0)), y1) → U3_GGA(y1, U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(113) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] 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))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
(114) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), y1) → U3_GGA(y1, U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(y1)) → U4_GGA(y1, p_out_ga(0))
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(115) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
M_IN_GGA(
s(
s(
x0)),
y1) →
U3_GGA(
y1,
U6_ga(
p_in_ga(
s(
x0)))) we obtained the following new rules [LPAR04]:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(0, U6_ga(p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_0))) → U3_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
(116) 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))
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
M_IN_GGA(s(s(x0)), 0) → U3_GGA(0, U6_ga(p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_0))) → U3_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(117) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] 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))
U3_GGA(0, p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), p_out_ga(0))
(118) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(s(s(x0)), p_out_ga(y1)) → U4_GGA(y1, U6_ga(p_in_ga(s(x0))))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
M_IN_GGA(s(s(x0)), 0) → U3_GGA(0, U6_ga(p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_0))) → U3_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
U3_GGA(0, p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), p_out_ga(0))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(119) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U3_GGA(
s(
s(
x0)),
p_out_ga(
y1)) →
U4_GGA(
y1,
U6_ga(
p_in_ga(
s(
x0)))) we obtained the following new rules [LPAR04]:
U3_GGA(s(s(x0)), p_out_ga(0)) → U4_GGA(0, U6_ga(p_in_ga(s(x0))))
U3_GGA(s(s(x0)), p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
(120) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
M_IN_GGA(s(s(x0)), 0) → U3_GGA(0, U6_ga(p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_0))) → U3_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
U3_GGA(0, p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), p_out_ga(0))
U3_GGA(s(s(x0)), p_out_ga(0)) → U4_GGA(0, U6_ga(p_in_ga(s(x0))))
U3_GGA(s(s(x0)), p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(121) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(122) Complex Obligation (AND)
(123) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(0, U6_ga(p_in_ga(s(x0))))
U3_GGA(0, p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), p_out_ga(0))
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
M_IN_GGA(s(s(x0)), s(s(y_0))) → U3_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
U3_GGA(s(s(x0)), p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(124) 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:
U3_GGA(0, p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), p_out_ga(0))
U4_GGA(s(s(y_0)), p_out_ga(x1)) → M_IN_GGA(s(s(y_0)), x1)
U3_GGA(s(s(x0)), p_out_ga(s(s(y_0)))) → U4_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(M_IN_GGA(x1, x2)) = 1 + x1 + x2
POL(U3_GGA(x1, x2)) = 1 + x1 + x2
POL(U4_GGA(x1, x2)) = x1 + x2
POL(U6_ga(x1)) = x1
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 2 + x1
POL(s(x1)) = x1
(125) Obligation:
Q DP problem:
The TRS P consists of the following rules:
M_IN_GGA(s(s(x0)), 0) → U3_GGA(0, U6_ga(p_in_ga(s(x0))))
M_IN_GGA(s(s(x0)), s(s(y_0))) → U3_GGA(s(s(y_0)), U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(126) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(127) TRUE
(128) 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(x1)) → M_IN_GGA(0, x1)
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
U3_GGA(s(s(x0)), p_out_ga(0)) → U4_GGA(0, U6_ga(p_in_ga(s(x0))))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(129) 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:
U3_GGA(s(s(x0)), p_out_ga(0)) → U4_GGA(0, U6_ga(p_in_ga(s(x0))))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(M_IN_GGA(x1, x2)) = 1 + x1 + x2
POL(U3_GGA(x1, x2)) = x1 + x2
POL(U4_GGA(x1, x2)) = x1 + x2
POL(U6_ga(x1)) = x1
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 1 + x1
POL(s(x1)) = x1
(130) 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(x1)) → M_IN_GGA(0, x1)
M_IN_GGA(0, s(s(y_0))) → U3_GGA(s(s(y_0)), p_out_ga(0))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(131) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(132) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
The TRS R consists of the following rules:
p_in_ga(s(s(X))) → U6_ga(p_in_ga(s(X)))
U6_ga(p_out_ga(Y)) → p_out_ga(s(Y))
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(133) 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.
(134) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
M_IN_GGA(0, 0) → U3_GGA(0, p_out_ga(0))
R is empty.
The set Q consists of the following terms:
p_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(135) 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)
U6_ga(x0)
(136) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
U4_GGA(0, p_out_ga(x1)) → M_IN_GGA(0, x1)
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.
(137) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
0,
p_out_ga(
x1)) →
M_IN_GGA(
0,
x1) we obtained the following new rules [LPAR04]:
U4_GGA(0, p_out_ga(0)) → M_IN_GGA(0, 0)
(138) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
M_IN_GGA(0, 0) → U3_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.
(139) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
0,
p_out_ga(
x1)) →
M_IN_GGA(
0,
x1) we obtained the following new rules [LPAR04]:
U4_GGA(0, p_out_ga(0)) → M_IN_GGA(0, 0)
(140) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(0, p_out_ga(0)) → U4_GGA(0, p_out_ga(0))
M_IN_GGA(0, 0) → U3_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.
(141) 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 =
U4_GGA(
0,
p_out_ga(
0)) evaluates to t =
U4_GGA(
0,
p_out_ga(
0))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceU4_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)) at position [] and matcher [ ]
U3_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))
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.
(142) FALSE