(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) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:times16(0, T35, 0).
times16(s(T40), T41, X69) :- times16(T40, T41, X68).
times16(s(T40), T41, X69) :- ','(times16(T40, T41, T44), plus27(T44, T41, X69)).
plus27(0, T53, T53).
plus27(s(T58), T59, s(X96)) :- plus27(T58, T59, X96).
factor1(cons(T4, nil), T4).
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) :- ','(times16(T24, T25, T28), plus27(T28, T25, X42)).
factor1(cons(s(T24), cons(T25, T12)), T14) :- ','(times16(T24, T25, T28), ','(plus27(T28, T25, T64), factor1(cons(T64, T12), T14))).
Queries:
factor1(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:factor1_in: (b,f)
times16_in: (b,b,f)
plus27_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
(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:
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, times16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_aga(T44, T41, X69))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → PLUS27_IN_AGA(T44, T41, X69)
PLUS27_IN_AGA(s(T58), T59, s(X96)) → U4_AGA(T58, T59, X96, plus27_in_aga(T58, T59, X96))
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → PLUS27_IN_AGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U5_GA(x1, x2, x3, x4) = U5_GA(x4)
U6_GA(x1, x2, x3, x4, x5) = U6_GA(x5)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)
PLUS27_IN_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
U4_AGA(x1, x2, x3, x4) = U4_AGA(x4)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5) = U8_GA(x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x3, x5)
U10_GA(x1, x2, x3, x4, x5) = U10_GA(x5)
We have to consider all (P,R,Pi)-chains
(6) 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, times16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_aga(T44, T41, X69))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → PLUS27_IN_AGA(T44, T41, X69)
PLUS27_IN_AGA(s(T58), T59, s(X96)) → U4_AGA(T58, T59, X96, plus27_in_aga(T58, T59, X96))
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → PLUS27_IN_AGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U5_GA(x1, x2, x3, x4) = U5_GA(x4)
U6_GA(x1, x2, x3, x4, x5) = U6_GA(x5)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)
PLUS27_IN_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
U4_AGA(x1, x2, x3, x4) = U4_AGA(x4)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5) = U8_GA(x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x3, x5)
U10_GA(x1, x2, x3, x4, x5) = U10_GA(x5)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 11 less nodes.(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
PLUS27_IN_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(11) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
PLUS27_IN_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(13) Obligation:
Q DP problem:The TRS P consists of the following rules:
PLUS27_IN_AGA(T59) → PLUS27_IN_AGA(T59)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.Found a loop by semiunifying a rule from P directly.
s = PLUS27_IN_AGA(T59) evaluates to t =PLUS27_IN_AGA(T59)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from PLUS27_IN_AGA(T59) to PLUS27_IN_AGA(T59).
(15) NO
(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)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(18) Obligation:
Pi DP problem:The TRS P consists of the following rules:
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
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(20) Obligation:
Q DP problem:The TRS P consists of the following rules:
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.
(21) 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
(22) YES
(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)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(24) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(25) 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
(26) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(27) 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.
(28) 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)) = x1
POL(cons(x1, x2)) = 1 + x1 + x2
(29) Obligation:
Q DP problem:P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(30) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.(31) YES
(32) 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, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
U7_ga(x1, x2, x3, x4, x5) = U7_ga(x2, x3, x5)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x3, x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(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:
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_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)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_gga
U1_gga(x1, x2, x3, x4) = U1_gga(x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
plus27_in_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(x4)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5) = U7_GA(x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(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:
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12))) → U7_GA(T25, T12, times16_in_gga(T24, T25))
U7_GA(T25, T12, times16_out_gga) → U9_GA(T12, plus27_in_aga(T25))
U9_GA(T12, plus27_out_aga(T28, T64)) → FACTOR1_IN_GA(cons(T64, T12))
The TRS R consists of the following rules:
times16_in_gga(0, T35) → times16_out_gga
times16_in_gga(s(T40), T41) → U1_gga(times16_in_gga(T40, T41))
times16_in_gga(s(T40), T41) → U2_gga(T41, times16_in_gga(T40, T41))
plus27_in_aga(T53) → plus27_out_aga(0, T53)
plus27_in_aga(T59) → U4_aga(plus27_in_aga(T59))
U1_gga(times16_out_gga) → times16_out_gga
U2_gga(T41, times16_out_gga) → U3_gga(plus27_in_aga(T41))
U4_aga(plus27_out_aga(T58, X96)) → plus27_out_aga(s(T58), s(X96))
U3_gga(plus27_out_aga(T44, X69)) → times16_out_gga
The set Q consists of the following terms:
times16_in_gga(x0, x1)
plus27_in_aga(x0)
U1_gga(x0)
U2_gga(x0, x1)
U4_aga(x0)
U3_gga(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.
The remaining pairs can at least be oriented weakly.
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12))) → U7_GA(T25, T12, times16_in_gga(T24, T25))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(FACTOR1_IN_GA(x1)) = x1
POL(U1_gga(x1)) = 0
POL(U2_gga(x1, x2)) = 0
POL(U3_gga(x1)) = 0
POL(U4_aga(x1)) = 0
POL(U7_GA(x1, x2, x3)) = 1 + x2
POL(U9_GA(x1, x2)) = 1 + x1
POL(cons(x1, x2)) = 1 + x2
POL(plus27_in_aga(x1)) = 0
POL(plus27_out_aga(x1, x2)) = 0
POL(s(x1)) = 0
POL(times16_in_gga(x1, x2)) = 0
POL(times16_out_gga) = 0
The following usable rules [FROCOS05] were oriented: none
(38) Obligation:
Q DP problem:The TRS P consists of the following rules:
U7_GA(T25, T12, times16_out_gga) → U9_GA(T12, plus27_in_aga(T25))
U9_GA(T12, plus27_out_aga(T28, T64)) → FACTOR1_IN_GA(cons(T64, T12))
The TRS R consists of the following rules:
times16_in_gga(0, T35) → times16_out_gga
times16_in_gga(s(T40), T41) → U1_gga(times16_in_gga(T40, T41))
times16_in_gga(s(T40), T41) → U2_gga(T41, times16_in_gga(T40, T41))
plus27_in_aga(T53) → plus27_out_aga(0, T53)
plus27_in_aga(T59) → U4_aga(plus27_in_aga(T59))
U1_gga(times16_out_gga) → times16_out_gga
U2_gga(T41, times16_out_gga) → U3_gga(plus27_in_aga(T41))
U4_aga(plus27_out_aga(T58, X96)) → plus27_out_aga(s(T58), s(X96))
U3_gga(plus27_out_aga(T44, X69)) → times16_out_gga
The set Q consists of the following terms:
times16_in_gga(x0, x1)
plus27_in_aga(x0)
U1_gga(x0)
U2_gga(x0, x1)
U4_aga(x0)
U3_gga(x0)
We have to consider all (P,Q,R)-chains.
(39) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.(40) TRUE
(41) PrologToPiTRSProof (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)
plus27_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(42) Obligation:
Pi-finite rewrite system:The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
(43) 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:
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, times16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_aga(T44, T41, X69))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → PLUS27_IN_AGA(T44, T41, X69)
PLUS27_IN_AGA(s(T58), T59, s(X96)) → U4_AGA(T58, T59, X96, plus27_in_aga(T58, T59, X96))
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → PLUS27_IN_AGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
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_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
U4_AGA(x1, x2, x3, x4) = U4_AGA(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
(44) 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, times16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_aga(T44, T41, X69))
U2_GGA(T40, T41, X69, times16_out_gga(T40, T41, T44)) → PLUS27_IN_AGA(T44, T41, X69)
PLUS27_IN_AGA(s(T58), T59, s(X96)) → U4_AGA(T58, T59, X96, plus27_in_aga(T58, T59, X96))
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
FACTOR1_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → PLUS27_IN_AGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
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_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
U4_AGA(x1, x2, x3, x4) = U4_AGA(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
(45) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 11 less nodes.(46) Complex Obligation (AND)
(47) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
PLUS27_IN_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
We have to consider all (P,R,Pi)-chains
(48) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(49) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS27_IN_AGA(s(T58), T59, s(X96)) → PLUS27_IN_AGA(T58, T59, X96)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
PLUS27_IN_AGA(x1, x2, x3) = PLUS27_IN_AGA(x2)
We have to consider all (P,R,Pi)-chains
(50) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(51) Obligation:
Q DP problem:The TRS P consists of the following rules:
PLUS27_IN_AGA(T59) → PLUS27_IN_AGA(T59)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(52) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.Found a loop by semiunifying a rule from P directly.
s = PLUS27_IN_AGA(T59) evaluates to t =PLUS27_IN_AGA(T59)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from PLUS27_IN_AGA(T59) to PLUS27_IN_AGA(T59).
(53) NO
(54) 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:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
TIMES16_IN_GGA(x1, x2, x3) = TIMES16_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(55) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(56) Obligation:
Pi DP problem:The TRS P consists of the following rules:
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
(57) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(58) Obligation:
Q DP problem:The TRS P consists of the following rules:
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.
(59) 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
(60) YES
(61) 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:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
FACTOR1_IN_GA(x1, x2) = FACTOR1_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(62) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(63) 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
(64) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(65) 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.
(66) 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)) = x1
POL(cons(x1, x2)) = 1 + x1 + x2
(67) Obligation:
Q DP problem:P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(68) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.(69) YES
(70) 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, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
factor1_in_ga(cons(T4, nil), T4) → factor1_out_ga(cons(T4, nil), T4)
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(s(T24), cons(T25, T12)), T14) → U6_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41, X69)
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U6_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, X41)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
factor1_in_ga(cons(s(T24), cons(T25, T12)), T14) → U7_ga(T24, T25, T12, T14, times16_in_gga(T24, T25, T28))
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U8_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, X42))
U8_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, X42)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U7_ga(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_ga(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_ga(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → U10_ga(T24, T25, T12, T14, factor1_in_ga(cons(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(cons(T64, T12), T14)) → factor1_out_ga(cons(s(T24), cons(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(cons(0, T12), T14)) → factor1_out_ga(cons(0, cons(T19, T12)), T14)
The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2) = factor1_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factor1_out_ga(x1, x2) = factor1_out_ga(x1)
0 = 0
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x2, x4)
s(x1) = s(x1)
U6_ga(x1, x2, x3, x4, x5) = U6_ga(x1, x2, x3, x5)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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)
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
(71) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(72) 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, times16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, times16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plus27_in_aga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12), T14)
The TRS R consists of the following rules:
times16_in_gga(0, T35, 0) → times16_out_gga(0, T35, 0)
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) → U2_gga(T40, T41, X69, times16_in_gga(T40, T41, T44))
plus27_in_aga(0, T53, T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(s(T58), T59, s(X96)) → U4_aga(T58, T59, X96, plus27_in_aga(T58, T59, X96))
U1_gga(T40, T41, X69, times16_out_gga(T40, T41, X68)) → times16_out_gga(s(T40), T41, X69)
U2_gga(T40, T41, X69, times16_out_gga(T40, T41, T44)) → U3_gga(T40, T41, X69, plus27_in_aga(T44, T41, X69))
U4_aga(T58, T59, X96, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, X69, plus27_out_aga(T44, T41, X69)) → times16_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)
times16_in_gga(x1, x2, x3) = times16_in_gga(x1, x2)
times16_out_gga(x1, x2, x3) = times16_out_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_aga(x1, x2, x3) = plus27_in_aga(x2)
plus27_out_aga(x1, x2, x3) = plus27_out_aga(x1, x2, x3)
U4_aga(x1, x2, x3, x4) = U4_aga(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
(73) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(74) 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, times16_in_gga(T24, T25))
U7_GA(T24, T25, T12, times16_out_gga(T24, T25)) → U9_GA(T24, T25, T12, plus27_in_aga(T25))
U9_GA(T24, T25, T12, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12))
The TRS R consists of the following rules:
times16_in_gga(0, T35) → times16_out_gga(0, T35)
times16_in_gga(s(T40), T41) → U1_gga(T40, T41, times16_in_gga(T40, T41))
times16_in_gga(s(T40), T41) → U2_gga(T40, T41, times16_in_gga(T40, T41))
plus27_in_aga(T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(T59) → U4_aga(T59, plus27_in_aga(T59))
U1_gga(T40, T41, times16_out_gga(T40, T41)) → times16_out_gga(s(T40), T41)
U2_gga(T40, T41, times16_out_gga(T40, T41)) → U3_gga(T40, T41, plus27_in_aga(T41))
U4_aga(T59, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41)
The set Q consists of the following terms:
times16_in_gga(x0, x1)
plus27_in_aga(x0)
U1_gga(x0, x1, x2)
U2_gga(x0, x1, x2)
U4_aga(x0, x1)
U3_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(75) 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, times16_in_gga(T24, T25))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(FACTOR1_IN_GA(x1)) = x1
POL(U1_gga(x1, x2, x3)) = 0
POL(U2_gga(x1, x2, x3)) = 0
POL(U3_gga(x1, x2, x3)) = 0
POL(U4_aga(x1, x2)) = 0
POL(U7_GA(x1, x2, x3, x4)) = 1 + x3
POL(U9_GA(x1, x2, x3, x4)) = 1 + x3
POL(cons(x1, x2)) = 1 + x2
POL(plus27_in_aga(x1)) = 0
POL(plus27_out_aga(x1, x2, x3)) = 0
POL(s(x1)) = 0
POL(times16_in_gga(x1, x2)) = 0
POL(times16_out_gga(x1, x2)) = 0
The following usable rules [FROCOS05] were oriented: none
(76) Obligation:
Q DP problem:The TRS P consists of the following rules:
U7_GA(T24, T25, T12, times16_out_gga(T24, T25)) → U9_GA(T24, T25, T12, plus27_in_aga(T25))
U9_GA(T24, T25, T12, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(cons(T64, T12))
The TRS R consists of the following rules:
times16_in_gga(0, T35) → times16_out_gga(0, T35)
times16_in_gga(s(T40), T41) → U1_gga(T40, T41, times16_in_gga(T40, T41))
times16_in_gga(s(T40), T41) → U2_gga(T40, T41, times16_in_gga(T40, T41))
plus27_in_aga(T53) → plus27_out_aga(0, T53, T53)
plus27_in_aga(T59) → U4_aga(T59, plus27_in_aga(T59))
U1_gga(T40, T41, times16_out_gga(T40, T41)) → times16_out_gga(s(T40), T41)
U2_gga(T40, T41, times16_out_gga(T40, T41)) → U3_gga(T40, T41, plus27_in_aga(T41))
U4_aga(T59, plus27_out_aga(T58, T59, X96)) → plus27_out_aga(s(T58), T59, s(X96))
U3_gga(T40, T41, plus27_out_aga(T44, T41, X69)) → times16_out_gga(s(T40), T41)
The set Q consists of the following terms:
times16_in_gga(x0, x1)
plus27_in_aga(x0)
U1_gga(x0, x1, x2)
U2_gga(x0, x1, x2)
U4_aga(x0, x1)
U3_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.