Left Termination proof of /tmp/tmpyoalBo/der-fb.pl

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

0 Prolog

  ↳1 PrologToPiTRSProof (⇐)

    ↳2 PiTRS

    ↳3 DependencyPairsProof (⇔)

    ↳4 PiDP

    ↳5 DependencyGraphProof (⇔)

    ↳6 AND

      ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 Narrowing (⇐)

        ↳13 QDP

        ↳14 Narrowing (⇐)

        ↳15 QDP

        ↳16 NonTerminationProof (⇔)

        ↳17 FALSE

      ↳18 PiDP

        ↳19 UsableRulesProof (⇔)

        ↳20 PiDP

        ↳21 PiDPToQDPProof (⇐)

        ↳22 QDP

        ↳23 QDPOrderProof (⇔)

        ↳24 QDP

        ↳25 DependencyGraphProof (⇔)

        ↳26 QDP

        ↳27 QDPOrderProof (⇔)

        ↳28 QDP

        ↳29 DependencyGraphProof (⇔)

        ↳30 TRUE

      ↳31 PiDP

        ↳32 UsableRulesProof (⇔)

        ↳33 PiDP

        ↳34 PiDPToQDPProof (⇐)

        ↳35 QDP

        ↳36 NonTerminationProof (⇔)

        ↳37 FALSE

      ↳38 PiDP

        ↳39 UsableRulesProof (⇔)

        ↳40 PiDP

        ↳41 PiDPToQDPProof (⇐)

        ↳42 QDP

        ↳43 QDPSizeChangeProof (⇔)

        ↳44 TRUE

      ↳45 PiDP

        ↳46 UsableRulesProof (⇔)

        ↳47 PiDP

        ↳48 PiDPToQDPProof (⇐)

        ↳49 QDP

        ↳50 QDPSizeChangeProof (⇔)

        ↳51 TRUE

      ↳52 PiDP

        ↳53 UsableRulesProof (⇔)

        ↳54 PiDP

        ↳55 PiDPToQDPProof (⇐)

        ↳56 QDP

        ↳57 QDPSizeChangeProof (⇔)

        ↳58 TRUE

  ↳59 PrologToPiTRSProof (⇐)

    ↳60 PiTRS

    ↳61 DependencyPairsProof (⇔)

    ↳62 PiDP

    ↳63 DependencyGraphProof (⇔)

    ↳64 AND

      ↳65 PiDP

        ↳66 UsableRulesProof (⇔)

        ↳67 PiDP

        ↳68 PiDPToQDPProof (⇐)

        ↳69 QDP

        ↳70 Narrowing (⇐)

        ↳71 QDP

        ↳72 Narrowing (⇐)

        ↳73 QDP

        ↳74 NonTerminationProof (⇔)

        ↳75 FALSE

      ↳76 PiDP

        ↳77 UsableRulesProof (⇔)

        ↳78 PiDP

        ↳79 PiDPToQDPProof (⇐)

        ↳80 QDP

        ↳81 QDPOrderProof (⇔)

        ↳82 QDP

        ↳83 DependencyGraphProof (⇔)

        ↳84 QDP

        ↳85 QDPOrderProof (⇔)

        ↳86 QDP

        ↳87 DependencyGraphProof (⇔)

        ↳88 TRUE

      ↳89 PiDP

        ↳90 UsableRulesProof (⇔)

        ↳91 PiDP

        ↳92 PiDPToQDPProof (⇐)

        ↳93 QDP

        ↳94 NonTerminationProof (⇔)

        ↳95 FALSE

      ↳96 PiDP

        ↳97 UsableRulesProof (⇔)

        ↳98 PiDP

        ↳99 PiDPToQDPProof (⇐)

        ↳100 QDP

        ↳101 QDPSizeChangeProof (⇔)

        ↳102 TRUE

      ↳103 PiDP

        ↳104 UsableRulesProof (⇔)

        ↳105 PiDP

        ↳106 PiDPToQDPProof (⇐)

        ↳107 QDP

        ↳108 QDPSizeChangeProof (⇔)

        ↳109 TRUE

      ↳110 PiDP

        ↳111 UsableRulesProof (⇔)

        ↳112 PiDP

        ↳113 PiDPToQDPProof (⇐)

        ↳114 QDP

        ↳115 QDPSizeChangeProof (⇔)

        ↳116 TRUE

(0) Obligation:

Clauses:

p(d(e(t)), const(1)).
p(d(e(const(A))), const(0)).
p(d(e(+(X, Y))), +(DX, DY)) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY)).
p(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY)).
p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX)).

Queries:

