(0) Obligation:

Clauses:

factor(.(X, []), X).
factor(.(X, .(Y, Xs)), T) :- ','(times(X, Y, Z), factor(.(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(.(T4, []), T4).
factor1(.(0, .(T19, T12)), T14) :- factor1(.(0, T12), T14).
factor1(.(s(T24), .(T25, T12)), T14) :- times16(T24, T25, X41).
factor1(.(s(T24), .(T25, T12)), T14) :- ','(times16(T24, T25, T28), plus27(T28, T25, X42)).
factor1(.(s(T24), .(T25, T12)), T14) :- ','(times16(T24, T25, T28), ','(plus27(T28, T25, T64), factor1(.(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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → U5_GA(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
FACTOR1_IN_GA(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)
FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U6_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
FACTOR1_IN_GA(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → U5_GA(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
FACTOR1_IN_GA(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)
FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U6_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
FACTOR1_IN_GA(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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:
  • Matcher: [ ]
  • Semiunifier: [ ]




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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(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(.(0, .(T19, T12))) → FACTOR1_IN_GA(.(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(.(0, .(T19, T12))) → FACTOR1_IN_GA(.(0, T12))


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x1 + 2·x2   
POL(0) = 0   
POL(FACTOR1_IN_GA(x1)) = 2·x1   

(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(.(s(T24), .(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(.(T64, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(s(T24), .(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(.(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:
.(x1, x2)  =  .(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(.(s(T24), .(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(.(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.


FACTOR1_IN_GA(.(s(T24), .(T25, T12))) → U7_GA(T25, T12, times16_in_gga(T24, T25))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
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(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(.(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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → U5_GA(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
FACTOR1_IN_GA(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)
FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U6_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
FACTOR1_IN_GA(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → U5_GA(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
FACTOR1_IN_GA(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)
FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U6_GA(T24, T25, T12, T14, times16_in_gga(T24, T25, X41))
FACTOR1_IN_GA(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plus27_out_aga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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:
  • Matcher: [ ]
  • Semiunifier: [ ]




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(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(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(.(0, .(T19, T12))) → FACTOR1_IN_GA(.(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(.(0, .(T19, T12))) → FACTOR1_IN_GA(.(0, T12))


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x1 + x2   
POL(0) = 0   
POL(FACTOR1_IN_GA(x1)) = x1   

(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(.(s(T24), .(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(.(T64, T12), T14)

The TRS R consists of the following rules:

factor1_in_ga(.(T4, []), T4) → factor1_out_ga(.(T4, []), T4)
factor1_in_ga(.(0, .(T19, T12)), T14) → U5_ga(T19, T12, T14, factor1_in_ga(.(0, T12), T14))
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(T25, T12)), T14)
factor1_in_ga(.(s(T24), .(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(.(s(T24), .(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(.(T64, T12), T14))
U10_ga(T24, T25, T12, T14, factor1_out_ga(.(T64, T12), T14)) → factor1_out_ga(.(s(T24), .(T25, T12)), T14)
U5_ga(T19, T12, T14, factor1_out_ga(.(0, T12), T14)) → factor1_out_ga(.(0, .(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
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(.(s(T24), .(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(.(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:
.(x1, x2)  =  .(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(.(s(T24), .(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(.(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.


FACTOR1_IN_GA(.(s(T24), .(T25, T12))) → U7_GA(T24, T25, T12, times16_in_gga(T24, T25))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
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(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(.(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.

(77) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(78) TRUE