0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 62 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 19 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 22 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 4 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 TRUE
logA_in_ga(0, s(0)) → logA_out_ga(0, s(0))
logA_in_ga(s(0), s(s(0))) → logA_out_ga(s(0), s(s(0)))
logA_in_ga(s(s(T10)), s(T7)) → U1_ga(T10, T7, pB_in_gaa(T10, X18, T7))
pB_in_gaa(T10, T11, T7) → U3_gaa(T10, T11, T7, halfC_in_ga(T10, T11))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14)), s(X27)) → U2_ga(T14, X27, halfC_in_ga(T14, X27))
U2_ga(T14, X27, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
U3_gaa(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_gaa(T10, T11, T7, logA_in_ga(s(T11), T7))
U4_gaa(T10, T11, T7, logA_out_ga(s(T11), T7)) → pB_out_gaa(T10, T11, T7)
U1_ga(T10, T7, pB_out_gaa(T10, X18, T7)) → logA_out_ga(s(s(T10)), s(T7))
LOGA_IN_GA(s(s(T10)), s(T7)) → U1_GA(T10, T7, pB_in_gaa(T10, X18, T7))
LOGA_IN_GA(s(s(T10)), s(T7)) → PB_IN_GAA(T10, X18, T7)
PB_IN_GAA(T10, T11, T7) → U3_GAA(T10, T11, T7, halfC_in_ga(T10, T11))
PB_IN_GAA(T10, T11, T7) → HALFC_IN_GA(T10, T11)
HALFC_IN_GA(s(s(T14)), s(X27)) → U2_GA(T14, X27, halfC_in_ga(T14, X27))
HALFC_IN_GA(s(s(T14)), s(X27)) → HALFC_IN_GA(T14, X27)
U3_GAA(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_GAA(T10, T11, T7, logA_in_ga(s(T11), T7))
U3_GAA(T10, T11, T7, halfC_out_ga(T10, T11)) → LOGA_IN_GA(s(T11), T7)
logA_in_ga(0, s(0)) → logA_out_ga(0, s(0))
logA_in_ga(s(0), s(s(0))) → logA_out_ga(s(0), s(s(0)))
logA_in_ga(s(s(T10)), s(T7)) → U1_ga(T10, T7, pB_in_gaa(T10, X18, T7))
pB_in_gaa(T10, T11, T7) → U3_gaa(T10, T11, T7, halfC_in_ga(T10, T11))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14)), s(X27)) → U2_ga(T14, X27, halfC_in_ga(T14, X27))
U2_ga(T14, X27, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
U3_gaa(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_gaa(T10, T11, T7, logA_in_ga(s(T11), T7))
U4_gaa(T10, T11, T7, logA_out_ga(s(T11), T7)) → pB_out_gaa(T10, T11, T7)
U1_ga(T10, T7, pB_out_gaa(T10, X18, T7)) → logA_out_ga(s(s(T10)), s(T7))
LOGA_IN_GA(s(s(T10)), s(T7)) → U1_GA(T10, T7, pB_in_gaa(T10, X18, T7))
LOGA_IN_GA(s(s(T10)), s(T7)) → PB_IN_GAA(T10, X18, T7)
PB_IN_GAA(T10, T11, T7) → U3_GAA(T10, T11, T7, halfC_in_ga(T10, T11))
PB_IN_GAA(T10, T11, T7) → HALFC_IN_GA(T10, T11)
HALFC_IN_GA(s(s(T14)), s(X27)) → U2_GA(T14, X27, halfC_in_ga(T14, X27))
HALFC_IN_GA(s(s(T14)), s(X27)) → HALFC_IN_GA(T14, X27)
U3_GAA(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_GAA(T10, T11, T7, logA_in_ga(s(T11), T7))
U3_GAA(T10, T11, T7, halfC_out_ga(T10, T11)) → LOGA_IN_GA(s(T11), T7)
logA_in_ga(0, s(0)) → logA_out_ga(0, s(0))
logA_in_ga(s(0), s(s(0))) → logA_out_ga(s(0), s(s(0)))
logA_in_ga(s(s(T10)), s(T7)) → U1_ga(T10, T7, pB_in_gaa(T10, X18, T7))
pB_in_gaa(T10, T11, T7) → U3_gaa(T10, T11, T7, halfC_in_ga(T10, T11))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14)), s(X27)) → U2_ga(T14, X27, halfC_in_ga(T14, X27))
U2_ga(T14, X27, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
U3_gaa(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_gaa(T10, T11, T7, logA_in_ga(s(T11), T7))
U4_gaa(T10, T11, T7, logA_out_ga(s(T11), T7)) → pB_out_gaa(T10, T11, T7)
U1_ga(T10, T7, pB_out_gaa(T10, X18, T7)) → logA_out_ga(s(s(T10)), s(T7))
HALFC_IN_GA(s(s(T14)), s(X27)) → HALFC_IN_GA(T14, X27)
logA_in_ga(0, s(0)) → logA_out_ga(0, s(0))
logA_in_ga(s(0), s(s(0))) → logA_out_ga(s(0), s(s(0)))
logA_in_ga(s(s(T10)), s(T7)) → U1_ga(T10, T7, pB_in_gaa(T10, X18, T7))
pB_in_gaa(T10, T11, T7) → U3_gaa(T10, T11, T7, halfC_in_ga(T10, T11))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14)), s(X27)) → U2_ga(T14, X27, halfC_in_ga(T14, X27))
U2_ga(T14, X27, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
U3_gaa(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_gaa(T10, T11, T7, logA_in_ga(s(T11), T7))
U4_gaa(T10, T11, T7, logA_out_ga(s(T11), T7)) → pB_out_gaa(T10, T11, T7)
U1_ga(T10, T7, pB_out_gaa(T10, X18, T7)) → logA_out_ga(s(s(T10)), s(T7))
HALFC_IN_GA(s(s(T14)), s(X27)) → HALFC_IN_GA(T14, X27)
HALFC_IN_GA(s(s(T14))) → HALFC_IN_GA(T14)
From the DPs we obtained the following set of size-change graphs:
LOGA_IN_GA(s(s(T10)), s(T7)) → PB_IN_GAA(T10, X18, T7)
PB_IN_GAA(T10, T11, T7) → U3_GAA(T10, T11, T7, halfC_in_ga(T10, T11))
U3_GAA(T10, T11, T7, halfC_out_ga(T10, T11)) → LOGA_IN_GA(s(T11), T7)
logA_in_ga(0, s(0)) → logA_out_ga(0, s(0))
logA_in_ga(s(0), s(s(0))) → logA_out_ga(s(0), s(s(0)))
logA_in_ga(s(s(T10)), s(T7)) → U1_ga(T10, T7, pB_in_gaa(T10, X18, T7))
pB_in_gaa(T10, T11, T7) → U3_gaa(T10, T11, T7, halfC_in_ga(T10, T11))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14)), s(X27)) → U2_ga(T14, X27, halfC_in_ga(T14, X27))
U2_ga(T14, X27, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
U3_gaa(T10, T11, T7, halfC_out_ga(T10, T11)) → U4_gaa(T10, T11, T7, logA_in_ga(s(T11), T7))
U4_gaa(T10, T11, T7, logA_out_ga(s(T11), T7)) → pB_out_gaa(T10, T11, T7)
U1_ga(T10, T7, pB_out_gaa(T10, X18, T7)) → logA_out_ga(s(s(T10)), s(T7))
LOGA_IN_GA(s(s(T10)), s(T7)) → PB_IN_GAA(T10, X18, T7)
PB_IN_GAA(T10, T11, T7) → U3_GAA(T10, T11, T7, halfC_in_ga(T10, T11))
U3_GAA(T10, T11, T7, halfC_out_ga(T10, T11)) → LOGA_IN_GA(s(T11), T7)
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14)), s(X27)) → U2_ga(T14, X27, halfC_in_ga(T14, X27))
U2_ga(T14, X27, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
LOGA_IN_GA(s(s(T10))) → PB_IN_GAA(T10)
PB_IN_GAA(T10) → U3_GAA(T10, halfC_in_ga(T10))
U3_GAA(T10, halfC_out_ga(T10, T11)) → LOGA_IN_GA(s(T11))
halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14))) → U2_ga(T14, halfC_in_ga(T14))
U2_ga(T14, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
halfC_in_ga(x0)
U2_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LOGA_IN_GA(s(s(T10))) → PB_IN_GAA(T10)
POL(0) = 0
POL(LOGA_IN_GA(x1)) = x1
POL(PB_IN_GAA(x1)) = 1 + x1
POL(U2_ga(x1, x2)) = 1 + x2
POL(U3_GAA(x1, x2)) = 1 + x2
POL(halfC_in_ga(x1)) = x1
POL(halfC_out_ga(x1, x2)) = x2
POL(s(x1)) = 1 + x1
halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14))) → U2_ga(T14, halfC_in_ga(T14))
U2_ga(T14, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
PB_IN_GAA(T10) → U3_GAA(T10, halfC_in_ga(T10))
U3_GAA(T10, halfC_out_ga(T10, T11)) → LOGA_IN_GA(s(T11))
halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T14))) → U2_ga(T14, halfC_in_ga(T14))
U2_ga(T14, halfC_out_ga(T14, X27)) → halfC_out_ga(s(s(T14)), s(X27))
halfC_in_ga(x0)
U2_ga(x0, x1)