p(a,g).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
p_in: (f,b) (b,b) (b,f) (f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

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

P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(d(X)), DDX) → U5_GG(X, DDX, p_in_ga(d(X), DX))
P_IN_GG(d(d(X)), DDX) → P_IN_GA(d(X), DX)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(d(X)), DDX) → U5_GA(X, DDX, p_in_ga(d(X), DX))
P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)
U5_GA(X, DDX, p_out_ga(d(X), DX)) → U6_GA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_GA(X, DDX, p_out_ga(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_GA(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_GA(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U5_GG(X, DDX, p_out_ga(d(X), DX)) → U6_GG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_GG(X, DDX, p_out_ga(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_GG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_GG(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_AG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_AG(d(d(X)), DDX) → U5_AG(X, DDX, p_in_aa(d(X), DX))
P_IN_AG(d(d(X)), DDX) → P_IN_AA(d(X), DX)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(d(X)), DDX) → U5_AA(X, DDX, p_in_aa(d(X), DX))
P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)
U5_AA(X, DDX, p_out_aa(d(X), DX)) → U6_AA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_AA(X, DDX, p_out_aa(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_AA(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_AA(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U5_AG(X, DDX, p_out_aa(d(X), DX)) → U6_AG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_AG(X, DDX, p_out_aa(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_AG(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

The argument filtering Pi contains the following mapping:
p_in_ag(x1, x2) = p_in_ag(x2)
const(x1) = const
1 = 1
p_out_ag(x1, x2) = p_out_ag(x1)
0 = 0
+(x1, x2) = +(x1, x2)
U1_ag(x1, x2, x3, x4, x5) = U1_ag(x4, x5)
*(x1, x2) = *(x1, x2)
U3_ag(x1, x2, x3, x4, x5) = U3_ag(x1, x2, x3, x5)
p_in_gg(x1, x2) = p_in_gg(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_out_gg(x1, x2) = p_out_gg
U1_gg(x1, x2, x3, x4, x5) = U1_gg(x2, x4, x5)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x2, x3, x5)
U5_gg(x1, x2, x3) = U5_gg(x2, x3)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x2, x5)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x5)
U5_ga(x1, x2, x3) = U5_ga(x3)
U6_ga(x1, x2, x3, x4) = U6_ga(x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x4, x5)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
U4_gg(x1, x2, x3, x4, x5) = U4_gg(x5)
U2_gg(x1, x2, x3, x4, x5) = U2_gg(x5)
U4_ag(x1, x2, x3, x4, x5) = U4_ag(x1, x2, x5)
U5_ag(x1, x2, x3) = U5_ag(x2, x3)
p_in_aa(x1, x2) = p_in_aa
p_out_aa(x1, x2) = p_out_aa(x1, x2)
U1_aa(x1, x2, x3, x4, x5) = U1_aa(x5)
U3_aa(x1, x2, x3, x4, x5) = U3_aa(x5)
U5_aa(x1, x2, x3) = U5_aa(x3)
U6_aa(x1, x2, x3, x4) = U6_aa(x1, x4)
U4_aa(x1, x2, x3, x4, x5) = U4_aa(x1, x4, x5)
U2_aa(x1, x2, x3, x4, x5) = U2_aa(x1, x3, x5)
U6_ag(x1, x2, x3, x4) = U6_ag(x1, x4)
U2_ag(x1, x2, x3, x4, x5) = U2_ag(x1, x5)
P_IN_AG(x1, x2) = P_IN_AG(x2)
U1_AG(x1, x2, x3, x4, x5) = U1_AG(x4, x5)
U3_AG(x1, x2, x3, x4, x5) = U3_AG(x1, x2, x3, x5)
P_IN_GG(x1, x2) = P_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4, x5) = U1_GG(x2, x4, x5)
U3_GG(x1, x2, x3, x4, x5) = U3_GG(x2, x3, x5)
U5_GG(x1, x2, x3) = U5_GG(x2, x3)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x2, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)
U5_GA(x1, x2, x3) = U5_GA(x3)
U6_GA(x1, x2, x3, x4) = U6_GA(x4)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x4, x5)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x3, x5)
U6_GG(x1, x2, x3, x4) = U6_GG(x4)
U4_GG(x1, x2, x3, x4, x5) = U4_GG(x5)
U2_GG(x1, x2, x3, x4, x5) = U2_GG(x5)
U4_AG(x1, x2, x3, x4, x5) = U4_AG(x1, x2, x5)
U5_AG(x1, x2, x3) = U5_AG(x2, x3)
P_IN_AA(x1, x2) = P_IN_AA
U1_AA(x1, x2, x3, x4, x5) = U1_AA(x5)
U3_AA(x1, x2, x3, x4, x5) = U3_AA(x5)
U5_AA(x1, x2, x3) = U5_AA(x3)
U6_AA(x1, x2, x3, x4) = U6_AA(x1, x4)
U4_AA(x1, x2, x3, x4, x5) = U4_AA(x1, x4, x5)
U2_AA(x1, x2, x3, x4, x5) = U2_AA(x1, x3, x5)
U6_AG(x1, x2, x3, x4) = U6_AG(x1, x4)
U2_AG(x1, x2, x3, x4, x5) = U2_AG(x1, x5)

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

(4) Obligation:

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

P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(d(X)), DDX) → U5_GG(X, DDX, p_in_ga(d(X), DX))
P_IN_GG(d(d(X)), DDX) → P_IN_GA(d(X), DX)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(d(X)), DDX) → U5_GA(X, DDX, p_in_ga(d(X), DX))
P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)
U5_GA(X, DDX, p_out_ga(d(X), DX)) → U6_GA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_GA(X, DDX, p_out_ga(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_GA(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_GA(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U5_GG(X, DDX, p_out_ga(d(X), DX)) → U6_GG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_GG(X, DDX, p_out_ga(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_GG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_GG(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_AG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_AG(d(d(X)), DDX) → U5_AG(X, DDX, p_in_aa(d(X), DX))
P_IN_AG(d(d(X)), DDX) → P_IN_AA(d(X), DX)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(d(X)), DDX) → U5_AA(X, DDX, p_in_aa(d(X), DX))
P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)
U5_AA(X, DDX, p_out_aa(d(X), DX)) → U6_AA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_AA(X, DDX, p_out_aa(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_AA(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_AA(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U5_AG(X, DDX, p_out_aa(d(X), DX)) → U6_AG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_AG(X, DDX, p_out_aa(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_AG(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 25 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

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

U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The argument filtering Pi contains the following mapping:
const(x1) = const
1 = 1
0 = 0
+(x1, x2) = +(x1, x2)
*(x1, x2) = *(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_in_aa(x1, x2) = p_in_aa
p_out_aa(x1, x2) = p_out_aa(x1, x2)
U1_aa(x1, x2, x3, x4, x5) = U1_aa(x5)
U3_aa(x1, x2, x3, x4, x5) = U3_aa(x5)
U4_aa(x1, x2, x3, x4, x5) = U4_aa(x1, x4, x5)
U2_aa(x1, x2, x3, x4, x5) = U2_aa(x1, x3, x5)
P_IN_AA(x1, x2) = P_IN_AA
U1_AA(x1, x2, x3, x4, x5) = U1_AA(x5)
U3_AA(x1, x2, x3, x4, x5) = U3_AA(x5)

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:

U1_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → U1_AA(p_in_aa)
P_IN_AA → P_IN_AA
P_IN_AA → U3_AA(p_in_aa)
U3_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA

The TRS R consists of the following rules:

p_in_aa → p_out_aa(d(e(t)), const)
p_in_aa → p_out_aa(d(e(const)), const)
p_in_aa → U1_aa(p_in_aa)
p_in_aa → U3_aa(p_in_aa)
U1_aa(p_out_aa(d(e(X)), DX)) → U2_aa(X, DX, p_in_aa)
U3_aa(p_out_aa(d(e(X)), DX)) → U4_aa(X, DX, p_in_aa)
U2_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_aa
U1_aa(x0)
U3_aa(x0)
U2_aa(x0, x1, x2)
U4_aa(x0, x1, x2)

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

(12) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P_IN_AA → U1_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

P_IN_AA → U1_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U1_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U1_AA(U1_aa(p_in_aa))
P_IN_AA → U1_AA(U3_aa(p_in_aa))

(13) Obligation:

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

U1_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → P_IN_AA
P_IN_AA → U3_AA(p_in_aa)
U3_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → U1_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U1_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U1_AA(U1_aa(p_in_aa))
P_IN_AA → U1_AA(U3_aa(p_in_aa))

The TRS R consists of the following rules:

p_in_aa → p_out_aa(d(e(t)), const)
p_in_aa → p_out_aa(d(e(const)), const)
p_in_aa → U1_aa(p_in_aa)
p_in_aa → U3_aa(p_in_aa)
U1_aa(p_out_aa(d(e(X)), DX)) → U2_aa(X, DX, p_in_aa)
U3_aa(p_out_aa(d(e(X)), DX)) → U4_aa(X, DX, p_in_aa)
U2_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_aa
U1_aa(x0)
U3_aa(x0)
U2_aa(x0, x1, x2)
U4_aa(x0, x1, x2)

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

(14) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P_IN_AA → U3_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

P_IN_AA → U3_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U3_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U3_AA(U1_aa(p_in_aa))
P_IN_AA → U3_AA(U3_aa(p_in_aa))

(15) Obligation:

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

U1_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → P_IN_AA
U3_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → U1_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U1_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U1_AA(U1_aa(p_in_aa))
P_IN_AA → U1_AA(U3_aa(p_in_aa))
P_IN_AA → U3_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U3_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U3_AA(U1_aa(p_in_aa))
P_IN_AA → U3_AA(U3_aa(p_in_aa))

The TRS R consists of the following rules:

p_in_aa → p_out_aa(d(e(t)), const)
p_in_aa → p_out_aa(d(e(const)), const)
p_in_aa → U1_aa(p_in_aa)
p_in_aa → U3_aa(p_in_aa)
U1_aa(p_out_aa(d(e(X)), DX)) → U2_aa(X, DX, p_in_aa)
U3_aa(p_out_aa(d(e(X)), DX)) → U4_aa(X, DX, p_in_aa)
U2_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_aa
U1_aa(x0)
U3_aa(x0)
U2_aa(x0, x1, x2)
U4_aa(x0, x1, x2)

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

(16) 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 = P_IN_AA evaluates to t =P_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from P_IN_AA to P_IN_AA.

(17) FALSE

(18) Obligation:

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

U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(19) UsableRulesProof (EQUIVALENT transformation)

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

(20) Obligation:

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

U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The argument filtering Pi contains the following mapping:
const(x1) = const
1 = 1
0 = 0
+(x1, x2) = +(x1, x2)
*(x1, x2) = *(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x2, x5)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x5)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x4, x5)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x3, x5)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x2, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)

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

(21) PiDPToQDPProof (SOUND transformation)

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

(22) Obligation:

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

U1_GA(Y, p_out_ga(DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(+(X, Y)))) → U1_GA(Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(+(X, Y)))) → P_IN_GA(d(e(X)))
P_IN_GA(d(e(*(X, Y)))) → U3_GA(X, Y, p_in_ga(d(e(X))))
U3_GA(X, Y, p_out_ga(DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(*(X, Y)))) → P_IN_GA(d(e(X)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(const)
p_in_ga(d(e(const))) → p_out_ga(const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(Y, p_out_ga(DX)) → U2_ga(DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(DX, p_out_ga(DY)) → p_out_ga(+(DX, DY))
U4_ga(X, Y, DX, p_out_ga(DY)) → p_out_ga(+(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1)
U3_ga(x0, x1, x2)
U2_ga(x0, x1)
U4_ga(x0, x1, x2, x3)

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

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P_IN_GA(d(e(*(X, Y)))) → U3_GA(X, Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(*(X, Y)))) → P_IN_GA(d(e(X)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x₁, x₂)) = 1 + x₁ + x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(P_IN_GA(x₁)) = x₁
POL(U1_GA(x₁, x₂)) = x₁
POL(U1_ga(x₁, x₂)) = 0
POL(U2_ga(x₁, x₂)) = 0
POL(U3_GA(x₁, x₂, x₃)) = x₂
POL(U3_ga(x₁, x₂, x₃)) = 0
POL(U4_ga(x₁, x₂, x₃, x₄)) = 0
POL(const) = 0
POL(d(x₁)) = x₁
POL(e(x₁)) = x₁
POL(p_in_ga(x₁)) = 0
POL(p_out_ga(x₁)) = 0
POL(t) = 0

The following usable rules [FROCOS05] were oriented: none

(24) Obligation:

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

U1_GA(Y, p_out_ga(DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(+(X, Y)))) → U1_GA(Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(+(X, Y)))) → P_IN_GA(d(e(X)))
U3_GA(X, Y, p_out_ga(DX)) → P_IN_GA(d(e(Y)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(const)
p_in_ga(d(e(const))) → p_out_ga(const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(Y, p_out_ga(DX)) → U2_ga(DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(DX, p_out_ga(DY)) → p_out_ga(+(DX, DY))
U4_ga(X, Y, DX, p_out_ga(DY)) → p_out_ga(+(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1)
U3_ga(x0, x1, x2)
U2_ga(x0, x1)
U4_ga(x0, x1, x2, x3)

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

(25) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(26) Obligation:

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

P_IN_GA(d(e(+(X, Y)))) → U1_GA(Y, p_in_ga(d(e(X))))
U1_GA(Y, p_out_ga(DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(+(X, Y)))) → P_IN_GA(d(e(X)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(const)
p_in_ga(d(e(const))) → p_out_ga(const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(Y, p_out_ga(DX)) → U2_ga(DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(DX, p_out_ga(DY)) → p_out_ga(+(DX, DY))
U4_ga(X, Y, DX, p_out_ga(DY)) → p_out_ga(+(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1)
U3_ga(x0, x1, x2)
U2_ga(x0, x1)
U4_ga(x0, x1, x2, x3)

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

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P_IN_GA(d(e(+(X, Y)))) → U1_GA(Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(+(X, Y)))) → P_IN_GA(d(e(X)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x₁, x₂)) = 0
POL(+(x₁, x₂)) = 1 + x₁ + x₂
POL(P_IN_GA(x₁)) = x₁
POL(U1_GA(x₁, x₂)) = x₁
POL(U1_ga(x₁, x₂)) = 0
POL(U2_ga(x₁, x₂)) = 0
POL(U3_ga(x₁, x₂, x₃)) = 0
POL(U4_ga(x₁, x₂, x₃, x₄)) = 0
POL(const) = 0
POL(d(x₁)) = x₁
POL(e(x₁)) = x₁
POL(p_in_ga(x₁)) = 0
POL(p_out_ga(x₁)) = 0
POL(t) = 0

The following usable rules [FROCOS05] were oriented: none

(28) Obligation:

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

U1_GA(Y, p_out_ga(DX)) → P_IN_GA(d(e(Y)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(const)
p_in_ga(d(e(const))) → p_out_ga(const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(Y, p_out_ga(DX)) → U2_ga(DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(DX, p_out_ga(DY)) → p_out_ga(+(DX, DY))
U4_ga(X, Y, DX, p_out_ga(DY)) → p_out_ga(+(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1)
U3_ga(x0, x1, x2)
U2_ga(x0, x1)
U4_ga(x0, x1, x2, x3)

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

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

(31) Obligation:

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

P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(32) UsableRulesProof (EQUIVALENT transformation)

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

(33) Obligation:

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

P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)

R is empty.
The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
P_IN_AA(x1, x2) = P_IN_AA

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

(34) PiDPToQDPProof (SOUND transformation)

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

(35) Obligation:

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

P_IN_AA → P_IN_AA

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

(36) NonTerminationProof (EQUIVALENT transformation)

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from P_IN_AA to P_IN_AA.

(37) FALSE

(38) Obligation:

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

P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(39) UsableRulesProof (EQUIVALENT transformation)

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

(40) Obligation:

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

P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)

R is empty.
The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
P_IN_GA(x1, x2) = P_IN_GA(x1)

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

(41) PiDPToQDPProof (SOUND transformation)

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

(42) Obligation:

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

P_IN_GA(d(d(X))) → P_IN_GA(d(X))

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

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

P_IN_GA(d(d(X))) → P_IN_GA(d(X))
The graph contains the following edges 1 > 1

(44) TRUE

(45) Obligation:

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

U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(46) UsableRulesProof (EQUIVALENT transformation)

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

(47) Obligation:

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

U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The argument filtering Pi contains the following mapping:
const(x1) = const
1 = 1
0 = 0
+(x1, x2) = +(x1, x2)
*(x1, x2) = *(x1, x2)
p_in_gg(x1, x2) = p_in_gg(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_out_gg(x1, x2) = p_out_gg
U1_gg(x1, x2, x3, x4, x5) = U1_gg(x2, x4, x5)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x2, x3, x5)
U4_gg(x1, x2, x3, x4, x5) = U4_gg(x5)
U2_gg(x1, x2, x3, x4, x5) = U2_gg(x5)
P_IN_GG(x1, x2) = P_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4, x5) = U1_GG(x2, x4, x5)
U3_GG(x1, x2, x3, x4, x5) = U3_GG(x2, x3, x5)

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

(48) PiDPToQDPProof (SOUND transformation)

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

(49) Obligation:

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

U1_GG(Y, DY, p_out_gg) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(Y, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(Y, DY, p_in_gg(d(e(X)), DX))
U3_GG(Y, DY, p_out_gg) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_gg(d(e(t)), const) → p_out_gg
p_in_gg(d(e(const)), const) → p_out_gg
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(Y, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(Y, DY, p_in_gg(d(e(X)), DX))
U1_gg(Y, DY, p_out_gg) → U2_gg(p_in_gg(d(e(Y)), DY))
U3_gg(Y, DY, p_out_gg) → U4_gg(p_in_gg(d(e(Y)), DY))
U2_gg(p_out_gg) → p_out_gg
U4_gg(p_out_gg) → p_out_gg

The set Q consists of the following terms:

p_in_gg(x0, x1)
U1_gg(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gg(x0)
U4_gg(x0)

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

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

P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(Y, DY, p_in_gg(d(e(X)), DX))
The graph contains the following edges 1 > 1, 2 > 2
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(Y, DY, p_in_gg(d(e(X)), DX))
The graph contains the following edges 1 > 1, 2 > 1, 2 > 2
U1_GG(Y, DY, p_out_gg) → P_IN_GG(d(e(Y)), DY)
The graph contains the following edges 2 >= 2
U3_GG(Y, DY, p_out_gg) → P_IN_GG(d(e(Y)), DY)
The graph contains the following edges 2 >= 2
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
The graph contains the following edges 2 > 2
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
The graph contains the following edges 2 > 2

(51) TRUE

(52) Obligation:

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

U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(53) UsableRulesProof (EQUIVALENT transformation)

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

(54) Obligation:

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

U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

(55) PiDPToQDPProof (SOUND transformation)

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

(56) Obligation:

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

U1_AG(DY, p_out_ag(d(e(X)))) → P_IN_AG(DY)
P_IN_AG(+(DX, DY)) → U1_AG(DY, p_in_ag(DX))
P_IN_AG(+(DX, DY)) → P_IN_AG(DX)

The TRS R consists of the following rules:

p_in_ag(const) → p_out_ag(d(e(t)))
p_in_ag(const) → p_out_ag(d(e(const)))
p_in_ag(+(DX, DY)) → U1_ag(DY, p_in_ag(DX))
p_in_ag(+(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, p_in_gg(d(e(X)), DX))
U1_ag(DY, p_out_ag(d(e(X)))) → U2_ag(X, p_in_ag(DY))
U3_ag(X, Y, DY, p_out_gg) → U4_ag(X, Y, p_in_gg(d(e(Y)), DY))
U2_ag(X, p_out_ag(d(e(Y)))) → p_out_ag(d(e(+(X, Y))))
p_in_gg(d(e(t)), const) → p_out_gg
p_in_gg(d(e(const)), const) → p_out_gg
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(Y, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(Y, DY, p_in_gg(d(e(X)), DX))
U4_ag(X, Y, p_out_gg) → p_out_ag(d(e(*(X, Y))))
U1_gg(Y, DY, p_out_gg) → U2_gg(p_in_gg(d(e(Y)), DY))
U3_gg(Y, DY, p_out_gg) → U4_gg(p_in_gg(d(e(Y)), DY))
U2_gg(p_out_gg) → p_out_gg
U4_gg(p_out_gg) → p_out_gg

The set Q consists of the following terms:

p_in_ag(x0)
U1_ag(x0, x1)
U3_ag(x0, x1, x2, x3)
U2_ag(x0, x1)
p_in_gg(x0, x1)
U4_ag(x0, x1, x2)
U1_gg(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gg(x0)
U4_gg(x0)

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

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

P_IN_AG(+(DX, DY)) → U1_AG(DY, p_in_ag(DX))
The graph contains the following edges 1 > 1
P_IN_AG(+(DX, DY)) → P_IN_AG(DX)
The graph contains the following edges 1 > 1
U1_AG(DY, p_out_ag(d(e(X)))) → P_IN_AG(DY)
The graph contains the following edges 1 >= 1

(58) TRUE

(59) PrologToPiTRSProof (SOUND transformation)

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(60) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

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

P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(d(X)), DDX) → U5_GG(X, DDX, p_in_ga(d(X), DX))
P_IN_GG(d(d(X)), DDX) → P_IN_GA(d(X), DX)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(d(X)), DDX) → U5_GA(X, DDX, p_in_ga(d(X), DX))
P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)
U5_GA(X, DDX, p_out_ga(d(X), DX)) → U6_GA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_GA(X, DDX, p_out_ga(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_GA(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_GA(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U5_GG(X, DDX, p_out_ga(d(X), DX)) → U6_GG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_GG(X, DDX, p_out_ga(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_GG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_GG(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_AG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_AG(d(d(X)), DDX) → U5_AG(X, DDX, p_in_aa(d(X), DX))
P_IN_AG(d(d(X)), DDX) → P_IN_AA(d(X), DX)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(d(X)), DDX) → U5_AA(X, DDX, p_in_aa(d(X), DX))
P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)
U5_AA(X, DDX, p_out_aa(d(X), DX)) → U6_AA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_AA(X, DDX, p_out_aa(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_AA(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_AA(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U5_AG(X, DDX, p_out_aa(d(X), DX)) → U6_AG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_AG(X, DDX, p_out_aa(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_AG(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

The argument filtering Pi contains the following mapping:
p_in_ag(x1, x2) = p_in_ag(x2)
const(x1) = const
1 = 1
p_out_ag(x1, x2) = p_out_ag(x1, x2)
0 = 0
+(x1, x2) = +(x1, x2)
U1_ag(x1, x2, x3, x4, x5) = U1_ag(x3, x4, x5)
*(x1, x2) = *(x1, x2)
U3_ag(x1, x2, x3, x4, x5) = U3_ag(x1, x2, x3, x4, x5)
p_in_gg(x1, x2) = p_in_gg(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_out_gg(x1, x2) = p_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4, x5) = U1_gg(x1, x2, x3, x4, x5)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x1, x2, x3, x4, x5)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x5)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x5)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x4, x5)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x2, x4)
U4_gg(x1, x2, x3, x4, x5) = U4_gg(x1, x2, x3, x4, x5)
U2_gg(x1, x2, x3, x4, x5) = U2_gg(x1, x2, x3, x4, x5)
U4_ag(x1, x2, x3, x4, x5) = U4_ag(x1, x2, x3, x4, x5)
U5_ag(x1, x2, x3) = U5_ag(x2, x3)
p_in_aa(x1, x2) = p_in_aa
p_out_aa(x1, x2) = p_out_aa(x1, x2)
U1_aa(x1, x2, x3, x4, x5) = U1_aa(x5)
U3_aa(x1, x2, x3, x4, x5) = U3_aa(x5)
U5_aa(x1, x2, x3) = U5_aa(x3)
U6_aa(x1, x2, x3, x4) = U6_aa(x1, x4)
U4_aa(x1, x2, x3, x4, x5) = U4_aa(x1, x4, x5)
U2_aa(x1, x2, x3, x4, x5) = U2_aa(x1, x3, x5)
U6_ag(x1, x2, x3, x4) = U6_ag(x1, x2, x4)
U2_ag(x1, x2, x3, x4, x5) = U2_ag(x1, x3, x4, x5)
P_IN_AG(x1, x2) = P_IN_AG(x2)
U1_AG(x1, x2, x3, x4, x5) = U1_AG(x3, x4, x5)
U3_AG(x1, x2, x3, x4, x5) = U3_AG(x1, x2, x3, x4, x5)
P_IN_GG(x1, x2) = P_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4, x5) = U1_GG(x1, x2, x3, x4, x5)
U3_GG(x1, x2, x3, x4, x5) = U3_GG(x1, x2, x3, x4, x5)
U5_GG(x1, x2, x3) = U5_GG(x1, x2, x3)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
U6_GA(x1, x2, x3, x4) = U6_GA(x1, x4)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x4, x5)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)
U6_GG(x1, x2, x3, x4) = U6_GG(x1, x2, x4)
U4_GG(x1, x2, x3, x4, x5) = U4_GG(x1, x2, x3, x4, x5)
U2_GG(x1, x2, x3, x4, x5) = U2_GG(x1, x2, x3, x4, x5)
U4_AG(x1, x2, x3, x4, x5) = U4_AG(x1, x2, x3, x4, x5)
U5_AG(x1, x2, x3) = U5_AG(x2, x3)
P_IN_AA(x1, x2) = P_IN_AA
U1_AA(x1, x2, x3, x4, x5) = U1_AA(x5)
U3_AA(x1, x2, x3, x4, x5) = U3_AA(x5)
U5_AA(x1, x2, x3) = U5_AA(x3)
U6_AA(x1, x2, x3, x4) = U6_AA(x1, x4)
U4_AA(x1, x2, x3, x4, x5) = U4_AA(x1, x4, x5)
U2_AA(x1, x2, x3, x4, x5) = U2_AA(x1, x3, x5)
U6_AG(x1, x2, x3, x4) = U6_AG(x1, x2, x4)
U2_AG(x1, x2, x3, x4, x5) = U2_AG(x1, x3, x4, x5)

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

(62) Obligation:

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

P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_AG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(d(X)), DDX) → U5_GG(X, DDX, p_in_ga(d(X), DX))
P_IN_GG(d(d(X)), DDX) → P_IN_GA(d(X), DX)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(d(X)), DDX) → U5_GA(X, DDX, p_in_ga(d(X), DX))
P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)
U5_GA(X, DDX, p_out_ga(d(X), DX)) → U6_GA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_GA(X, DDX, p_out_ga(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_GA(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_GA(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
U5_GG(X, DDX, p_out_ga(d(X), DX)) → U6_GG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_GG(X, DDX, p_out_ga(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_GG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_GG(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_AG(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U3_AG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_AG(d(d(X)), DDX) → U5_AG(X, DDX, p_in_aa(d(X), DX))
P_IN_AG(d(d(X)), DDX) → P_IN_AA(d(X), DX)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(d(X)), DDX) → U5_AA(X, DDX, p_in_aa(d(X), DX))
P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)
U5_AA(X, DDX, p_out_aa(d(X), DX)) → U6_AA(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U5_AA(X, DDX, p_out_aa(d(X), DX)) → P_IN_GA(d(e(DX)), DDX)
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_AA(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_AA(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
U5_AG(X, DDX, p_out_aa(d(X), DX)) → U6_AG(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U5_AG(X, DDX, p_out_aa(d(X), DX)) → P_IN_GG(d(e(DX)), DDX)
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_AG(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(63) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 25 less nodes.

(64) Complex Obligation (AND)

(65) Obligation:

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

U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(66) UsableRulesProof (EQUIVALENT transformation)

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

(67) Obligation:

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

U1_AA(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → U1_AA(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
P_IN_AA(d(e(+(X, Y))), +(DX, DY)) → P_IN_AA(d(e(X)), DX)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_AA(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
U3_AA(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → P_IN_AA(d(e(Y)), DY)
P_IN_AA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_AA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

(68) PiDPToQDPProof (SOUND transformation)

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

(69) Obligation:

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

U1_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → U1_AA(p_in_aa)
P_IN_AA → P_IN_AA
P_IN_AA → U3_AA(p_in_aa)
U3_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA

The TRS R consists of the following rules:

p_in_aa → p_out_aa(d(e(t)), const)
p_in_aa → p_out_aa(d(e(const)), const)
p_in_aa → U1_aa(p_in_aa)
p_in_aa → U3_aa(p_in_aa)
U1_aa(p_out_aa(d(e(X)), DX)) → U2_aa(X, DX, p_in_aa)
U3_aa(p_out_aa(d(e(X)), DX)) → U4_aa(X, DX, p_in_aa)
U2_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_aa
U1_aa(x0)
U3_aa(x0)
U2_aa(x0, x1, x2)
U4_aa(x0, x1, x2)

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

(70) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P_IN_AA → U1_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

P_IN_AA → U1_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U1_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U1_AA(U1_aa(p_in_aa))
P_IN_AA → U1_AA(U3_aa(p_in_aa))

(71) Obligation:

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

U1_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → P_IN_AA
P_IN_AA → U3_AA(p_in_aa)
U3_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → U1_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U1_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U1_AA(U1_aa(p_in_aa))
P_IN_AA → U1_AA(U3_aa(p_in_aa))

The TRS R consists of the following rules:

p_in_aa → p_out_aa(d(e(t)), const)
p_in_aa → p_out_aa(d(e(const)), const)
p_in_aa → U1_aa(p_in_aa)
p_in_aa → U3_aa(p_in_aa)
U1_aa(p_out_aa(d(e(X)), DX)) → U2_aa(X, DX, p_in_aa)
U3_aa(p_out_aa(d(e(X)), DX)) → U4_aa(X, DX, p_in_aa)
U2_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_aa
U1_aa(x0)
U3_aa(x0)
U2_aa(x0, x1, x2)
U4_aa(x0, x1, x2)

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

(72) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P_IN_AA → U3_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

P_IN_AA → U3_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U3_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U3_AA(U1_aa(p_in_aa))
P_IN_AA → U3_AA(U3_aa(p_in_aa))

(73) Obligation:

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

U1_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → P_IN_AA
U3_AA(p_out_aa(d(e(X)), DX)) → P_IN_AA
P_IN_AA → U1_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U1_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U1_AA(U1_aa(p_in_aa))
P_IN_AA → U1_AA(U3_aa(p_in_aa))
P_IN_AA → U3_AA(p_out_aa(d(e(t)), const))
P_IN_AA → U3_AA(p_out_aa(d(e(const)), const))
P_IN_AA → U3_AA(U1_aa(p_in_aa))
P_IN_AA → U3_AA(U3_aa(p_in_aa))

The TRS R consists of the following rules:

p_in_aa → p_out_aa(d(e(t)), const)
p_in_aa → p_out_aa(d(e(const)), const)
p_in_aa → U1_aa(p_in_aa)
p_in_aa → U3_aa(p_in_aa)
U1_aa(p_out_aa(d(e(X)), DX)) → U2_aa(X, DX, p_in_aa)
U3_aa(p_out_aa(d(e(X)), DX)) → U4_aa(X, DX, p_in_aa)
U2_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U4_aa(X, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_aa
U1_aa(x0)
U3_aa(x0)
U2_aa(x0, x1, x2)
U4_aa(x0, x1, x2)

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

(74) NonTerminationProof (EQUIVALENT transformation)

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from P_IN_AA to P_IN_AA.

(75) FALSE

(76) Obligation:

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

U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(77) UsableRulesProof (EQUIVALENT transformation)

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

(78) Obligation:

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

U1_GA(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → U1_GA(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
P_IN_GA(d(e(+(X, Y))), +(DX, DY)) → P_IN_GA(d(e(X)), DX)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GA(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
U3_GA(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)), DY)
P_IN_GA(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GA(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The argument filtering Pi contains the following mapping:
const(x1) = const
1 = 1
0 = 0
+(x1, x2) = +(x1, x2)
*(x1, x2) = *(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x5)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x5)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x4, x5)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x3, x5)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)

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

(79) PiDPToQDPProof (SOUND transformation)

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

(80) Obligation:

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

U1_GA(X, Y, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(+(X, Y)))) → U1_GA(X, Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(+(X, Y)))) → P_IN_GA(d(e(X)))
P_IN_GA(d(e(*(X, Y)))) → U3_GA(X, Y, p_in_ga(d(e(X))))
U3_GA(X, Y, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(*(X, Y)))) → P_IN_GA(d(e(X)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(d(e(t)), const)
p_in_ga(d(e(const))) → p_out_ga(d(e(const)), const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(X, Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(X, Y, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U4_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1, x2)
U3_ga(x0, x1, x2)
U2_ga(x0, x1, x2, x3)
U4_ga(x0, x1, x2, x3)

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

(81) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P_IN_GA(d(e(+(X, Y)))) → U1_GA(X, Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(+(X, Y)))) → P_IN_GA(d(e(X)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x₁, x₂)) = x₁ + x₂
POL(+(x₁, x₂)) = 1 + x₁ + x₂
POL(P_IN_GA(x₁)) = x₁
POL(U1_GA(x₁, x₂, x₃)) = x₁ + x₂
POL(U1_ga(x₁, x₂, x₃)) = 0
POL(U2_ga(x₁, x₂, x₃, x₄)) = 0
POL(U3_GA(x₁, x₂, x₃)) = x₂
POL(U3_ga(x₁, x₂, x₃)) = 0
POL(U4_ga(x₁, x₂, x₃, x₄)) = 0
POL(const) = 0
POL(d(x₁)) = x₁
POL(e(x₁)) = x₁
POL(p_in_ga(x₁)) = 0
POL(p_out_ga(x₁, x₂)) = 0
POL(t) = 0

The following usable rules [FROCOS05] were oriented: none

(82) Obligation:

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

U1_GA(X, Y, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(*(X, Y)))) → U3_GA(X, Y, p_in_ga(d(e(X))))
U3_GA(X, Y, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(*(X, Y)))) → P_IN_GA(d(e(X)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(d(e(t)), const)
p_in_ga(d(e(const))) → p_out_ga(d(e(const)), const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(X, Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(X, Y, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U4_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1, x2)
U3_ga(x0, x1, x2)
U2_ga(x0, x1, x2, x3)
U4_ga(x0, x1, x2, x3)

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

(83) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(84) Obligation:

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

U3_GA(X, Y, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)))
P_IN_GA(d(e(*(X, Y)))) → U3_GA(X, Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(*(X, Y)))) → P_IN_GA(d(e(X)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(d(e(t)), const)
p_in_ga(d(e(const))) → p_out_ga(d(e(const)), const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(X, Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(X, Y, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U4_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1, x2)
U3_ga(x0, x1, x2)
U2_ga(x0, x1, x2, x3)
U4_ga(x0, x1, x2, x3)

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

(85) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P_IN_GA(d(e(*(X, Y)))) → U3_GA(X, Y, p_in_ga(d(e(X))))
P_IN_GA(d(e(*(X, Y)))) → P_IN_GA(d(e(X)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x₁, x₂)) = 1 + x₁ + x₂
POL(+(x₁, x₂)) = 0
POL(P_IN_GA(x₁)) = x₁
POL(U1_ga(x₁, x₂, x₃)) = 0
POL(U2_ga(x₁, x₂, x₃, x₄)) = 0
POL(U3_GA(x₁, x₂, x₃)) = x₂
POL(U3_ga(x₁, x₂, x₃)) = 0
POL(U4_ga(x₁, x₂, x₃, x₄)) = 0
POL(const) = 0
POL(d(x₁)) = x₁
POL(e(x₁)) = x₁
POL(p_in_ga(x₁)) = 0
POL(p_out_ga(x₁, x₂)) = 0
POL(t) = 0

The following usable rules [FROCOS05] were oriented: none

(86) Obligation:

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

U3_GA(X, Y, p_out_ga(d(e(X)), DX)) → P_IN_GA(d(e(Y)))

The TRS R consists of the following rules:

p_in_ga(d(e(t))) → p_out_ga(d(e(t)), const)
p_in_ga(d(e(const))) → p_out_ga(d(e(const)), const)
p_in_ga(d(e(+(X, Y)))) → U1_ga(X, Y, p_in_ga(d(e(X))))
p_in_ga(d(e(*(X, Y)))) → U3_ga(X, Y, p_in_ga(d(e(X))))
U1_ga(X, Y, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, p_in_ga(d(e(Y))))
U3_ga(X, Y, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DX, p_in_ga(d(e(Y))))
U2_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U4_ga(X, Y, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ga(x0)
U1_ga(x0, x1, x2)
U3_ga(x0, x1, x2)
U2_ga(x0, x1, x2, x3)
U4_ga(x0, x1, x2, x3)

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

(87) DependencyGraphProof (EQUIVALENT transformation)

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

(88) TRUE

(89) Obligation:

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

P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(90) UsableRulesProof (EQUIVALENT transformation)

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

(91) Obligation:

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

P_IN_AA(d(d(X)), DDX) → P_IN_AA(d(X), DX)

R is empty.
The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
P_IN_AA(x1, x2) = P_IN_AA

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

(92) PiDPToQDPProof (SOUND transformation)

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

(93) Obligation:

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

P_IN_AA → P_IN_AA

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

(94) NonTerminationProof (EQUIVALENT transformation)

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from P_IN_AA to P_IN_AA.

(95) FALSE

(96) Obligation:

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

P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(97) UsableRulesProof (EQUIVALENT transformation)

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

(98) Obligation:

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

P_IN_GA(d(d(X)), DDX) → P_IN_GA(d(X), DX)

R is empty.
The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
P_IN_GA(x1, x2) = P_IN_GA(x1)

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

(99) PiDPToQDPProof (SOUND transformation)

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

(100) Obligation:

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

P_IN_GA(d(d(X))) → P_IN_GA(d(X))

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

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

P_IN_GA(d(d(X))) → P_IN_GA(d(X))
The graph contains the following edges 1 > 1

(102) TRUE

(103) Obligation:

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

U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(104) UsableRulesProof (EQUIVALENT transformation)

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

(105) Obligation:

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

U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The argument filtering Pi contains the following mapping:
const(x1) = const
1 = 1
0 = 0
+(x1, x2) = +(x1, x2)
*(x1, x2) = *(x1, x2)
p_in_gg(x1, x2) = p_in_gg(x1, x2)
d(x1) = d(x1)
e(x1) = e(x1)
t = t
p_out_gg(x1, x2) = p_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4, x5) = U1_gg(x1, x2, x3, x4, x5)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x1, x2, x3, x4, x5)
U4_gg(x1, x2, x3, x4, x5) = U4_gg(x1, x2, x3, x4, x5)
U2_gg(x1, x2, x3, x4, x5) = U2_gg(x1, x2, x3, x4, x5)
P_IN_GG(x1, x2) = P_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4, x5) = U1_GG(x1, x2, x3, x4, x5)
U3_GG(x1, x2, x3, x4, x5) = U3_GG(x1, x2, x3, x4, x5)

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

(106) PiDPToQDPProof (SOUND transformation)

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

(107) Obligation:

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

U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_gg(d(e(t)), const) → p_out_gg(d(e(t)), const)
p_in_gg(d(e(const)), const) → p_out_gg(d(e(const)), const)
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_gg(x0, x1)
U1_gg(x0, x1, x2, x3, x4)
U3_gg(x0, x1, x2, x3, x4)
U2_gg(x0, x1, x2, x3, x4)
U4_gg(x0, x1, x2, x3, x4)

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

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

P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → U1_GG(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 2 > 4
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_GG(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
The graph contains the following edges 1 > 1, 2 > 1, 1 > 2, 2 > 2, 2 > 3, 2 > 4
U1_GG(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
The graph contains the following edges 4 >= 2
U3_GG(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → P_IN_GG(d(e(Y)), DY)
The graph contains the following edges 3 >= 2
P_IN_GG(d(e(+(X, Y))), +(DX, DY)) → P_IN_GG(d(e(X)), DX)
The graph contains the following edges 2 > 2
P_IN_GG(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → P_IN_GG(d(e(X)), DX)
The graph contains the following edges 2 > 2

(109) TRUE

(110) Obligation:

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

U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
p_in_gg(d(d(X)), DDX) → U5_gg(X, DDX, p_in_ga(d(X), DX))
p_in_ga(d(e(t)), const(1)) → p_out_ga(d(e(t)), const(1))
p_in_ga(d(e(const(A))), const(0)) → p_out_ga(d(e(const(A))), const(0))
p_in_ga(d(e(+(X, Y))), +(DX, DY)) → U1_ga(X, Y, DX, DY, p_in_ga(d(e(X)), DX))
p_in_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ga(X, Y, DY, DX, p_in_ga(d(e(X)), DX))
p_in_ga(d(d(X)), DDX) → U5_ga(X, DDX, p_in_ga(d(X), DX))
U5_ga(X, DDX, p_out_ga(d(X), DX)) → U6_ga(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_ga(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_ga(d(d(X)), DDX)
U3_ga(X, Y, DY, DX, p_out_ga(d(e(X)), DX)) → U4_ga(X, Y, DY, DX, p_in_ga(d(e(Y)), DY))
U4_ga(X, Y, DY, DX, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_ga(X, Y, DX, DY, p_out_ga(d(e(X)), DX)) → U2_ga(X, Y, DX, DY, p_in_ga(d(e(Y)), DY))
U2_ga(X, Y, DX, DY, p_out_ga(d(e(Y)), DY)) → p_out_ga(d(e(+(X, Y))), +(DX, DY))
U5_gg(X, DDX, p_out_ga(d(X), DX)) → U6_gg(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_gg(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_gg(d(d(X)), DDX)
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
p_in_ag(d(d(X)), DDX) → U5_ag(X, DDX, p_in_aa(d(X), DX))
p_in_aa(d(e(t)), const(1)) → p_out_aa(d(e(t)), const(1))
p_in_aa(d(e(const(A))), const(0)) → p_out_aa(d(e(const(A))), const(0))
p_in_aa(d(e(+(X, Y))), +(DX, DY)) → U1_aa(X, Y, DX, DY, p_in_aa(d(e(X)), DX))
p_in_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_aa(X, Y, DY, DX, p_in_aa(d(e(X)), DX))
p_in_aa(d(d(X)), DDX) → U5_aa(X, DDX, p_in_aa(d(X), DX))
U5_aa(X, DDX, p_out_aa(d(X), DX)) → U6_aa(X, DDX, DX, p_in_ga(d(e(DX)), DDX))
U6_aa(X, DDX, DX, p_out_ga(d(e(DX)), DDX)) → p_out_aa(d(d(X)), DDX)
U3_aa(X, Y, DY, DX, p_out_aa(d(e(X)), DX)) → U4_aa(X, Y, DY, DX, p_in_aa(d(e(Y)), DY))
U4_aa(X, Y, DY, DX, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_aa(X, Y, DX, DY, p_out_aa(d(e(X)), DX)) → U2_aa(X, Y, DX, DY, p_in_aa(d(e(Y)), DY))
U2_aa(X, Y, DX, DY, p_out_aa(d(e(Y)), DY)) → p_out_aa(d(e(+(X, Y))), +(DX, DY))
U5_ag(X, DDX, p_out_aa(d(X), DX)) → U6_ag(X, DDX, DX, p_in_gg(d(e(DX)), DDX))
U6_ag(X, DDX, DX, p_out_gg(d(e(DX)), DDX)) → p_out_ag(d(d(X)), DDX)
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))

(111) UsableRulesProof (EQUIVALENT transformation)

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

(112) Obligation:

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

U1_AG(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(d(e(Y)), DY)
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → U1_AG(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
P_IN_AG(d(e(+(X, Y))), +(DX, DY)) → P_IN_AG(d(e(X)), DX)

The TRS R consists of the following rules:

p_in_ag(d(e(t)), const(1)) → p_out_ag(d(e(t)), const(1))
p_in_ag(d(e(const(A))), const(0)) → p_out_ag(d(e(const(A))), const(0))
p_in_ag(d(e(+(X, Y))), +(DX, DY)) → U1_ag(X, Y, DX, DY, p_in_ag(d(e(X)), DX))
p_in_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U1_ag(X, Y, DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, Y, DX, DY, p_in_ag(d(e(Y)), DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_ag(X, Y, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))
p_in_gg(d(e(t)), const(1)) → p_out_gg(d(e(t)), const(1))
p_in_gg(d(e(const(A))), const(0)) → p_out_gg(d(e(const(A))), const(0))
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

(113) PiDPToQDPProof (SOUND transformation)

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

(114) Obligation:

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

U1_AG(DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(DY)
P_IN_AG(+(DX, DY)) → U1_AG(DX, DY, p_in_ag(DX))
P_IN_AG(+(DX, DY)) → P_IN_AG(DX)

The TRS R consists of the following rules:

p_in_ag(const) → p_out_ag(d(e(t)), const)
p_in_ag(const) → p_out_ag(d(e(const)), const)
p_in_ag(+(DX, DY)) → U1_ag(DX, DY, p_in_ag(DX))
p_in_ag(+(*(X, DY), *(Y, DX))) → U3_ag(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U1_ag(DX, DY, p_out_ag(d(e(X)), DX)) → U2_ag(X, DX, DY, p_in_ag(DY))
U3_ag(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_ag(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_ag(X, DX, DY, p_out_ag(d(e(Y)), DY)) → p_out_ag(d(e(+(X, Y))), +(DX, DY))
p_in_gg(d(e(t)), const) → p_out_gg(d(e(t)), const)
p_in_gg(d(e(const)), const) → p_out_gg(d(e(const)), const)
p_in_gg(d(e(+(X, Y))), +(DX, DY)) → U1_gg(X, Y, DX, DY, p_in_gg(d(e(X)), DX))
p_in_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) → U3_gg(X, Y, DY, DX, p_in_gg(d(e(X)), DX))
U4_ag(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_ag(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))
U1_gg(X, Y, DX, DY, p_out_gg(d(e(X)), DX)) → U2_gg(X, Y, DX, DY, p_in_gg(d(e(Y)), DY))
U3_gg(X, Y, DY, DX, p_out_gg(d(e(X)), DX)) → U4_gg(X, Y, DY, DX, p_in_gg(d(e(Y)), DY))
U2_gg(X, Y, DX, DY, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(+(X, Y))), +(DX, DY))
U4_gg(X, Y, DY, DX, p_out_gg(d(e(Y)), DY)) → p_out_gg(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))

The set Q consists of the following terms:

p_in_ag(x0)
U1_ag(x0, x1, x2)
U3_ag(x0, x1, x2, x3, x4)
U2_ag(x0, x1, x2, x3)
p_in_gg(x0, x1)
U4_ag(x0, x1, x2, x3, x4)
U1_gg(x0, x1, x2, x3, x4)
U3_gg(x0, x1, x2, x3, x4)
U2_gg(x0, x1, x2, x3, x4)
U4_gg(x0, x1, x2, x3, x4)

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

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

P_IN_AG(+(DX, DY)) → U1_AG(DX, DY, p_in_ag(DX))
The graph contains the following edges 1 > 1, 1 > 2
P_IN_AG(+(DX, DY)) → P_IN_AG(DX)
The graph contains the following edges 1 > 1
U1_AG(DX, DY, p_out_ag(d(e(X)), DX)) → P_IN_AG(DY)
The graph contains the following edges 2 >= 1