(0) Obligation:
Clauses:
times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, Z) :- ','(!, eq(Z, 0)).
mult(s(X), Y, 0, Z) :- ','(!, mult(X, Y, Y, Z)).
mult(X, Y, W, s(Z)) :- ','(p(W, P), mult(X, Y, P, Z)).
p(0, 0).
p(s(X), X).
eq(X, X).
Queries:
times(g,g,a).
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, Z) :- eq(Z, 0).
mult(s(X), Y, 0, Z) :- mult(X, Y, Y, Z).
mult(X, Y, W, s(Z)) :- ','(p(W, P), mult(X, Y, P, Z)).
p(0, 0).
p(s(X), X).
eq(X, X).
Queries:
times(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:
times_in: (b,b,f)
mult_in: (b,b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
(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:
TIMES_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
TIMES_IN_GGA(X, Y, Z) → MULT_IN_GGGA(X, Y, 0, Z)
MULT_IN_GGGA(0, Y, 0, Z) → U2_GGGA(Y, Z, eq_in_ag(Z, 0))
MULT_IN_GGGA(0, Y, 0, Z) → EQ_IN_AG(Z, 0)
MULT_IN_GGGA(s(X), Y, 0, Z) → U3_GGGA(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, Z)
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
MULT_IN_GGGA(X, Y, W, s(Z)) → P_IN_GA(W, P)
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → U5_GGGA(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x4)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U2_GGGA(
x1,
x2,
x3) =
U2_GGGA(
x3)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGGA(
x1,
x2,
x3,
x4) =
U3_GGGA(
x4)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
x5)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U5_GGGA(
x1,
x2,
x3,
x4,
x5) =
U5_GGGA(
x5)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TIMES_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
TIMES_IN_GGA(X, Y, Z) → MULT_IN_GGGA(X, Y, 0, Z)
MULT_IN_GGGA(0, Y, 0, Z) → U2_GGGA(Y, Z, eq_in_ag(Z, 0))
MULT_IN_GGGA(0, Y, 0, Z) → EQ_IN_AG(Z, 0)
MULT_IN_GGGA(s(X), Y, 0, Z) → U3_GGGA(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, Z)
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
MULT_IN_GGGA(X, Y, W, s(Z)) → P_IN_GA(W, P)
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → U5_GGGA(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x4)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U2_GGGA(
x1,
x2,
x3) =
U2_GGGA(
x3)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGGA(
x1,
x2,
x3,
x4) =
U3_GGGA(
x4)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
x5)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U5_GGGA(
x1,
x2,
x3,
x4,
x5) =
U5_GGGA(
x5)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 7 less nodes.
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, Z)
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
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:
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, 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
s(
x1) =
s(
x1)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x2)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
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:
MULT_IN_GGGA(X, Y, W) → U4_GGGA(X, Y, p_in_ga(W))
U4_GGGA(X, Y, p_out_ga(P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(s(X), Y, 0) → MULT_IN_GGGA(X, Y, Y)
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0)
p_in_ga(s(X)) → p_out_ga(X)
The set Q consists of the following terms:
p_in_ga(x0)
We have to consider all (P,Q,R)-chains.
(13) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MULT_IN_GGGA(s(X), Y, 0) → MULT_IN_GGGA(X, Y, Y)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(MULT_IN_GGGA(x1, x2, x3)) = x1
POL(U4_GGGA(x1, x2, x3)) = x1
POL(p_in_ga(x1)) = 0
POL(p_out_ga(x1)) = 0
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
none
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W) → U4_GGGA(X, Y, p_in_ga(W))
U4_GGGA(X, Y, p_out_ga(P)) → MULT_IN_GGGA(X, Y, P)
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0)
p_in_ga(s(X)) → p_out_ga(X)
The set Q consists of the following terms:
p_in_ga(x0)
We have to consider all (P,Q,R)-chains.
(15) 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(MULT_IN_GGGA(x1, x2, x3)) = x1 + x2 + x3
POL(U4_GGGA(x1, x2, x3)) = x1 + x2 + x3
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 2·x1
POL(s(x1)) = 2·x1
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W) → U4_GGGA(X, Y, p_in_ga(W))
U4_GGGA(X, Y, p_out_ga(P)) → MULT_IN_GGGA(X, Y, P)
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
MULT_IN_GGGA(
X,
Y,
W) →
U4_GGGA(
X,
Y,
p_in_ga(
W)) at position [2] we obtained the following new rules [LPAR04]:
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, p_out_ga(0))
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGGA(X, Y, p_out_ga(P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, 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_GGGA(X, Y, p_out_ga(P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, 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_GGGA(X, Y, p_out_ga(P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, 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_GGGA(
X,
Y,
p_out_ga(
P)) →
MULT_IN_GGGA(
X,
Y,
P) we obtained the following new rules [LPAR04]:
U4_GGGA(z0, z1, p_out_ga(0)) → MULT_IN_GGGA(z0, z1, 0)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, p_out_ga(0))
U4_GGGA(z0, z1, p_out_ga(0)) → MULT_IN_GGGA(z0, z1, 0)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(25) 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_GGGA(
z0,
z1,
p_out_ga(
0)) evaluates to t =
U4_GGGA(
z0,
z1,
p_out_ga(
0))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceU4_GGGA(z0, z1, p_out_ga(0)) →
MULT_IN_GGGA(
z0,
z1,
0)
with rule
U4_GGGA(
z0',
z1',
p_out_ga(
0)) →
MULT_IN_GGGA(
z0',
z1',
0) at position [] and matcher [
z0' /
z0,
z1' /
z1]
MULT_IN_GGGA(z0, z1, 0) →
U4_GGGA(
z0,
z1,
p_out_ga(
0))
with rule
MULT_IN_GGGA(
y0,
y1,
0) →
U4_GGGA(
y0,
y1,
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.
(26) FALSE
(27) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
times_in: (b,b,f)
mult_in: (b,b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x1,
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x1,
x2,
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x3,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x1,
x2,
x3,
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(28) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x1,
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x1,
x2,
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x3,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x1,
x2,
x3,
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
(29) 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:
TIMES_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
TIMES_IN_GGA(X, Y, Z) → MULT_IN_GGGA(X, Y, 0, Z)
MULT_IN_GGGA(0, Y, 0, Z) → U2_GGGA(Y, Z, eq_in_ag(Z, 0))
MULT_IN_GGGA(0, Y, 0, Z) → EQ_IN_AG(Z, 0)
MULT_IN_GGGA(s(X), Y, 0, Z) → U3_GGGA(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, Z)
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
MULT_IN_GGGA(X, Y, W, s(Z)) → P_IN_GA(W, P)
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → U5_GGGA(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x1,
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x1,
x2,
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x3,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x1,
x2,
x3,
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U2_GGGA(
x1,
x2,
x3) =
U2_GGGA(
x1,
x3)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGGA(
x1,
x2,
x3,
x4) =
U3_GGGA(
x1,
x2,
x4)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
x3,
x5)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U5_GGGA(
x1,
x2,
x3,
x4,
x5) =
U5_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(30) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TIMES_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
TIMES_IN_GGA(X, Y, Z) → MULT_IN_GGGA(X, Y, 0, Z)
MULT_IN_GGGA(0, Y, 0, Z) → U2_GGGA(Y, Z, eq_in_ag(Z, 0))
MULT_IN_GGGA(0, Y, 0, Z) → EQ_IN_AG(Z, 0)
MULT_IN_GGGA(s(X), Y, 0, Z) → U3_GGGA(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, Z)
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
MULT_IN_GGGA(X, Y, W, s(Z)) → P_IN_GA(W, P)
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → U5_GGGA(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x1,
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x1,
x2,
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x3,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x1,
x2,
x3,
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U2_GGGA(
x1,
x2,
x3) =
U2_GGGA(
x1,
x3)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGGA(
x1,
x2,
x3,
x4) =
U3_GGGA(
x1,
x2,
x4)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
x3,
x5)
P_IN_GA(
x1,
x2) =
P_IN_GA(
x1)
U5_GGGA(
x1,
x2,
x3,
x4,
x5) =
U5_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(31) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 7 less nodes.
(32) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, Z)
The TRS R consists of the following rules:
times_in_gga(X, Y, Z) → U1_gga(X, Y, Z, mult_in_ggga(X, Y, 0, Z))
mult_in_ggga(0, Y, 0, Z) → U2_ggga(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggga(Y, Z, eq_out_ag(Z, 0)) → mult_out_ggga(0, Y, 0, Z)
mult_in_ggga(s(X), Y, 0, Z) → U3_ggga(X, Y, Z, mult_in_ggga(X, Y, Y, Z))
mult_in_ggga(X, Y, W, s(Z)) → U4_ggga(X, Y, W, Z, p_in_ga(W, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U4_ggga(X, Y, W, Z, p_out_ga(W, P)) → U5_ggga(X, Y, W, Z, mult_in_ggga(X, Y, P, Z))
U5_ggga(X, Y, W, Z, mult_out_ggga(X, Y, P, Z)) → mult_out_ggga(X, Y, W, s(Z))
U3_ggga(X, Y, Z, mult_out_ggga(X, Y, Y, Z)) → mult_out_ggga(s(X), Y, 0, Z)
U1_gga(X, Y, Z, mult_out_ggga(X, Y, 0, Z)) → times_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
mult_in_ggga(
x1,
x2,
x3,
x4) =
mult_in_ggga(
x1,
x2,
x3)
0 =
0
U2_ggga(
x1,
x2,
x3) =
U2_ggga(
x1,
x3)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
mult_out_ggga(
x1,
x2,
x3,
x4) =
mult_out_ggga(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
U3_ggga(
x1,
x2,
x3,
x4) =
U3_ggga(
x1,
x2,
x4)
U4_ggga(
x1,
x2,
x3,
x4,
x5) =
U4_ggga(
x1,
x2,
x3,
x5)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
U5_ggga(
x1,
x2,
x3,
x4,
x5) =
U5_ggga(
x1,
x2,
x3,
x5)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(33) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(34) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W, s(Z)) → U4_GGGA(X, Y, W, Z, p_in_ga(W, P))
U4_GGGA(X, Y, W, Z, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P, Z)
MULT_IN_GGGA(s(X), Y, 0, Z) → MULT_IN_GGGA(X, Y, Y, 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
s(
x1) =
s(
x1)
p_in_ga(
x1,
x2) =
p_in_ga(
x1)
p_out_ga(
x1,
x2) =
p_out_ga(
x1,
x2)
MULT_IN_GGGA(
x1,
x2,
x3,
x4) =
MULT_IN_GGGA(
x1,
x2,
x3)
U4_GGGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(35) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W) → U4_GGGA(X, Y, W, p_in_ga(W))
U4_GGGA(X, Y, W, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(s(X), Y, 0) → MULT_IN_GGGA(X, Y, Y)
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
The set Q consists of the following terms:
p_in_ga(x0)
We have to consider all (P,Q,R)-chains.
(37) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MULT_IN_GGGA(s(X), Y, 0) → MULT_IN_GGGA(X, Y, Y)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(MULT_IN_GGGA(x1, x2, x3)) = x1
POL(U4_GGGA(x1, x2, x3, x4)) = x1
POL(p_in_ga(x1)) = 0
POL(p_out_ga(x1, x2)) = 0
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
none
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(X, Y, W) → U4_GGGA(X, Y, W, p_in_ga(W))
U4_GGGA(X, Y, W, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P)
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
The set Q consists of the following terms:
p_in_ga(x0)
We have to consider all (P,Q,R)-chains.
(39) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
MULT_IN_GGGA(
X,
Y,
W) →
U4_GGGA(
X,
Y,
W,
p_in_ga(
W)) at position [3] we obtained the following new rules [LPAR04]:
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, 0, p_out_ga(0, 0))
MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGGA(X, Y, W, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, 0, p_out_ga(0, 0))
MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
The TRS R consists of the following rules:
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
The set Q consists of the following terms:
p_in_ga(x0)
We have to consider all (P,Q,R)-chains.
(41) 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.
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGGA(X, Y, W, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, 0, p_out_ga(0, 0))
MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
R is empty.
The set Q consists of the following terms:
p_in_ga(x0)
We have to consider all (P,Q,R)-chains.
(43) 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)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGGA(X, Y, W, p_out_ga(W, P)) → MULT_IN_GGGA(X, Y, P)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, 0, p_out_ga(0, 0))
MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(45) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGGA(
X,
Y,
W,
p_out_ga(
W,
P)) →
MULT_IN_GGGA(
X,
Y,
P) we obtained the following new rules [LPAR04]:
U4_GGGA(z0, z1, 0, p_out_ga(0, 0)) → MULT_IN_GGGA(z0, z1, 0)
U4_GGGA(z0, z1, s(z2), p_out_ga(s(z2), z2)) → MULT_IN_GGGA(z0, z1, z2)
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, 0, p_out_ga(0, 0))
MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
U4_GGGA(z0, z1, 0, p_out_ga(0, 0)) → MULT_IN_GGGA(z0, z1, 0)
U4_GGGA(z0, z1, s(z2), p_out_ga(s(z2), z2)) → MULT_IN_GGGA(z0, z1, z2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(47) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(48) Complex Obligation (AND)
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGGA(z0, z1, 0, p_out_ga(0, 0)) → MULT_IN_GGGA(z0, z1, 0)
MULT_IN_GGGA(y0, y1, 0) → U4_GGGA(y0, y1, 0, p_out_ga(0, 0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(50) 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 =
MULT_IN_GGGA(
y0,
y1,
0) evaluates to t =
MULT_IN_GGGA(
y0,
y1,
0)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequenceMULT_IN_GGGA(y0, y1, 0) →
U4_GGGA(
y0,
y1,
0,
p_out_ga(
0,
0))
with rule
MULT_IN_GGGA(
y0',
y1',
0) →
U4_GGGA(
y0',
y1',
0,
p_out_ga(
0,
0)) at position [] and matcher [
y0' /
y0,
y1' /
y1]
U4_GGGA(y0, y1, 0, p_out_ga(0, 0)) →
MULT_IN_GGGA(
y0,
y1,
0)
with rule
U4_GGGA(
z0,
z1,
0,
p_out_ga(
0,
0)) →
MULT_IN_GGGA(
z0,
z1,
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.
(51) FALSE
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
U4_GGGA(z0, z1, s(z2), p_out_ga(s(z2), z2)) → MULT_IN_GGGA(z0, z1, z2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(53) 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:
- U4_GGGA(z0, z1, s(z2), p_out_ga(s(z2), z2)) → MULT_IN_GGGA(z0, z1, z2)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 3
- MULT_IN_GGGA(y0, y1, s(x0)) → U4_GGGA(y0, y1, s(x0), p_out_ga(s(x0), x0))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
(54) TRUE