Left Termination proof of /tmp/tmppbHMs

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

    ↳3 PrologToPiTRSProof (⇐)

        ↳4 PiTRS

        ↳5 DependencyPairsProof (⇔)

        ↳6 PiDP

        ↳7 DependencyGraphProof (⇔)

        ↳8 AND

            ↳9 PiDP

                ↳10 UsableRulesProof (⇔)

                ↳11 PiDP

                ↳12 PiDPToQDPProof (⇐)

                ↳13 QDP

                ↳14 NonTerminationProof (⇔)

                ↳15 NO

            ↳16 PiDP

                ↳17 UsableRulesProof (⇔)

                ↳18 PiDP

                ↳19 PiDPToQDPProof (⇐)

                ↳20 QDP

                ↳21 QDPSizeChangeProof (⇔)

                ↳22 YES

            ↳23 PiDP

                ↳24 UsableRulesProof (⇔)

                ↳25 PiDP

                ↳26 PiDPToQDPProof (⇐)

                ↳27 QDP

                ↳28 MRRProof (⇔)

                ↳29 QDP

                ↳30 PisEmptyProof (⇔)

                ↳31 YES

            ↳32 PiDP

                ↳33 UsableRulesProof (⇔)

                ↳34 PiDP

                ↳35 PiDPToQDPProof (⇐)

                ↳36 QDP

                ↳37 QDPOrderProof (⇔)

                ↳38 QDP

                ↳39 DependencyGraphProof (⇔)

                ↳40 TRUE

    ↳41 PrologToPiTRSProof (⇐)

        ↳42 PiTRS

        ↳43 DependencyPairsProof (⇔)

        ↳44 PiDP

        ↳45 DependencyGraphProof (⇔)

        ↳46 AND

            ↳47 PiDP

                ↳48 UsableRulesProof (⇔)

                ↳49 PiDP

                ↳50 PiDPToQDPProof (⇐)

                ↳51 QDP

                ↳52 NonTerminationProof (⇔)

                ↳53 NO

            ↳54 PiDP

                ↳55 UsableRulesProof (⇔)

                ↳56 PiDP

                ↳57 PiDPToQDPProof (⇐)

                ↳58 QDP

                ↳59 QDPSizeChangeProof (⇔)

                ↳60 YES

            ↳61 PiDP

                ↳62 UsableRulesProof (⇔)

                ↳63 PiDP

                ↳64 PiDPToQDPProof (⇐)

                ↳65 QDP

                ↳66 MRRProof (⇔)

                ↳67 QDP

                ↳68 PisEmptyProof (⇔)

                ↳69 YES

            ↳70 PiDP

                ↳71 UsableRulesProof (⇔)

                ↳72 PiDP

                ↳73 PiDPToQDPProof (⇐)

                ↳74 QDP

                ↳75 QDPOrderProof (⇔)

                ↳76 QDP

                ↳77 DependencyGraphProof (⇔)

                ↳78 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) 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)

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)

(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)

(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)

(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)

(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)

(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(.(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(0) = 0
POL(FACTOR1_IN_GA(x₁)) = 2·x₁

(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(.(x₁, x₂)) = 1 + x₂
POL(0) = 0
POL(FACTOR1_IN_GA(x₁)) = x₁
POL(U1_gga(x₁)) = 0
POL(U2_gga(x₁, x₂)) = 0
POL(U3_gga(x₁)) = 0
POL(U4_aga(x₁)) = 0
POL(U7_GA(x₁, x₂, x₃)) = 1 + x₂
POL(U9_GA(x₁, x₂)) = 1 + x₁
POL(plus27_in_aga(x₁)) = 0
POL(plus27_out_aga(x₁, x₂)) = 0
POL(s(x₁)) = 0
POL(times16_in_gga(x₁, x₂)) = 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)

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)

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)

(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)

(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)

(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)

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)

(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)

(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)

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

Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₁ + x₂
POL(0) = 0
POL(FACTOR1_IN_GA(x₁)) = x₁

(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)

(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(.(x₁, x₂)) = 1 + x₂
POL(0) = 0
POL(FACTOR1_IN_GA(x₁)) = x₁
POL(U1_gga(x₁, x₂, x₃)) = 0
POL(U2_gga(x₁, x₂, x₃)) = 0
POL(U3_gga(x₁, x₂, x₃)) = 0
POL(U4_aga(x₁, x₂)) = 0
POL(U7_GA(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(U9_GA(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(plus27_in_aga(x₁)) = 0
POL(plus27_out_aga(x₁, x₂, x₃)) = 0
POL(s(x₁)) = 0
POL(times16_in_gga(x₁, x₂)) = 0
POL(times16_out_gga(x₁, x₂)) = 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.

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) NonTerminationProof (EQUIVALENT transformation)

(15) NO

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) MRRProof (EQUIVALENT transformation)

(29) Obligation:

(30) PisEmptyProof (EQUIVALENT transformation)

(31) YES

(32) Obligation:

(33) UsableRulesProof (EQUIVALENT transformation)

(34) Obligation:

(35) PiDPToQDPProof (SOUND transformation)

(36) Obligation:

(37) QDPOrderProof (EQUIVALENT transformation)

(38) Obligation:

(39) DependencyGraphProof (EQUIVALENT transformation)

(40) TRUE

(41) PrologToPiTRSProof (SOUND transformation)

(42) Obligation:

(43) DependencyPairsProof (EQUIVALENT transformation)

(44) Obligation:

(45) DependencyGraphProof (EQUIVALENT transformation)

(46) Complex Obligation (AND)

(47) Obligation:

(48) UsableRulesProof (EQUIVALENT transformation)

(49) Obligation:

(50) PiDPToQDPProof (SOUND transformation)

(51) Obligation:

(52) NonTerminationProof (EQUIVALENT transformation)

(53) NO

(54) Obligation:

(55) UsableRulesProof (EQUIVALENT transformation)

(56) Obligation:

(57) PiDPToQDPProof (SOUND transformation)

(58) Obligation:

(59) QDPSizeChangeProof (EQUIVALENT transformation)

(60) YES

(61) Obligation:

(62) UsableRulesProof (EQUIVALENT transformation)

(63) Obligation:

(64) PiDPToQDPProof (SOUND transformation)

(65) Obligation:

(66) MRRProof (EQUIVALENT transformation)

(67) Obligation:

(68) PisEmptyProof (EQUIVALENT transformation)

(69) YES

(70) Obligation:

(71) UsableRulesProof (EQUIVALENT transformation)

(72) Obligation:

(73) PiDPToQDPProof (SOUND transformation)

(74) Obligation:

(75) QDPOrderProof (EQUIVALENT transformation)

(76) Obligation:

(77) DependencyGraphProof (EQUIVALENT transformation)

(78) TRUE