0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 184 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 176 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 PiDPToQDPProof (⇒, 0 ms)
↳9 QDP
↳10 QDPSizeChangeProof (⇔, 0 ms)
↳11 YES
↳12 PiDP
↳13 PiDPToQDPProof (⇒, 0 ms)
↳14 QDP
↳15 QDPSizeChangeProof (⇔, 0 ms)
↳16 YES
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNB_IN_GA(X1, X2) → U1_GA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANNB_IN_GA(X1, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANNC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNC_IN_GA(s(X1), X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermanncB_in_ga(X1, X3))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → U4_GA(X1, X2, ackermannD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3, X2)
ACKERMANND_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANND_IN_GGA(s(X1), 0, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X3)
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermanncB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackermannC_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → ACKERMANNC_IN_GA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermanncC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermanncD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackermannA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5, X3)
ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNB_IN_GA(X1, X2) → U1_GA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANNB_IN_GA(X1, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANNC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNC_IN_GA(s(X1), X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermanncB_in_ga(X1, X3))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → U4_GA(X1, X2, ackermannD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3, X2)
ACKERMANND_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANND_IN_GGA(s(X1), 0, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X3)
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermanncB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackermannC_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → ACKERMANNC_IN_GA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermanncC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermanncD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackermannA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5, X3)
ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)
ACKERMANNB_IN_GA(X1, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANNC_IN_GA(s(X1), X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermanncB_in_ga(X1, X3))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3, X2)
ACKERMANND_IN_GGA(s(X1), 0, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X3)
ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)
ACKERMANNB_IN_GA(X1) → ACKERMANNC_IN_GA(X1)
ACKERMANNC_IN_GA(s(X1)) → ACKERMANNB_IN_GA(X1)
ACKERMANNC_IN_GA(s(X1)) → U3_GA(X1, ackermanncB_in_ga(X1))
U3_GA(X1, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3)
ACKERMANND_IN_GGA(s(X1), 0) → ACKERMANNC_IN_GA(X1)
ACKERMANND_IN_GGA(s(X1), s(X2)) → ACKERMANND_IN_GGA(s(X1), X2)
ACKERMANND_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackermanncD_in_gga(s(X1), X2))
U7_GGA(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4)
ackermanncB_in_ga(X1) → U28_ga(X1, ackermanncC_in_ga(X1))
ackermanncC_in_ga(0) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1)) → U29_ga(X1, ackermanncB_in_ga(X1))
U29_ga(X1, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, ackermanncD_in_gga(X1, X3))
ackermanncD_in_gga(0, X1) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0) → U31_gga(X1, ackermanncC_in_ga(X1))
U31_gga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackermanncD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackermanncD_in_gga(X1, X4))
U33_gga(X1, X2, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)
ackermanncB_in_ga(x0)
ackermanncC_in_ga(x0)
U29_ga(x0, x1)
ackermanncD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)
From the DPs we obtained the following set of size-change graphs:
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermanncB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermanncC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermanncD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5, X3)
ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)
ACKERMANNA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackermanncB_in_ga(X1))
U10_GGA(X1, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackermanncC_in_ga(X1))
U13_GGA(X1, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackermanncD_in_gga(s(X1), X2))
U16_GGA(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackermanncD_in_gga(X1, X4))
U18_GGA(X1, X2, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5)
ackermanncB_in_ga(X1) → U28_ga(X1, ackermanncC_in_ga(X1))
ackermanncC_in_ga(0) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1)) → U29_ga(X1, ackermanncB_in_ga(X1))
U29_ga(X1, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, ackermanncD_in_gga(X1, X3))
ackermanncD_in_gga(0, X1) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0) → U31_gga(X1, ackermanncC_in_ga(X1))
U31_gga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackermanncD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackermanncD_in_gga(X1, X4))
U33_gga(X1, X2, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)
ackermanncB_in_ga(x0)
ackermanncC_in_ga(x0)
U29_ga(x0, x1)
ackermanncD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)
From the DPs we obtained the following set of size-change graphs: