Left Termination of the query pattern factor_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇐)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇐)
        ↳25 QDP
        ↳26 MRRProof (⇔)
        ↳27 QDP
        ↳28 PisEmptyProof (⇔)
        ↳29 YES
    ↳30 PiDP
        ↳31 PiDPToQDPProof (⇐)
        ↳32 QDP
        ↳33 QDPOrderProof (⇔)
        ↳34 QDP
        ↳35 DependencyGraphProof (⇔)
        ↳36 TRUE

(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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

times16(s(T40), T41, X69) :- times16(T40, T41, X68).
times16(s(T40), T41, X69) :- ','(timesc16(T40, T41, T44), plus27(T44, T41, X69)).
plus27(s(T58), T59, s(X96)) :- plus27(T58, T59, X96).
factor1(.(0, .(T19, T12)), T14) :- factor1(.(0, T12), T14).
factor1(.(s(T24), .(T25, T12)), T14) :- times16(T24, T25, X41).
factor1(.(s(T24), .(T25, T12)), T14) :- ','(timesc16(T24, T25, T28), plus27(T28, T25, X42)).
factor1(.(s(T24), .(T25, T12)), T14) :- ','(timesc16(T24, T25, T28), ','(plusc27(T28, T25, T64), factor1(.(T64, T12), T14))).

Clauses:

factorc1(.(T4, []), T4).
factorc1(.(0, .(T19, T12)), T14) :- factorc1(.(0, T12), T14).
factorc1(.(s(T24), .(T25, T12)), T14) :- ','(timesc16(T24, T25, T28), ','(plusc27(T28, T25, T64), factorc1(.(T64, T12), T14))).
timesc16(0, T35, 0).
timesc16(s(T40), T41, X69) :- ','(timesc16(T40, T41, T44), plusc27(T44, T41, X69)).
plusc27(0, T53, T53).
plusc27(s(T58), T59, s(X96)) :- plusc27(T58, T59, X96).

Afs:

factor1(x1, x2)  =  factor1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
factor1_in: (b,f)
times16_in: (b,b,f)
timesc16_in: (b,b,f)
plusc27_in: (b,b,f)
plus27_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(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, timesc16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_gga(T44, T41, X69))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → PLUS27_IN_GGA(T44, T41, X69)
PLUS27_IN_GGA(s(T58), T59, s(X96)) → U4_GGA(T58, T59, X96, plus27_in_gga(T58, T59, X96))
PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)
FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, timesc16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_gga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → PLUS27_IN_GGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plusc27_in_gga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(.(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
0  =  0
s(x1)  =  s(x1)
times16_in_gga(x1, x2, x3)  =  times16_in_gga(x1, x2)
timesc16_in_gga(x1, x2, x3)  =  timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3)  =  timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3)  =  plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3)  =  plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
plus27_in_gga(x1, x2, x3)  =  plus27_in_gga(x1, x2)
FACTOR1_IN_GA(x1, x2)  =  FACTOR1_IN_GA(x1)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x3, x5)
TIMES16_IN_GGA(x1, x2, x3)  =  TIMES16_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PLUS27_IN_GGA(x1, x2, x3)  =  PLUS27_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(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, timesc16_in_gga(T40, T41, T44))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U3_GGA(T40, T41, X69, plus27_in_gga(T44, T41, X69))
U2_GGA(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → PLUS27_IN_GGA(T44, T41, X69)
PLUS27_IN_GGA(s(T58), T59, s(X96)) → U4_GGA(T58, T59, X96, plus27_in_gga(T58, T59, X96))
PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)
FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, timesc16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U8_GA(T24, T25, T12, T14, plus27_in_gga(T28, T25, X42))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → PLUS27_IN_GGA(T28, T25, X42)
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plusc27_in_gga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → U10_GA(T24, T25, T12, T14, factor1_in_ga(.(T64, T12), T14))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The argument filtering Pi contains the following mapping:
factor1_in_ga(x1, x2)  =  factor1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
0  =  0
s(x1)  =  s(x1)
times16_in_gga(x1, x2, x3)  =  times16_in_gga(x1, x2)
timesc16_in_gga(x1, x2, x3)  =  timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3)  =  timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3)  =  plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3)  =  plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
plus27_in_gga(x1, x2, x3)  =  plus27_in_gga(x1, x2)
FACTOR1_IN_GA(x1, x2)  =  FACTOR1_IN_GA(x1)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x3, x5)
TIMES16_IN_GGA(x1, x2, x3)  =  TIMES16_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PLUS27_IN_GGA(x1, x2, x3)  =  PLUS27_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 11 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)

The TRS R consists of the following rules:

timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
timesc16_in_gga(x1, x2, x3)  =  timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3)  =  timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3)  =  plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3)  =  plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
PLUS27_IN_GGA(x1, x2, x3)  =  PLUS27_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUS27_IN_GGA(s(T58), T59, s(X96)) → PLUS27_IN_GGA(T58, T59, X96)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUS27_IN_GGA(x1, x2, x3)  =  PLUS27_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS27_IN_GGA(s(T58), T59) → PLUS27_IN_GGA(T58, T59)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUS27_IN_GGA(s(T58), T59) → PLUS27_IN_GGA(T58, T59)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMES16_IN_GGA(s(T40), T41, X69) → TIMES16_IN_GGA(T40, T41, X68)

The TRS R consists of the following rules:

timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
timesc16_in_gga(x1, x2, x3)  =  timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3)  =  timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3)  =  plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3)  =  plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
TIMES16_IN_GGA(x1, x2, x3)  =  TIMES16_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMES16_IN_GGA(s(T40), T41, X69) → TIMES16_IN_GGA(T40, T41, X68)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
TIMES16_IN_GGA(x1, x2, x3)  =  TIMES16_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES16_IN_GGA(s(T40), T41) → TIMES16_IN_GGA(T40, T41)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TIMES16_IN_GGA(s(T40), T41) → TIMES16_IN_GGA(T40, T41)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(0, .(T19, T12)), T14) → FACTOR1_IN_GA(.(0, T12), T14)

The TRS R consists of the following rules:

timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
s(x1)  =  s(x1)
timesc16_in_gga(x1, x2, x3)  =  timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3)  =  timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3)  =  plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3)  =  plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
FACTOR1_IN_GA(x1, x2)  =  FACTOR1_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(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

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(0, .(T19, T12))) → FACTOR1_IN_GA(.(0, T12))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FACTOR1_IN_GA(.(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   

(27) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(s(T24), .(T25, T12)), T14) → U7_GA(T24, T25, T12, T14, timesc16_in_gga(T24, T25, T28))
U7_GA(T24, T25, T12, T14, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, T14, plusc27_in_gga(T28, T25, T64))
U9_GA(T24, T25, T12, T14, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12), T14)

The TRS R consists of the following rules:

timesc16_in_gga(0, T35, 0) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41, X69) → U16_gga(T40, T41, X69, timesc16_in_gga(T40, T41, T44))
U16_gga(T40, T41, X69, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, X69, plusc27_in_gga(T44, T41, X69))
plusc27_in_gga(0, T53, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59, s(X96)) → U18_gga(T58, T59, X96, plusc27_in_gga(T58, T59, X96))
U18_gga(T58, T59, X96, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, X69, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
s(x1)  =  s(x1)
timesc16_in_gga(x1, x2, x3)  =  timesc16_in_gga(x1, x2)
timesc16_out_gga(x1, x2, x3)  =  timesc16_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
plusc27_in_gga(x1, x2, x3)  =  plusc27_in_gga(x1, x2)
plusc27_out_gga(x1, x2, x3)  =  plusc27_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
FACTOR1_IN_GA(x1, x2)  =  FACTOR1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FACTOR1_IN_GA(.(s(T24), .(T25, T12))) → U7_GA(T24, T25, T12, timesc16_in_gga(T24, T25))
U7_GA(T24, T25, T12, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, plusc27_in_gga(T28, T25))
U9_GA(T24, T25, T12, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12))

The TRS R consists of the following rules:

timesc16_in_gga(0, T35) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41) → U16_gga(T40, T41, timesc16_in_gga(T40, T41))
U16_gga(T40, T41, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, plusc27_in_gga(T44, T41))
plusc27_in_gga(0, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59) → U18_gga(T58, T59, plusc27_in_gga(T58, T59))
U18_gga(T58, T59, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The set Q consists of the following terms:

timesc16_in_gga(x0, x1)
U16_gga(x0, x1, x2)
plusc27_in_gga(x0, x1)
U18_gga(x0, x1, x2)
U17_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


FACTOR1_IN_GA(.(s(T24), .(T25, T12))) → U7_GA(T24, T25, T12, timesc16_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(U16_gga(x1, x2, x3)) = 0   
POL(U17_gga(x1, x2, x3)) = 0   
POL(U18_gga(x1, x2, x3)) = 1   
POL(U7_GA(x1, x2, x3, x4)) = 1 + x3   
POL(U9_GA(x1, x2, x3, x4)) = x3 + x4   
POL(plusc27_in_gga(x1, x2)) = 1   
POL(plusc27_out_gga(x1, x2, x3)) = 1   
POL(s(x1)) = 0   
POL(timesc16_in_gga(x1, x2)) = 0   
POL(timesc16_out_gga(x1, x2, x3)) = 0   

The following usable rules [FROCOS05] were oriented:

plusc27_in_gga(0, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59) → U18_gga(T58, T59, plusc27_in_gga(T58, T59))
U18_gga(T58, T59, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(T24, T25, T12, timesc16_out_gga(T24, T25, T28)) → U9_GA(T24, T25, T12, plusc27_in_gga(T28, T25))
U9_GA(T24, T25, T12, plusc27_out_gga(T28, T25, T64)) → FACTOR1_IN_GA(.(T64, T12))

The TRS R consists of the following rules:

timesc16_in_gga(0, T35) → timesc16_out_gga(0, T35, 0)
timesc16_in_gga(s(T40), T41) → U16_gga(T40, T41, timesc16_in_gga(T40, T41))
U16_gga(T40, T41, timesc16_out_gga(T40, T41, T44)) → U17_gga(T40, T41, plusc27_in_gga(T44, T41))
plusc27_in_gga(0, T53) → plusc27_out_gga(0, T53, T53)
plusc27_in_gga(s(T58), T59) → U18_gga(T58, T59, plusc27_in_gga(T58, T59))
U18_gga(T58, T59, plusc27_out_gga(T58, T59, X96)) → plusc27_out_gga(s(T58), T59, s(X96))
U17_gga(T40, T41, plusc27_out_gga(T44, T41, X69)) → timesc16_out_gga(s(T40), T41, X69)

The set Q consists of the following terms:

timesc16_in_gga(x0, x1)
U16_gga(x0, x1, x2)
plusc27_in_gga(x0, x1)
U18_gga(x0, x1, x2)
U17_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE