(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(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

p29(T38, T42, T39, T43, T10, T44) :- p1(d(e(T38)), T42).
p29(T38, T42, T39, T45, T10, T46) :- ','(pc1(d(e(T38)), T42), p1(d(e(T39)), T45)).
p29(T38, T42, T39, T45, T10, T47) :- ','(pc1(d(e(T38)), T42), ','(pc1(d(e(T39)), T45), p1(d(e(T10)), T47))).
p65(e(t), const(1), T138) :- p1(d(e(const(1))), T138).
p65(e(const(T143)), const(0), T138) :- p1(d(e(const(0))), T138).
p65(e(+(T152, T153)), +(X214, X215), T138) :- p1(d(e(T152)), X214).
p65(e(+(T152, T153)), +(T154, X215), T138) :- ','(pc1(d(e(T152)), T154), p1(d(e(T153)), X215)).
p65(e(+(T152, T153)), +(T154, T155), T138) :- ','(pc1(d(e(T152)), T154), ','(pc1(d(e(T153)), T155), p1(d(e(+(T154, T155))), T138))).
p65(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) :- p1(d(e(T168)), X255).
p65(e(*(T168, T169)), +(*(T168, X254), *(T169, T170)), T138) :- ','(pc1(d(e(T168)), T170), p1(d(e(T169)), X254)).
p65(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) :- ','(pc1(d(e(T168)), T170), ','(pc1(d(e(T169)), T171), p1(d(e(+(*(T168, T171), *(T169, T170)))), T138))).
p65(d(T180), X276, T138) :- p1(d(T180), X275).
p65(d(T180), X276, T138) :- ','(pc1(d(T180), T181), p65(e(T181), X276, T138)).
p1(d(e(+(t, T10))), +(const(1), T15)) :- p1(d(e(T10)), T15).
p1(d(e(+(const(T20), T10))), +(const(0), T21)) :- p1(d(e(T10)), T21).
p1(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) :- p29(T38, T42, T39, T43, T10, T44).
p1(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) :- p29(T64, T68, T65, T69, T10, T70).
p1(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) :- p1(d(e(T76)), T81).
p1(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) :- p1(d(e(T76)), T87).
p1(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) :- p29(T104, T108, T105, T109, T76, T110).
p1(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) :- p29(T127, T131, T128, T132, T76, T133).
p1(d(d(T136)), T138) :- p65(T136, X173, T138).

Clauses:

pc1(d(e(t)), const(1)).
pc1(d(e(const(T4))), const(0)).
pc1(d(e(+(t, T10))), +(const(1), T15)) :- pc1(d(e(T10)), T15).
pc1(d(e(+(const(T20), T10))), +(const(0), T21)) :- pc1(d(e(T10)), T21).
pc1(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) :- qc29(T38, T42, T39, T43, T10, T44).
pc1(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) :- qc29(T64, T68, T65, T69, T10, T70).
pc1(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) :- pc1(d(e(T76)), T81).
pc1(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) :- pc1(d(e(T76)), T87).
pc1(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) :- qc29(T104, T108, T105, T109, T76, T110).
pc1(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) :- qc29(T127, T131, T128, T132, T76, T133).
pc1(d(d(T136)), T138) :- qc65(T136, X173, T138).
qc29(T38, T42, T39, T45, T10, T47) :- ','(pc1(d(e(T38)), T42), ','(pc1(d(e(T39)), T45), pc1(d(e(T10)), T47))).
qc65(e(t), const(1), T138) :- pc1(d(e(const(1))), T138).
qc65(e(const(T143)), const(0), T138) :- pc1(d(e(const(0))), T138).
qc65(e(+(T152, T153)), +(T154, T155), T138) :- ','(pc1(d(e(T152)), T154), ','(pc1(d(e(T153)), T155), pc1(d(e(+(T154, T155))), T138))).
qc65(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) :- ','(pc1(d(e(T168)), T170), ','(pc1(d(e(T169)), T171), pc1(d(e(+(*(T168, T171), *(T169, T170)))), T138))).
qc65(d(T180), X276, T138) :- ','(pc1(d(T180), T181), qc65(e(T181), X276, T138)).

Afs:

p1(x1, x2)  =  p1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
p1_in: (b,f)
p29_in: (b,f,b,f,b,f)
pc1_in: (b,f)
qc29_in: (b,f,b,f,b,f)
qc65_in: (b,f,f)
p65_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → U24_GA(T10, T15, p1_in_ga(d(e(T10)), T15))
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → U25_GA(T20, T10, T21, p1_in_ga(d(e(T10)), T21))
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U26_GA(T38, T39, T10, T42, T43, T44, p29_in_gagaga(T38, T42, T39, T43, T10, T44))
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → U1_GAGAGA(T38, T42, T39, T43, T10, T44, p1_in_ga(d(e(T38)), T42))
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U27_GA(T64, T65, T10, T69, T68, T70, p29_in_gagaga(T64, T68, T65, T69, T10, T70))
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → U3_GAGAGA(T38, T42, T39, T45, T10, T46, p1_in_ga(d(e(T39)), T45))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U28_GA(T76, T81, p1_in_ga(d(e(T76)), T81))
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U29_GA(T86, T76, T87, p1_in_ga(d(e(T76)), T87))
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U30_GA(T104, T105, T76, T110, T108, T109, p29_in_gagaga(T104, T108, T105, T109, T76, T110))
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U6_GAGAGA(T38, T42, T39, T45, T10, T47, p1_in_ga(d(e(T10)), T47))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U31_GA(T127, T128, T76, T133, T132, T131, p29_in_gagaga(T127, T131, T128, T132, T76, T133))
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)
P1_IN_GA(d(d(T136)), T138) → U32_GA(T136, T138, p65_in_gaa(T136, X173, T138))
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)
P65_IN_GAA(e(t), const(1), T138) → U7_GAA(T138, p1_in_ga(d(e(const(1))), T138))
P65_IN_GAA(e(t), const(1), T138) → P1_IN_GA(d(e(const(1))), T138)
P65_IN_GAA(e(const(T143)), const(0), T138) → U8_GAA(T143, T138, p1_in_ga(d(e(const(0))), T138))
P65_IN_GAA(e(const(T143)), const(0), T138) → P1_IN_GA(d(e(const(0))), T138)
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → U9_GAA(T152, T153, X214, X215, T138, p1_in_ga(d(e(T152)), X214))
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → P1_IN_GA(d(e(T152)), X214)
P65_IN_GAA(e(+(T152, T153)), +(T154, X215), T138) → U10_GAA(T152, T153, T154, X215, T138, pc1_in_ga(d(e(T152)), T154))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → U11_GAA(T152, T153, T154, X215, T138, p1_in_ga(d(e(T153)), X215))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → P1_IN_GA(d(e(T153)), X215)
P65_IN_GAA(e(+(T152, T153)), +(T154, T155), T138) → U12_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U12_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U13_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U14_GAA(T152, T153, T154, T155, T138, p1_in_ga(d(e(+(T154, T155))), T138))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → P1_IN_GA(d(e(+(T154, T155))), T138)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → U15_GAA(T168, T169, X254, X255, T138, p1_in_ga(d(e(T168)), X255))
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → P1_IN_GA(d(e(T168)), X255)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, T170)), T138) → U16_GAA(T168, T169, X254, T170, T138, pc1_in_ga(d(e(T168)), T170))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U17_GAA(T168, T169, X254, T170, T138, p1_in_ga(d(e(T169)), X254))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → P1_IN_GA(d(e(T169)), X254)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U18_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U18_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U19_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U20_GAA(T168, T169, T171, T170, T138, p1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → P1_IN_GA(d(e(+(*(T168, T171), *(T169, T170)))), T138)
P65_IN_GAA(d(T180), X276, T138) → U21_GAA(T180, X276, T138, p1_in_ga(d(T180), X275))
P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P65_IN_GAA(d(T180), X276, T138) → U22_GAA(T180, X276, T138, pc1_in_ga(d(T180), T181))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U23_GAA(T180, X276, T138, p65_in_gaa(e(T181), X276, T138))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → P65_IN_GAA(e(T181), X276, T138)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
p1_in_ga(x1, x2)  =  p1_in_ga(x1)
d(x1)  =  d(x1)
e(x1)  =  e(x1)
+(x1, x2)  =  +(x1, x2)
t  =  t
const(x1)  =  const(x1)
p29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  p29_in_gagaga(x1, x3, x5)
*(x1, x2)  =  *(x1, x2)
pc1_in_ga(x1, x2)  =  pc1_in_ga(x1)
pc1_out_ga(x1, x2)  =  pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7)  =  U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7)  =  U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7)  =  U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7)  =  U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3)  =  qc65_in_gaa(x1)
U46_gaa(x1, x2)  =  U46_gaa(x2)
1  =  1
qc65_out_gaa(x1, x2, x3)  =  qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3)  =  U47_gaa(x1, x3)
0  =  0
U48_gaa(x1, x2, x3, x4, x5, x6)  =  U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6)  =  U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6)  =  U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6)  =  U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6)  =  U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6)  =  U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4)  =  U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4)  =  U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U45_gagaga(x1, x2, x3, x4, x5, x7)
p65_in_gaa(x1, x2, x3)  =  p65_in_gaa(x1)
P1_IN_GA(x1, x2)  =  P1_IN_GA(x1)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x2, x4)
U26_GA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GA(x1, x2, x3, x7)
P29_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  P29_IN_GAGAGA(x1, x3, x5)
U1_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GAGAGA(x1, x3, x5, x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7)  =  U27_GA(x1, x2, x3, x7)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GAGAGA(x1, x3, x5, x7)
U3_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U3_GAGAGA(x1, x3, x5, x7)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U29_GA(x1, x2, x3, x4)  =  U29_GA(x1, x2, x4)
U30_GA(x1, x2, x3, x4, x5, x6, x7)  =  U30_GA(x1, x2, x3, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAGAGA(x1, x3, x5, x7)
U31_GA(x1, x2, x3, x4, x5, x6, x7)  =  U31_GA(x1, x2, x3, x7)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
P65_IN_GAA(x1, x2, x3)  =  P65_IN_GAA(x1)
U7_GAA(x1, x2)  =  U7_GAA(x2)
U8_GAA(x1, x2, x3)  =  U8_GAA(x1, x3)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x6)
U10_GAA(x1, x2, x3, x4, x5, x6)  =  U10_GAA(x1, x2, x6)
U11_GAA(x1, x2, x3, x4, x5, x6)  =  U11_GAA(x1, x2, x6)
U12_GAA(x1, x2, x3, x4, x5, x6)  =  U12_GAA(x1, x2, x6)
U13_GAA(x1, x2, x3, x4, x5, x6)  =  U13_GAA(x1, x2, x3, x6)
U14_GAA(x1, x2, x3, x4, x5, x6)  =  U14_GAA(x1, x2, x6)
U15_GAA(x1, x2, x3, x4, x5, x6)  =  U15_GAA(x1, x2, x6)
U16_GAA(x1, x2, x3, x4, x5, x6)  =  U16_GAA(x1, x2, x6)
U17_GAA(x1, x2, x3, x4, x5, x6)  =  U17_GAA(x1, x2, x6)
U18_GAA(x1, x2, x3, x4, x5, x6)  =  U18_GAA(x1, x2, x6)
U19_GAA(x1, x2, x3, x4, x5, x6)  =  U19_GAA(x1, x2, x4, x6)
U20_GAA(x1, x2, x3, x4, x5, x6)  =  U20_GAA(x1, x2, x6)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x4)
U22_GAA(x1, x2, x3, x4)  =  U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4)  =  U23_GAA(x1, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → U24_GA(T10, T15, p1_in_ga(d(e(T10)), T15))
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → U25_GA(T20, T10, T21, p1_in_ga(d(e(T10)), T21))
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U26_GA(T38, T39, T10, T42, T43, T44, p29_in_gagaga(T38, T42, T39, T43, T10, T44))
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → U1_GAGAGA(T38, T42, T39, T43, T10, T44, p1_in_ga(d(e(T38)), T42))
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U27_GA(T64, T65, T10, T69, T68, T70, p29_in_gagaga(T64, T68, T65, T69, T10, T70))
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → U3_GAGAGA(T38, T42, T39, T45, T10, T46, p1_in_ga(d(e(T39)), T45))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U28_GA(T76, T81, p1_in_ga(d(e(T76)), T81))
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U29_GA(T86, T76, T87, p1_in_ga(d(e(T76)), T87))
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U30_GA(T104, T105, T76, T110, T108, T109, p29_in_gagaga(T104, T108, T105, T109, T76, T110))
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U6_GAGAGA(T38, T42, T39, T45, T10, T47, p1_in_ga(d(e(T10)), T47))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U31_GA(T127, T128, T76, T133, T132, T131, p29_in_gagaga(T127, T131, T128, T132, T76, T133))
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)
P1_IN_GA(d(d(T136)), T138) → U32_GA(T136, T138, p65_in_gaa(T136, X173, T138))
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)
P65_IN_GAA(e(t), const(1), T138) → U7_GAA(T138, p1_in_ga(d(e(const(1))), T138))
P65_IN_GAA(e(t), const(1), T138) → P1_IN_GA(d(e(const(1))), T138)
P65_IN_GAA(e(const(T143)), const(0), T138) → U8_GAA(T143, T138, p1_in_ga(d(e(const(0))), T138))
P65_IN_GAA(e(const(T143)), const(0), T138) → P1_IN_GA(d(e(const(0))), T138)
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → U9_GAA(T152, T153, X214, X215, T138, p1_in_ga(d(e(T152)), X214))
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → P1_IN_GA(d(e(T152)), X214)
P65_IN_GAA(e(+(T152, T153)), +(T154, X215), T138) → U10_GAA(T152, T153, T154, X215, T138, pc1_in_ga(d(e(T152)), T154))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → U11_GAA(T152, T153, T154, X215, T138, p1_in_ga(d(e(T153)), X215))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → P1_IN_GA(d(e(T153)), X215)
P65_IN_GAA(e(+(T152, T153)), +(T154, T155), T138) → U12_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U12_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U13_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U14_GAA(T152, T153, T154, T155, T138, p1_in_ga(d(e(+(T154, T155))), T138))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → P1_IN_GA(d(e(+(T154, T155))), T138)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → U15_GAA(T168, T169, X254, X255, T138, p1_in_ga(d(e(T168)), X255))
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → P1_IN_GA(d(e(T168)), X255)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, T170)), T138) → U16_GAA(T168, T169, X254, T170, T138, pc1_in_ga(d(e(T168)), T170))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U17_GAA(T168, T169, X254, T170, T138, p1_in_ga(d(e(T169)), X254))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → P1_IN_GA(d(e(T169)), X254)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U18_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U18_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U19_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U20_GAA(T168, T169, T171, T170, T138, p1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → P1_IN_GA(d(e(+(*(T168, T171), *(T169, T170)))), T138)
P65_IN_GAA(d(T180), X276, T138) → U21_GAA(T180, X276, T138, p1_in_ga(d(T180), X275))
P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P65_IN_GAA(d(T180), X276, T138) → U22_GAA(T180, X276, T138, pc1_in_ga(d(T180), T181))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U23_GAA(T180, X276, T138, p65_in_gaa(e(T181), X276, T138))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → P65_IN_GAA(e(T181), X276, T138)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
p1_in_ga(x1, x2)  =  p1_in_ga(x1)
d(x1)  =  d(x1)
e(x1)  =  e(x1)
+(x1, x2)  =  +(x1, x2)
t  =  t
const(x1)  =  const(x1)
p29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  p29_in_gagaga(x1, x3, x5)
*(x1, x2)  =  *(x1, x2)
pc1_in_ga(x1, x2)  =  pc1_in_ga(x1)
pc1_out_ga(x1, x2)  =  pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7)  =  U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7)  =  U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7)  =  U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7)  =  U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3)  =  qc65_in_gaa(x1)
U46_gaa(x1, x2)  =  U46_gaa(x2)
1  =  1
qc65_out_gaa(x1, x2, x3)  =  qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3)  =  U47_gaa(x1, x3)
0  =  0
U48_gaa(x1, x2, x3, x4, x5, x6)  =  U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6)  =  U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6)  =  U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6)  =  U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6)  =  U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6)  =  U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4)  =  U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4)  =  U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U45_gagaga(x1, x2, x3, x4, x5, x7)
p65_in_gaa(x1, x2, x3)  =  p65_in_gaa(x1)
P1_IN_GA(x1, x2)  =  P1_IN_GA(x1)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x2, x4)
U26_GA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GA(x1, x2, x3, x7)
P29_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  P29_IN_GAGAGA(x1, x3, x5)
U1_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GAGAGA(x1, x3, x5, x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7)  =  U27_GA(x1, x2, x3, x7)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GAGAGA(x1, x3, x5, x7)
U3_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U3_GAGAGA(x1, x3, x5, x7)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U29_GA(x1, x2, x3, x4)  =  U29_GA(x1, x2, x4)
U30_GA(x1, x2, x3, x4, x5, x6, x7)  =  U30_GA(x1, x2, x3, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAGAGA(x1, x3, x5, x7)
U31_GA(x1, x2, x3, x4, x5, x6, x7)  =  U31_GA(x1, x2, x3, x7)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
P65_IN_GAA(x1, x2, x3)  =  P65_IN_GAA(x1)
U7_GAA(x1, x2)  =  U7_GAA(x2)
U8_GAA(x1, x2, x3)  =  U8_GAA(x1, x3)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x6)
U10_GAA(x1, x2, x3, x4, x5, x6)  =  U10_GAA(x1, x2, x6)
U11_GAA(x1, x2, x3, x4, x5, x6)  =  U11_GAA(x1, x2, x6)
U12_GAA(x1, x2, x3, x4, x5, x6)  =  U12_GAA(x1, x2, x6)
U13_GAA(x1, x2, x3, x4, x5, x6)  =  U13_GAA(x1, x2, x3, x6)
U14_GAA(x1, x2, x3, x4, x5, x6)  =  U14_GAA(x1, x2, x6)
U15_GAA(x1, x2, x3, x4, x5, x6)  =  U15_GAA(x1, x2, x6)
U16_GAA(x1, x2, x3, x4, x5, x6)  =  U16_GAA(x1, x2, x6)
U17_GAA(x1, x2, x3, x4, x5, x6)  =  U17_GAA(x1, x2, x6)
U18_GAA(x1, x2, x3, x4, x5, x6)  =  U18_GAA(x1, x2, x6)
U19_GAA(x1, x2, x3, x4, x5, x6)  =  U19_GAA(x1, x2, x4, x6)
U20_GAA(x1, x2, x3, x4, x5, x6)  =  U20_GAA(x1, x2, x6)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x4)
U22_GAA(x1, x2, x3, x4)  =  U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4)  =  U23_GAA(x1, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 38 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
d(x1)  =  d(x1)
e(x1)  =  e(x1)
+(x1, x2)  =  +(x1, x2)
t  =  t
const(x1)  =  const(x1)
*(x1, x2)  =  *(x1, x2)
pc1_in_ga(x1, x2)  =  pc1_in_ga(x1)
pc1_out_ga(x1, x2)  =  pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7)  =  U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7)  =  U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7)  =  U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7)  =  U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3)  =  qc65_in_gaa(x1)
U46_gaa(x1, x2)  =  U46_gaa(x2)
1  =  1
qc65_out_gaa(x1, x2, x3)  =  qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3)  =  U47_gaa(x1, x3)
0  =  0
U48_gaa(x1, x2, x3, x4, x5, x6)  =  U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6)  =  U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6)  =  U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6)  =  U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6)  =  U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6)  =  U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4)  =  U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4)  =  U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U45_gagaga(x1, x2, x3, x4, x5, x7)
P1_IN_GA(x1, x2)  =  P1_IN_GA(x1)
P29_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  P29_IN_GAGAGA(x1, x3, x5)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GAGAGA(x1, x3, x5, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)

The argument filtering Pi contains the following mapping:
d(x1)  =  d(x1)
e(x1)  =  e(x1)
+(x1, x2)  =  +(x1, x2)
t  =  t
const(x1)  =  const(x1)
*(x1, x2)  =  *(x1, x2)
pc1_in_ga(x1, x2)  =  pc1_in_ga(x1)
pc1_out_ga(x1, x2)  =  pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7)  =  U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7)  =  U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7)  =  U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7)  =  U41_ga(x1, x2, x3, x7)
1  =  1
0  =  0
U44_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U45_gagaga(x1, x2, x3, x4, x5, x7)
P1_IN_GA(x1, x2)  =  P1_IN_GA(x1)
P29_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  P29_IN_GAGAGA(x1, x3, x5)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GAGAGA(x1, x3, x5, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)

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:

P1_IN_GA(d(e(+(const(T20), T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(t, T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(+(T38, T39), T10)))) → P29_IN_GAGAGA(T38, T39, T10)
P29_IN_GAGAGA(T38, T39, T10) → P1_IN_GA(d(e(T38)))
P1_IN_GA(d(e(+(*(T64, T65), T10)))) → P29_IN_GAGAGA(T64, T65, T10)
P29_IN_GAGAGA(T38, T39, T10) → U2_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
U2_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)))
P1_IN_GA(d(e(*(t, T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(const(T86), T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(+(T104, T105), T76)))) → P29_IN_GAGAGA(T104, T105, T76)
P29_IN_GAGAGA(T38, T39, T10) → U4_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
U4_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T39))))
U5_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(*(*(T127, T128), T76)))) → P29_IN_GAGAGA(T127, T128, T76)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t))) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4)))) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10)))) → U34_ga(T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(const(T20), T10)))) → U35_ga(T20, T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(+(T38, T39), T10)))) → U36_ga(T38, T39, T10, qc29_in_gagaga(T38, T39, T10))
pc1_in_ga(d(e(+(*(T64, T65), T10)))) → U37_ga(T64, T65, T10, qc29_in_gagaga(T64, T65, T10))
pc1_in_ga(d(e(*(t, T76)))) → U38_ga(T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(const(T86), T76)))) → U39_ga(T86, T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(+(T104, T105), T76)))) → U40_ga(T104, T105, T76, qc29_in_gagaga(T104, T105, T76))
pc1_in_ga(d(e(*(*(T127, T128), T76)))) → U41_ga(T127, T128, T76, qc29_in_gagaga(T127, T128, T76))
U34_ga(T10, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))
U35_ga(T20, T10, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U36_ga(T38, T39, T10, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U37_ga(T64, T65, T10, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
U38_ga(T76, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U39_ga(T86, T76, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U40_ga(T104, T105, T76, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
U41_ga(T127, T128, T76, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
qc29_in_gagaga(T38, T39, T10) → U43_gagaga(T38, T39, T10, pc1_in_ga(d(e(T38))))
U43_gagaga(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T10, pc1_in_ga(d(e(T39))))
U44_gagaga(T38, T42, T39, T10, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, pc1_in_ga(d(e(T10))))
U45_gagaga(T38, T42, T39, T45, T10, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)

The set Q consists of the following terms:

pc1_in_ga(x0)
U34_ga(x0, x1)
U35_ga(x0, x1, x2)
U36_ga(x0, x1, x2, x3)
U37_ga(x0, x1, x2, x3)
U38_ga(x0, x1)
U39_ga(x0, x1, x2)
U40_ga(x0, x1, x2, x3)
U41_ga(x0, x1, x2, x3)
qc29_in_gagaga(x0, x1, x2)
U43_gagaga(x0, x1, x2, x3)
U44_gagaga(x0, x1, x2, x3, x4)
U45_gagaga(x0, x1, x2, x3, x4, x5)

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

(12) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


P1_IN_GA(d(e(+(const(T20), T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(t, T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(+(T38, T39), T10)))) → P29_IN_GAGAGA(T38, T39, T10)
P29_IN_GAGAGA(T38, T39, T10) → P1_IN_GA(d(e(T38)))
P1_IN_GA(d(e(+(*(T64, T65), T10)))) → P29_IN_GAGAGA(T64, T65, T10)
U2_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)))
P1_IN_GA(d(e(*(t, T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(const(T86), T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(+(T104, T105), T76)))) → P29_IN_GAGAGA(T104, T105, T76)
P29_IN_GAGAGA(T38, T39, T10) → U4_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
P1_IN_GA(d(e(*(*(T127, T128), T76)))) → P29_IN_GAGAGA(T127, T128, T76)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x1, x2)) = 1 + x1 + x2   
POL(+(x1, x2)) = 1 + x1 + x2   
POL(0) = 0   
POL(1) = 0   
POL(P1_IN_GA(x1)) = x1   
POL(P29_IN_GAGAGA(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(U2_GAGAGA(x1, x2, x3, x4)) = 1 + x2 + x3   
POL(U34_ga(x1, x2)) = 0   
POL(U35_ga(x1, x2, x3)) = 0   
POL(U36_ga(x1, x2, x3, x4)) = 0   
POL(U37_ga(x1, x2, x3, x4)) = 0   
POL(U38_ga(x1, x2)) = 0   
POL(U39_ga(x1, x2, x3)) = 0   
POL(U40_ga(x1, x2, x3, x4)) = 0   
POL(U41_ga(x1, x2, x3, x4)) = 0   
POL(U43_gagaga(x1, x2, x3, x4)) = 0   
POL(U44_gagaga(x1, x2, x3, x4, x5)) = 0   
POL(U45_gagaga(x1, x2, x3, x4, x5, x6)) = 0   
POL(U4_GAGAGA(x1, x2, x3, x4)) = x2 + x3   
POL(U5_GAGAGA(x1, x2, x3, x4)) = x2 + x3   
POL(const(x1)) = 1   
POL(d(x1)) = x1   
POL(e(x1)) = x1   
POL(pc1_in_ga(x1)) = 0   
POL(pc1_out_ga(x1, x2)) = 0   
POL(qc29_in_gagaga(x1, x2, x3)) = 0   
POL(qc29_out_gagaga(x1, x2, x3, x4, x5, x6)) = 0   
POL(t) = 1   

The following usable rules [FROCOS05] were oriented: none

(13) Obligation:

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

P29_IN_GAGAGA(T38, T39, T10) → U2_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
U4_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T39))))
U5_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)))

The TRS R consists of the following rules:

pc1_in_ga(d(e(t))) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4)))) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10)))) → U34_ga(T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(const(T20), T10)))) → U35_ga(T20, T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(+(T38, T39), T10)))) → U36_ga(T38, T39, T10, qc29_in_gagaga(T38, T39, T10))
pc1_in_ga(d(e(+(*(T64, T65), T10)))) → U37_ga(T64, T65, T10, qc29_in_gagaga(T64, T65, T10))
pc1_in_ga(d(e(*(t, T76)))) → U38_ga(T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(const(T86), T76)))) → U39_ga(T86, T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(+(T104, T105), T76)))) → U40_ga(T104, T105, T76, qc29_in_gagaga(T104, T105, T76))
pc1_in_ga(d(e(*(*(T127, T128), T76)))) → U41_ga(T127, T128, T76, qc29_in_gagaga(T127, T128, T76))
U34_ga(T10, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))
U35_ga(T20, T10, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U36_ga(T38, T39, T10, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U37_ga(T64, T65, T10, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
U38_ga(T76, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U39_ga(T86, T76, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U40_ga(T104, T105, T76, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
U41_ga(T127, T128, T76, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
qc29_in_gagaga(T38, T39, T10) → U43_gagaga(T38, T39, T10, pc1_in_ga(d(e(T38))))
U43_gagaga(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T10, pc1_in_ga(d(e(T39))))
U44_gagaga(T38, T42, T39, T10, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, pc1_in_ga(d(e(T10))))
U45_gagaga(T38, T42, T39, T45, T10, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)

The set Q consists of the following terms:

pc1_in_ga(x0)
U34_ga(x0, x1)
U35_ga(x0, x1, x2)
U36_ga(x0, x1, x2, x3)
U37_ga(x0, x1, x2, x3)
U38_ga(x0, x1)
U39_ga(x0, x1, x2)
U40_ga(x0, x1, x2, x3)
U41_ga(x0, x1, x2, x3)
qc29_in_gagaga(x0, x1, x2)
U43_gagaga(x0, x1, x2, x3)
U44_gagaga(x0, x1, x2, x3, x4)
U45_gagaga(x0, x1, x2, x3, x4, x5)

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

(14) DependencyGraphProof (EQUIVALENT transformation)

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

(15) TRUE

(16) Obligation:

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

P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
d(x1)  =  d(x1)
e(x1)  =  e(x1)
+(x1, x2)  =  +(x1, x2)
t  =  t
const(x1)  =  const(x1)
*(x1, x2)  =  *(x1, x2)
pc1_in_ga(x1, x2)  =  pc1_in_ga(x1)
pc1_out_ga(x1, x2)  =  pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4)  =  U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7)  =  U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7)  =  U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6)  =  qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7)  =  U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7)  =  U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3)  =  qc65_in_gaa(x1)
U46_gaa(x1, x2)  =  U46_gaa(x2)
1  =  1
qc65_out_gaa(x1, x2, x3)  =  qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3)  =  U47_gaa(x1, x3)
0  =  0
U48_gaa(x1, x2, x3, x4, x5, x6)  =  U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6)  =  U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6)  =  U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6)  =  U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6)  =  U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6)  =  U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4)  =  U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4)  =  U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U45_gagaga(x1, x2, x3, x4, x5, x7)
P1_IN_GA(x1, x2)  =  P1_IN_GA(x1)
P65_IN_GAA(x1, x2, x3)  =  P65_IN_GAA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

P65_IN_GAA(d(T180)) → P1_IN_GA(d(T180))
P1_IN_GA(d(d(T136))) → P65_IN_GAA(T136)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • P1_IN_GA(d(d(T136))) → P65_IN_GAA(T136)
    The graph contains the following edges 1 > 1

  • P65_IN_GAA(d(T180)) → P1_IN_GA(d(T180))
    The graph contains the following edges 1 >= 1

(22) YES