(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(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
=(X, X).
Queries:
q(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(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
=(X, X).
Queries:
q(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:
q_in: (b,b,f)
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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
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)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gga(
x1,
x2,
x3) =
q_out_gga
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
q_in_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
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)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gga(
x1,
x2,
x3) =
q_out_gga
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
Q_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, m_in_gga(X, Y, Z))
Q_IN_GGA(X, Y, Z) → M_IN_GGA(X, Y, Z)
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)
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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
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)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gga(
x1,
x2,
x3) =
q_out_gga
Q_IN_GGA(
x1,
x2,
x3) =
Q_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_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)
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
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
Q_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, m_in_gga(X, Y, Z))
Q_IN_GGA(X, Y, Z) → M_IN_GGA(X, Y, Z)
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)
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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
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)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gga(
x1,
x2,
x3) =
q_out_gga
Q_IN_GGA(
x1,
x2,
x3) =
Q_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_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)
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
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 9 less nodes.
(8) 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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
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)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x4,
x5)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
q_out_gga(
x1,
x2,
x3) =
q_out_gga
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
(9) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(10) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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
(11) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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.
(13) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
No dependency pairs are removed.
The following rules are removed from R:
p_in_ga(s(X)) → p_out_ga(X)
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(0) = 0
POL(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
(14) 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.
(15) 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))
(16) 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.
(17) 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))
(18) 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.
(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(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.
(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(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.
(23) 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)
(24) 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.
(25) 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))
(26) 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.
(27) 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))
(28) 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.
(29) 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)
(30) 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.
(31) 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.
(32) FALSE
(33) 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,f)
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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
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)
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_gga(
x1,
x2,
x3) =
q_out_gga(
x1,
x2)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(34) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
q_in_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
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)
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_gga(
x1,
x2,
x3) =
q_out_gga(
x1,
x2)
(35) 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_GGA(X, Y, Z) → U6_GGA(X, Y, Z, m_in_gga(X, Y, Z))
Q_IN_GGA(X, Y, Z) → M_IN_GGA(X, Y, Z)
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)
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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
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)
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_gga(
x1,
x2,
x3) =
q_out_gga(
x1,
x2)
Q_IN_GGA(
x1,
x2,
x3) =
Q_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_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)
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
(36) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
Q_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, m_in_gga(X, Y, Z))
Q_IN_GGA(X, Y, Z) → M_IN_GGA(X, Y, Z)
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)
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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
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)
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_gga(
x1,
x2,
x3) =
q_out_gga(
x1,
x2)
Q_IN_GGA(
x1,
x2,
x3) =
Q_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_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)
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
(37) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 9 less nodes.
(38) 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_gga(X, Y, Z) → U6_gga(X, Y, Z, m_in_gga(X, Y, Z))
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(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)
U6_gga(X, Y, Z, m_out_gga(X, Y, Z)) → q_out_gga(X, Y, Z)
q_in_gga(X, Y, Z) → q_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
q_in_gga(
x1,
x2,
x3) =
q_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
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)
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_gga(
x1,
x2,
x3) =
q_out_gga(
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
(39) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(40) 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
(41) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(42) 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.
(43) 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))
(44) 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.
(45) 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))
(46) 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.
(47) 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.
(48) 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.
(49) 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)
(50) 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.
(51) 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)
(52) 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.
(53) 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))
(54) 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.
(55) 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))
(56) 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.
(57) 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)
(58) 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.
(59) 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)
(60) 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.
(61) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(62) Complex Obligation (AND)
(63) 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.
(64) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U4_GGA(0, s(z0), 0, p_out_ga(s(z0), z0)) → M_IN_GGA(0, z0)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(M_IN_GGA(x1, x2)) = x2
POL(U3_GGA(x1, x2, x3)) = x2
POL(U4_GGA(x1, x2, x3, x4)) = x2
POL(p_out_ga(x1, x2)) = 0
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
none
(65) 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))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(66) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(67) 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.
(68) 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))
(69) 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.
(70) 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))
(71) 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.
(72) 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.
(73) FALSE
(74) 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.
(75) 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
(76) TRUE