(0) Obligation:
Clauses:factor(cons(X, nil), X).
factor(cons(X, cons(Y, Xs)), T) :- ','(times(X, Y, Z), factor(cons(Z, Xs), T)).
times(0, X_, 0).
times(s(X), Y, Z) :- ','(times(X, Y, XY), plus(XY, Y, Z)).
plus(0, X, X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
Queries:
factor(g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:times16(s(T40), T41, X69) :- times16(T40, T41, X68).
times16(s(T40), T41, X69) :- ','(timesc16(T40, T41, T44), plus27(T44, T41, X69)).
plus27(s(T58), T59, s(X96)) :- plus27(T58, T59, X96).
factor1(cons(0, cons(T19, T12)), T14) :- factor1(cons(0, T12), T14).
factor1(cons(s(T24), cons(T25, T12)), T14) :- times16(T24, T25, X41).
factor1(cons(s(T24), cons(T25, T12)), T14) :- ','(timesc16(T24, T25, T28), plus27(T28, T25, X42)).
factor1(cons(s(T24), cons(T25, T12)), T14) :- ','(timesc16(T24, T25, T28), ','(plusc27(T28, T25, T64), factor1(cons(T64, T12), T14))).
Clauses:
factorc1(cons(T4, nil), T4).
factorc1(cons(0, cons(T19, T12)), T14) :- factorc1(cons(0, T12), T14).
factorc1(cons(s(T24), cons(T25, T12)), T14) :- ','(timesc16(T24, T25, T28), ','(plusc27(T28, T25, T64), factorc1(cons(T64, T12), T14))).
timesc16(0, T35, 0).
timesc16(s(T40), T41, X69) :- ','(timesc16(T40, T41, T44), plusc27(T44, T41, X69)).
plusc27(0, T53, T53).
plusc27(s(T58), T59, s(X96)) :- plusc27(T58, T59, X96).
Afs:
factor1(x1, x2) = factor1(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:factor1_in: (b,f)
times16_in: (b,b,f)
timesc16_in: (b,b,f)
plusc27_in: (b,b,f)
plus27_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(0, cons(T19, T12)), T14) → U5_GA(T19, T12, T14, factor1_in_ga(cons(0, T12), T14))
FACTOR1_IN_GA(cons(0, cons(T19, T12)), T14) → FACTOR1_IN_GA(cons(0, T12), T14)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U6_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → TIMES16_IN_GGA(T24, T25, X41)
TIMES16_IN_GGA(s(T40), T41, X69) → U1_GGA(T40, T41, X69, times16_in_gga(T40, T41, X68))
TIMES16_IN_GGA(s(T40), T41, X69) → TIMES16_IN_GGA(T40, T41, X68)
TIMES16_IN_GGA(s(T40), T41, X69) → U2_GGA(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_gga(T44, T41, X69))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → PLUS27_IN_GGA(T44, T41, X69)
PLUS27_IN_GGA(s(T58), T59, s(X96)) → U4_GGA(T58, T59, X96, plus27_in_gga(T58, T59, X96))
PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, timesc16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_gga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → PLUS27_IN_GGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plusc27_in_gga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
0 = 0
s(x1) = s(x1)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
timesc16_in_gga(x1, x2, x3) = timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3) = timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4) = U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3) = plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3) = plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
plus27_in_gga(x1, x2, x3) = plus27_in_gga(x1, x2)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U5_GA(x1, x2, x3, x4) = U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4, x5) = U6_GA(x1, x2, x3, x5)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
PLUS27_IN_GGA(x1, x2, x3) = PLUS27_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4) = U4_GGA(x1, x2, x4)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5) = U8_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5) = U10_GA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(0, cons(T19, T12)), T14) → U5_GA(T19, T12, T14, factor1_in_ga(cons(0, T12), T14))
FACTOR1_IN_GA(cons(0, cons(T19, T12)), T14) → FACTOR1_IN_GA(cons(0, T12), T14)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U6_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → TIMES16_IN_GGA(T24, T25, X41)
TIMES16_IN_GGA(s(T40), T41, X69) → U1_GGA(T40, T41, X69, times16_in_gga(T40, T41, X68))
TIMES16_IN_GGA(s(T40), T41, X69) → TIMES16_IN_GGA(T40, T41, X68)
TIMES16_IN_GGA(s(T40), T41, X69) → U2_GGA(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_gga(T44, T41, X69))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → PLUS27_IN_GGA(T44, T41, X69)
PLUS27_IN_GGA(s(T58), T59, s(X96)) → U4_GGA(T58, T59, X96, plus27_in_gga(T58, T59, X96))
PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, timesc16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_gga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → PLUS27_IN_GGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plusc27_in_gga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
0 = 0
s(x1) = s(x1)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
timesc16_in_gga(x1, x2, x3) = timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3) = timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4) = U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3) = plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3) = plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
plus27_in_gga(x1, x2, x3) = plus27_in_gga(x1, x2)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U5_GA(x1, x2, x3, x4) = U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4, x5) = U6_GA(x1, x2, x3, x5)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
PLUS27_IN_GGA(x1, x2, x3) = PLUS27_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4) = U4_GGA(x1, x2, x4)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5) = U8_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5) = U10_GA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 11 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)
The TRS R consists of the following rules:
timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
timesc16_in_gga(x1, x2, x3) = timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3) = timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4) = U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3) = plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3) = plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
PLUS27_IN_GGA(x1, x2, x3) = PLUS27_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
PLUS27_IN_GGA(x1, x2, x3) = PLUS27_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(11) Obligation:
Q DP problem:The TRS P consists of the following rules:
PLUS27_IN_GGA(s(T58), T59) → PLUS27_IN_GGA(T58, T59)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) 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:
- PLUS27_IN_GGA(s(T58), T59) → PLUS27_IN_GGA(T58, T59)
The graph contains the following edges 1 > 1, 2 >= 2
(13) YES
(14) Obligation:
Pi DP problem:The TRS P consists of the following rules:
TIMES16_IN_GGA(s(T40), T41, X69) → TIMES16_IN_GGA(T40, T41, X68)
The TRS R consists of the following rules:
timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
timesc16_in_gga(x1, x2, x3) = timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3) = timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4) = U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3) = plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3) = plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(16) Obligation:
Pi DP problem:The TRS P consists of the following rules:
TIMES16_IN_GGA(s(T40), T41, X69) → TIMES16_IN_GGA(T40, T41, X68)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(18) Obligation:
Q DP problem:The TRS P consists of the following rules:
TIMES16_IN_GGA(s(T40), T41) → TIMES16_IN_GGA(T40, T41)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) 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:
- TIMES16_IN_GGA(s(T40), T41) → TIMES16_IN_GGA(T40, T41)
The graph contains the following edges 1 > 1, 2 >= 2
(20) YES
(21) Obligation:
Pi DP problem:The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(0, cons(T19, T12)), T14) → FACTOR1_IN_GA(cons(0, T12), T14)
The TRS R consists of the following rules:
timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
0 = 0
s(x1) = s(x1)
timesc16_in_gga(x1, x2, x3) = timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3) = timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4) = U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3) = plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3) = plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(22) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(23) Obligation:
Pi DP problem:The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(0, cons(T19, T12)), T14) → FACTOR1_IN_GA(cons(0, T12), T14)
R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
0 = 0
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(24) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(25) Obligation:
Q DP problem:The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(0, cons(T19, T12))) → FACTOR1_IN_GA(cons(0, T12))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(26) 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:
FACTOR1_IN_GA(cons(0, cons(T19, T12))) → FACTOR1_IN_GA(cons(0, T12))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(FACTOR1_IN_GA(x1)) = 2·x1
POL(cons(x1, x2)) = 1 + x1 + 2·x2
(27) Obligation:
Q DP problem:P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(28) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.(29) YES
(30) Obligation:
Pi DP problem:The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, timesc16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plusc27_in_gga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
0 = 0
s(x1) = s(x1)
timesc16_in_gga(x1, x2, x3) = timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3) = timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4) = U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3) = plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3) = plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(31) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(32) Obligation:
Q DP problem:The TRS P consists of the following rules:
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12))) → U7_GA(T24, T25, T12, timesc16_in_gga(T24, T25))
U7_GA(T24, T25, T12, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, plusc27_in_gga(T28, T25))
U9_GA(T24, T25, T12, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12))
The TRS R consists of the following rules:
timesc16_in_gga(0, T35) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41) → U16_gga(T40, T41, timesc16_in_gga(T40, T41))
U16_gga(T40, T41, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, plusc27_in_gga(T44, T41))
plusc27_in_gga(0, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59) → U18_gga(T58, T59, plusc27_in_gga(T58, T59))
U18_gga(T58, T59, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The set Q consists of the following terms:
timesc16_in_gga(x0, x1)
U16_gga(x0, x1, x2)
plusc27_in_gga(x0, x1)
U18_gga(x0, x1, x2)
U17_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12))) → U7_GA(T24, T25, T12, timesc16_in_gga(T24, T25))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(FACTOR1_IN_GA(x1)) = x1
POL(U16_gga(x1, x2, x3)) = 0
POL(U17_gga(x1, x2, x3)) = 0
POL(U18_gga(x1, x2, x3)) = 1
POL(U7_GA(x1, x2, x3, x4)) = 1 + x3
POL(U9_GA(x1, x2, x3, x4)) = x3 + x4
POL(cons(x1, x2)) = 1 + x2
POL(plusc27_in_gga(x1, x2)) = 1
POL(plusc27_out_gga(x1, x2, x3)) = 1
POL(s(x1)) = 0
POL(timesc16_in_gga(x1, x2)) = 0
POL(timesc16_out_gga(x1, x2, x3)) = 0
The following usable rules [FROCOS05] were oriented:
plusc27_in_gga(0, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59) → U18_gga(T58, T59, plusc27_in_gga(T58, T59))
U18_gga(T58, T59, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
(34) Obligation:
Q DP problem:The TRS P consists of the following rules:
U7_GA(T24, T25, T12, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, plusc27_in_gga(T28, T25))
U9_GA(T24, T25, T12, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12))
The TRS R consists of the following rules:
timesc16_in_gga(0, T35) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41) → U16_gga(T40, T41, timesc16_in_gga(T40, T41))
U16_gga(T40, T41, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, plusc27_in_gga(T44, T41))
plusc27_in_gga(0, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59) → U18_gga(T58, T59, plusc27_in_gga(T58, T59))
U18_gga(T58, T59, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)
The set Q consists of the following terms:
timesc16_in_gga(x0, x1)
U16_gga(x0, x1, x2)
plusc27_in_gga(x0, x1)
U18_gga(x0, x1, x2)
U17_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.