0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 54 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 21 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 6 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 (⇔, 21 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 TRUE
plusA_in_gaa(0, T5, T5) → plusA_out_gaa(0, T5, T5)
plusA_in_gaa(s(0), T20, s(T20)) → plusA_out_gaa(s(0), T20, s(T20))
plusA_in_gaa(s(s(T23)), T12, s(T13)) → U1_gaa(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
pB_in_gaaa(T23, T24, T12, T13) → U3_gaaa(T23, T24, T12, T13, pC_in_ga(T23, T24))
pC_in_ga(s(T27), s(X40)) → U2_ga(T27, X40, pC_in_ga(T27, X40))
U2_ga(T27, X40, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
U3_gaaa(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_gaaa(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U4_gaaa(T23, T24, T12, T13, plusA_out_gaa(s(s(T24)), T12, T13)) → pB_out_gaaa(T23, T24, T12, T13)
U1_gaa(T23, T12, T13, pB_out_gaaa(T23, X31, T12, T13)) → plusA_out_gaa(s(s(T23)), T12, s(T13))
PLUSA_IN_GAA(s(s(T23)), T12, s(T13)) → U1_GAA(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
PLUSA_IN_GAA(s(s(T23)), T12, s(T13)) → PB_IN_GAAA(T23, X31, T12, T13)
PB_IN_GAAA(T23, T24, T12, T13) → U3_GAAA(T23, T24, T12, T13, pC_in_ga(T23, T24))
PB_IN_GAAA(T23, T24, T12, T13) → PC_IN_GA(T23, T24)
PC_IN_GA(s(T27), s(X40)) → U2_GA(T27, X40, pC_in_ga(T27, X40))
PC_IN_GA(s(T27), s(X40)) → PC_IN_GA(T27, X40)
U3_GAAA(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_GAAA(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U3_GAAA(T23, T24, T12, T13, pC_out_ga(T23, T24)) → PLUSA_IN_GAA(s(s(T24)), T12, T13)
plusA_in_gaa(0, T5, T5) → plusA_out_gaa(0, T5, T5)
plusA_in_gaa(s(0), T20, s(T20)) → plusA_out_gaa(s(0), T20, s(T20))
plusA_in_gaa(s(s(T23)), T12, s(T13)) → U1_gaa(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
pB_in_gaaa(T23, T24, T12, T13) → U3_gaaa(T23, T24, T12, T13, pC_in_ga(T23, T24))
pC_in_ga(s(T27), s(X40)) → U2_ga(T27, X40, pC_in_ga(T27, X40))
U2_ga(T27, X40, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
U3_gaaa(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_gaaa(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U4_gaaa(T23, T24, T12, T13, plusA_out_gaa(s(s(T24)), T12, T13)) → pB_out_gaaa(T23, T24, T12, T13)
U1_gaa(T23, T12, T13, pB_out_gaaa(T23, X31, T12, T13)) → plusA_out_gaa(s(s(T23)), T12, s(T13))
PLUSA_IN_GAA(s(s(T23)), T12, s(T13)) → U1_GAA(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
PLUSA_IN_GAA(s(s(T23)), T12, s(T13)) → PB_IN_GAAA(T23, X31, T12, T13)
PB_IN_GAAA(T23, T24, T12, T13) → U3_GAAA(T23, T24, T12, T13, pC_in_ga(T23, T24))
PB_IN_GAAA(T23, T24, T12, T13) → PC_IN_GA(T23, T24)
PC_IN_GA(s(T27), s(X40)) → U2_GA(T27, X40, pC_in_ga(T27, X40))
PC_IN_GA(s(T27), s(X40)) → PC_IN_GA(T27, X40)
U3_GAAA(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_GAAA(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U3_GAAA(T23, T24, T12, T13, pC_out_ga(T23, T24)) → PLUSA_IN_GAA(s(s(T24)), T12, T13)
plusA_in_gaa(0, T5, T5) → plusA_out_gaa(0, T5, T5)
plusA_in_gaa(s(0), T20, s(T20)) → plusA_out_gaa(s(0), T20, s(T20))
plusA_in_gaa(s(s(T23)), T12, s(T13)) → U1_gaa(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
pB_in_gaaa(T23, T24, T12, T13) → U3_gaaa(T23, T24, T12, T13, pC_in_ga(T23, T24))
pC_in_ga(s(T27), s(X40)) → U2_ga(T27, X40, pC_in_ga(T27, X40))
U2_ga(T27, X40, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
U3_gaaa(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_gaaa(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U4_gaaa(T23, T24, T12, T13, plusA_out_gaa(s(s(T24)), T12, T13)) → pB_out_gaaa(T23, T24, T12, T13)
U1_gaa(T23, T12, T13, pB_out_gaaa(T23, X31, T12, T13)) → plusA_out_gaa(s(s(T23)), T12, s(T13))
PC_IN_GA(s(T27), s(X40)) → PC_IN_GA(T27, X40)
plusA_in_gaa(0, T5, T5) → plusA_out_gaa(0, T5, T5)
plusA_in_gaa(s(0), T20, s(T20)) → plusA_out_gaa(s(0), T20, s(T20))
plusA_in_gaa(s(s(T23)), T12, s(T13)) → U1_gaa(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
pB_in_gaaa(T23, T24, T12, T13) → U3_gaaa(T23, T24, T12, T13, pC_in_ga(T23, T24))
pC_in_ga(s(T27), s(X40)) → U2_ga(T27, X40, pC_in_ga(T27, X40))
U2_ga(T27, X40, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
U3_gaaa(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_gaaa(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U4_gaaa(T23, T24, T12, T13, plusA_out_gaa(s(s(T24)), T12, T13)) → pB_out_gaaa(T23, T24, T12, T13)
U1_gaa(T23, T12, T13, pB_out_gaaa(T23, X31, T12, T13)) → plusA_out_gaa(s(s(T23)), T12, s(T13))
PC_IN_GA(s(T27), s(X40)) → PC_IN_GA(T27, X40)
PC_IN_GA(s(T27)) → PC_IN_GA(T27)
From the DPs we obtained the following set of size-change graphs:
PLUSA_IN_GAA(s(s(T23)), T12, s(T13)) → PB_IN_GAAA(T23, X31, T12, T13)
PB_IN_GAAA(T23, T24, T12, T13) → U3_GAAA(T23, T24, T12, T13, pC_in_ga(T23, T24))
U3_GAAA(T23, T24, T12, T13, pC_out_ga(T23, T24)) → PLUSA_IN_GAA(s(s(T24)), T12, T13)
plusA_in_gaa(0, T5, T5) → plusA_out_gaa(0, T5, T5)
plusA_in_gaa(s(0), T20, s(T20)) → plusA_out_gaa(s(0), T20, s(T20))
plusA_in_gaa(s(s(T23)), T12, s(T13)) → U1_gaa(T23, T12, T13, pB_in_gaaa(T23, X31, T12, T13))
pB_in_gaaa(T23, T24, T12, T13) → U3_gaaa(T23, T24, T12, T13, pC_in_ga(T23, T24))
pC_in_ga(s(T27), s(X40)) → U2_ga(T27, X40, pC_in_ga(T27, X40))
U2_ga(T27, X40, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
U3_gaaa(T23, T24, T12, T13, pC_out_ga(T23, T24)) → U4_gaaa(T23, T24, T12, T13, plusA_in_gaa(s(s(T24)), T12, T13))
U4_gaaa(T23, T24, T12, T13, plusA_out_gaa(s(s(T24)), T12, T13)) → pB_out_gaaa(T23, T24, T12, T13)
U1_gaa(T23, T12, T13, pB_out_gaaa(T23, X31, T12, T13)) → plusA_out_gaa(s(s(T23)), T12, s(T13))
PLUSA_IN_GAA(s(s(T23)), T12, s(T13)) → PB_IN_GAAA(T23, X31, T12, T13)
PB_IN_GAAA(T23, T24, T12, T13) → U3_GAAA(T23, T24, T12, T13, pC_in_ga(T23, T24))
U3_GAAA(T23, T24, T12, T13, pC_out_ga(T23, T24)) → PLUSA_IN_GAA(s(s(T24)), T12, T13)
pC_in_ga(s(T27), s(X40)) → U2_ga(T27, X40, pC_in_ga(T27, X40))
U2_ga(T27, X40, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
PLUSA_IN_GAA(s(s(T23))) → PB_IN_GAAA(T23)
PB_IN_GAAA(T23) → U3_GAAA(T23, pC_in_ga(T23))
U3_GAAA(T23, pC_out_ga(T23, T24)) → PLUSA_IN_GAA(s(s(T24)))
pC_in_ga(s(T27)) → U2_ga(T27, pC_in_ga(T27))
U2_ga(T27, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
pC_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.
PB_IN_GAAA(T23) → U3_GAAA(T23, pC_in_ga(T23))
POL(PB_IN_GAAA(x1)) = 1
POL(PLUSA_IN_GAA(x1)) = x1
POL(U2_ga(x1, x2)) = x2
POL(U3_GAAA(x1, x2)) = x2
POL(pC_in_ga(x1)) = 0
POL(pC_out_ga(x1, x2)) = 1
POL(s(x1)) = 1
pC_in_ga(s(T27)) → U2_ga(T27, pC_in_ga(T27))
U2_ga(T27, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
PLUSA_IN_GAA(s(s(T23))) → PB_IN_GAAA(T23)
U3_GAAA(T23, pC_out_ga(T23, T24)) → PLUSA_IN_GAA(s(s(T24)))
pC_in_ga(s(T27)) → U2_ga(T27, pC_in_ga(T27))
U2_ga(T27, pC_out_ga(T27, X40)) → pC_out_ga(s(T27), s(X40))
pC_in_ga(x0)
U2_ga(x0, x1)