0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 71 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 51 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 12 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 26 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 TRUE
divA_in_gga(T7, s(T8), T10) → U1_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U3_gga(T24, T25, lssC_in_gg(T24, T25))
lssC_in_gg(s(T36), s(T37)) → U2_gg(T36, T37, lssC_in_gg(T36, T37))
lssC_in_gg(0, s(T42)) → lssC_out_gg(0, s(T42))
U2_gg(T36, T37, lssC_out_gg(T36, T37)) → lssC_out_gg(s(T36), s(T37))
U3_gga(T24, T25, lssC_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
pD_in_ggaa(T49, T50, T55, T52) → U6_ggaa(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
U6_ggaa(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_ggaa(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U7_ggaa(T49, T50, T55, T52, div_sB_out_gga(T55, T50, T52)) → pD_out_ggaa(T49, T50, T55, T52)
U4_gga(T49, T50, T52, pD_out_ggaa(T49, T50, X49, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U1_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divA_out_gga(T7, s(T8), T10)
DIVA_IN_GGA(T7, s(T8), T10) → U1_GGA(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
DIVA_IN_GGA(T7, s(T8), T10) → DIV_SB_IN_GGA(T7, T8, T10)
DIV_SB_IN_GGA(s(T24), T25, 0) → U3_GGA(T24, T25, lssC_in_gg(T24, T25))
DIV_SB_IN_GGA(s(T24), T25, 0) → LSSC_IN_GG(T24, T25)
LSSC_IN_GG(s(T36), s(T37)) → U2_GG(T36, T37, lssC_in_gg(T36, T37))
LSSC_IN_GG(s(T36), s(T37)) → LSSC_IN_GG(T36, T37)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U4_GGA(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → PD_IN_GGAA(T49, T50, X49, T52)
PD_IN_GGAA(T49, T50, T55, T52) → U6_GGAA(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
PD_IN_GGAA(T49, T50, T55, T52) → SUBE_IN_GGA(T49, T50, T55)
SUBE_IN_GGA(s(T66), s(T67), X77) → U5_GGA(T66, T67, X77, subE_in_gga(T66, T67, X77))
SUBE_IN_GGA(s(T66), s(T67), X77) → SUBE_IN_GGA(T66, T67, X77)
U6_GGAA(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_GGAA(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U6_GGAA(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
divA_in_gga(T7, s(T8), T10) → U1_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U3_gga(T24, T25, lssC_in_gg(T24, T25))
lssC_in_gg(s(T36), s(T37)) → U2_gg(T36, T37, lssC_in_gg(T36, T37))
lssC_in_gg(0, s(T42)) → lssC_out_gg(0, s(T42))
U2_gg(T36, T37, lssC_out_gg(T36, T37)) → lssC_out_gg(s(T36), s(T37))
U3_gga(T24, T25, lssC_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
pD_in_ggaa(T49, T50, T55, T52) → U6_ggaa(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
U6_ggaa(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_ggaa(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U7_ggaa(T49, T50, T55, T52, div_sB_out_gga(T55, T50, T52)) → pD_out_ggaa(T49, T50, T55, T52)
U4_gga(T49, T50, T52, pD_out_ggaa(T49, T50, X49, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U1_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divA_out_gga(T7, s(T8), T10)
DIVA_IN_GGA(T7, s(T8), T10) → U1_GGA(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
DIVA_IN_GGA(T7, s(T8), T10) → DIV_SB_IN_GGA(T7, T8, T10)
DIV_SB_IN_GGA(s(T24), T25, 0) → U3_GGA(T24, T25, lssC_in_gg(T24, T25))
DIV_SB_IN_GGA(s(T24), T25, 0) → LSSC_IN_GG(T24, T25)
LSSC_IN_GG(s(T36), s(T37)) → U2_GG(T36, T37, lssC_in_gg(T36, T37))
LSSC_IN_GG(s(T36), s(T37)) → LSSC_IN_GG(T36, T37)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U4_GGA(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → PD_IN_GGAA(T49, T50, X49, T52)
PD_IN_GGAA(T49, T50, T55, T52) → U6_GGAA(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
PD_IN_GGAA(T49, T50, T55, T52) → SUBE_IN_GGA(T49, T50, T55)
SUBE_IN_GGA(s(T66), s(T67), X77) → U5_GGA(T66, T67, X77, subE_in_gga(T66, T67, X77))
SUBE_IN_GGA(s(T66), s(T67), X77) → SUBE_IN_GGA(T66, T67, X77)
U6_GGAA(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_GGAA(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U6_GGAA(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
divA_in_gga(T7, s(T8), T10) → U1_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U3_gga(T24, T25, lssC_in_gg(T24, T25))
lssC_in_gg(s(T36), s(T37)) → U2_gg(T36, T37, lssC_in_gg(T36, T37))
lssC_in_gg(0, s(T42)) → lssC_out_gg(0, s(T42))
U2_gg(T36, T37, lssC_out_gg(T36, T37)) → lssC_out_gg(s(T36), s(T37))
U3_gga(T24, T25, lssC_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
pD_in_ggaa(T49, T50, T55, T52) → U6_ggaa(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
U6_ggaa(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_ggaa(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U7_ggaa(T49, T50, T55, T52, div_sB_out_gga(T55, T50, T52)) → pD_out_ggaa(T49, T50, T55, T52)
U4_gga(T49, T50, T52, pD_out_ggaa(T49, T50, X49, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U1_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divA_out_gga(T7, s(T8), T10)
SUBE_IN_GGA(s(T66), s(T67), X77) → SUBE_IN_GGA(T66, T67, X77)
divA_in_gga(T7, s(T8), T10) → U1_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U3_gga(T24, T25, lssC_in_gg(T24, T25))
lssC_in_gg(s(T36), s(T37)) → U2_gg(T36, T37, lssC_in_gg(T36, T37))
lssC_in_gg(0, s(T42)) → lssC_out_gg(0, s(T42))
U2_gg(T36, T37, lssC_out_gg(T36, T37)) → lssC_out_gg(s(T36), s(T37))
U3_gga(T24, T25, lssC_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
pD_in_ggaa(T49, T50, T55, T52) → U6_ggaa(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
U6_ggaa(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_ggaa(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U7_ggaa(T49, T50, T55, T52, div_sB_out_gga(T55, T50, T52)) → pD_out_ggaa(T49, T50, T55, T52)
U4_gga(T49, T50, T52, pD_out_ggaa(T49, T50, X49, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U1_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divA_out_gga(T7, s(T8), T10)
SUBE_IN_GGA(s(T66), s(T67), X77) → SUBE_IN_GGA(T66, T67, X77)
SUBE_IN_GGA(s(T66), s(T67)) → SUBE_IN_GGA(T66, T67)
From the DPs we obtained the following set of size-change graphs:
LSSC_IN_GG(s(T36), s(T37)) → LSSC_IN_GG(T36, T37)
divA_in_gga(T7, s(T8), T10) → U1_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U3_gga(T24, T25, lssC_in_gg(T24, T25))
lssC_in_gg(s(T36), s(T37)) → U2_gg(T36, T37, lssC_in_gg(T36, T37))
lssC_in_gg(0, s(T42)) → lssC_out_gg(0, s(T42))
U2_gg(T36, T37, lssC_out_gg(T36, T37)) → lssC_out_gg(s(T36), s(T37))
U3_gga(T24, T25, lssC_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
pD_in_ggaa(T49, T50, T55, T52) → U6_ggaa(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
U6_ggaa(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_ggaa(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U7_ggaa(T49, T50, T55, T52, div_sB_out_gga(T55, T50, T52)) → pD_out_ggaa(T49, T50, T55, T52)
U4_gga(T49, T50, T52, pD_out_ggaa(T49, T50, X49, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U1_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divA_out_gga(T7, s(T8), T10)
LSSC_IN_GG(s(T36), s(T37)) → LSSC_IN_GG(T36, T37)
LSSC_IN_GG(s(T36), s(T37)) → LSSC_IN_GG(T36, T37)
From the DPs we obtained the following set of size-change graphs:
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → PD_IN_GGAA(T49, T50, X49, T52)
PD_IN_GGAA(T49, T50, T55, T52) → U6_GGAA(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
U6_GGAA(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
divA_in_gga(T7, s(T8), T10) → U1_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U3_gga(T24, T25, lssC_in_gg(T24, T25))
lssC_in_gg(s(T36), s(T37)) → U2_gg(T36, T37, lssC_in_gg(T36, T37))
lssC_in_gg(0, s(T42)) → lssC_out_gg(0, s(T42))
U2_gg(T36, T37, lssC_out_gg(T36, T37)) → lssC_out_gg(s(T36), s(T37))
U3_gga(T24, T25, lssC_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, pD_in_ggaa(T49, T50, X49, T52))
pD_in_ggaa(T49, T50, T55, T52) → U6_ggaa(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
U6_ggaa(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → U7_ggaa(T49, T50, T55, T52, div_sB_in_gga(T55, T50, T52))
U7_ggaa(T49, T50, T55, T52, div_sB_out_gga(T55, T50, T52)) → pD_out_ggaa(T49, T50, T55, T52)
U4_gga(T49, T50, T52, pD_out_ggaa(T49, T50, X49, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U1_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divA_out_gga(T7, s(T8), T10)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → PD_IN_GGAA(T49, T50, X49, T52)
PD_IN_GGAA(T49, T50, T55, T52) → U6_GGAA(T49, T50, T55, T52, subE_in_gga(T49, T50, T55))
U6_GGAA(T49, T50, T55, T52, subE_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
subE_in_gga(s(T66), s(T67), X77) → U5_gga(T66, T67, X77, subE_in_gga(T66, T67, X77))
subE_in_gga(T72, 0, T72) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, X77, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
DIV_SB_IN_GGA(s(T49), T50) → PD_IN_GGAA(T49, T50)
PD_IN_GGAA(T49, T50) → U6_GGAA(T49, T50, subE_in_gga(T49, T50))
U6_GGAA(T49, T50, subE_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50)
subE_in_gga(s(T66), s(T67)) → U5_gga(T66, T67, subE_in_gga(T66, T67))
subE_in_gga(T72, 0) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
subE_in_gga(x0, x1)
U5_gga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PD_IN_GGAA(T49, T50) → U6_GGAA(T49, T50, subE_in_gga(T49, T50))
POL(0) = 0
POL(DIV_SB_IN_GGA(x1, x2)) = x1 + x2
POL(PD_IN_GGAA(x1, x2)) = 1 + x1 + x2
POL(U5_gga(x1, x2, x3)) = 1 + x3
POL(U6_GGAA(x1, x2, x3)) = x3
POL(s(x1)) = 1 + x1
POL(subE_in_gga(x1, x2)) = x1
POL(subE_out_gga(x1, x2, x3)) = x2 + x3
subE_in_gga(s(T66), s(T67)) → U5_gga(T66, T67, subE_in_gga(T66, T67))
subE_in_gga(T72, 0) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
DIV_SB_IN_GGA(s(T49), T50) → PD_IN_GGAA(T49, T50)
U6_GGAA(T49, T50, subE_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50)
subE_in_gga(s(T66), s(T67)) → U5_gga(T66, T67, subE_in_gga(T66, T67))
subE_in_gga(T72, 0) → subE_out_gga(T72, 0, T72)
U5_gga(T66, T67, subE_out_gga(T66, T67, X77)) → subE_out_gga(s(T66), s(T67), X77)
subE_in_gga(x0, x1)
U5_gga(x0, x1, x2)