0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 64 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 13 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 1 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 20 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
app3_bA_in_ggga(T9, [], T18, T13) → U1_ggga(T9, T18, T13, appB_in_gga(T9, T18, T13))
appB_in_gga([], T25, T25) → appB_out_gga([], T25, T25)
appB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appB_out_gga(T35, T36, T38)) → appB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T9, T18, T13, appB_out_gga(T9, T18, T13)) → app3_bA_out_ggga(T9, [], T18, T13)
app3_bA_in_ggga(T9, .(T47, T48), T49, T13) → U2_ggga(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
pC_in_ggagga(T48, T49, T52, T9, T47, T13) → U5_ggagga(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
appD_in_gga([], T59, T59) → appD_out_gga([], T59, T59)
appD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appD_out_gga(T67, T68, X74)) → appD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U6_ggagga(T48, T49, T52, T9, T47, T13, appB_out_gga(T9, .(T47, T52), T13)) → pC_out_ggagga(T48, T49, T52, T9, T47, T13)
U2_ggga(T9, T47, T48, T49, T13, pC_out_ggagga(T48, T49, X50, T9, T47, T13)) → app3_bA_out_ggga(T9, .(T47, T48), T49, T13)
APP3_BA_IN_GGGA(T9, [], T18, T13) → U1_GGGA(T9, T18, T13, appB_in_gga(T9, T18, T13))
APP3_BA_IN_GGGA(T9, [], T18, T13) → APPB_IN_GGA(T9, T18, T13)
APPB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U3_GGA(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
APPB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPB_IN_GGA(T35, T36, T38)
APP3_BA_IN_GGGA(T9, .(T47, T48), T49, T13) → U2_GGGA(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
APP3_BA_IN_GGGA(T9, .(T47, T48), T49, T13) → PC_IN_GGAGGA(T48, T49, X50, T9, T47, T13)
PC_IN_GGAGGA(T48, T49, T52, T9, T47, T13) → U5_GGAGGA(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
PC_IN_GGAGGA(T48, T49, T52, T9, T47, T13) → APPD_IN_GGA(T48, T49, T52)
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U4_GGA(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPD_IN_GGA(T67, T68, X74)
U5_GGAGGA(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_GGAGGA(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U5_GGAGGA(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → APPB_IN_GGA(T9, .(T47, T52), T13)
app3_bA_in_ggga(T9, [], T18, T13) → U1_ggga(T9, T18, T13, appB_in_gga(T9, T18, T13))
appB_in_gga([], T25, T25) → appB_out_gga([], T25, T25)
appB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appB_out_gga(T35, T36, T38)) → appB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T9, T18, T13, appB_out_gga(T9, T18, T13)) → app3_bA_out_ggga(T9, [], T18, T13)
app3_bA_in_ggga(T9, .(T47, T48), T49, T13) → U2_ggga(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
pC_in_ggagga(T48, T49, T52, T9, T47, T13) → U5_ggagga(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
appD_in_gga([], T59, T59) → appD_out_gga([], T59, T59)
appD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appD_out_gga(T67, T68, X74)) → appD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U6_ggagga(T48, T49, T52, T9, T47, T13, appB_out_gga(T9, .(T47, T52), T13)) → pC_out_ggagga(T48, T49, T52, T9, T47, T13)
U2_ggga(T9, T47, T48, T49, T13, pC_out_ggagga(T48, T49, X50, T9, T47, T13)) → app3_bA_out_ggga(T9, .(T47, T48), T49, T13)
APP3_BA_IN_GGGA(T9, [], T18, T13) → U1_GGGA(T9, T18, T13, appB_in_gga(T9, T18, T13))
APP3_BA_IN_GGGA(T9, [], T18, T13) → APPB_IN_GGA(T9, T18, T13)
APPB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U3_GGA(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
APPB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPB_IN_GGA(T35, T36, T38)
APP3_BA_IN_GGGA(T9, .(T47, T48), T49, T13) → U2_GGGA(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
APP3_BA_IN_GGGA(T9, .(T47, T48), T49, T13) → PC_IN_GGAGGA(T48, T49, X50, T9, T47, T13)
PC_IN_GGAGGA(T48, T49, T52, T9, T47, T13) → U5_GGAGGA(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
PC_IN_GGAGGA(T48, T49, T52, T9, T47, T13) → APPD_IN_GGA(T48, T49, T52)
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U4_GGA(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPD_IN_GGA(T67, T68, X74)
U5_GGAGGA(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_GGAGGA(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U5_GGAGGA(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → APPB_IN_GGA(T9, .(T47, T52), T13)
app3_bA_in_ggga(T9, [], T18, T13) → U1_ggga(T9, T18, T13, appB_in_gga(T9, T18, T13))
appB_in_gga([], T25, T25) → appB_out_gga([], T25, T25)
appB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appB_out_gga(T35, T36, T38)) → appB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T9, T18, T13, appB_out_gga(T9, T18, T13)) → app3_bA_out_ggga(T9, [], T18, T13)
app3_bA_in_ggga(T9, .(T47, T48), T49, T13) → U2_ggga(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
pC_in_ggagga(T48, T49, T52, T9, T47, T13) → U5_ggagga(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
appD_in_gga([], T59, T59) → appD_out_gga([], T59, T59)
appD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appD_out_gga(T67, T68, X74)) → appD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U6_ggagga(T48, T49, T52, T9, T47, T13, appB_out_gga(T9, .(T47, T52), T13)) → pC_out_ggagga(T48, T49, T52, T9, T47, T13)
U2_ggga(T9, T47, T48, T49, T13, pC_out_ggagga(T48, T49, X50, T9, T47, T13)) → app3_bA_out_ggga(T9, .(T47, T48), T49, T13)
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPD_IN_GGA(T67, T68, X74)
app3_bA_in_ggga(T9, [], T18, T13) → U1_ggga(T9, T18, T13, appB_in_gga(T9, T18, T13))
appB_in_gga([], T25, T25) → appB_out_gga([], T25, T25)
appB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appB_out_gga(T35, T36, T38)) → appB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T9, T18, T13, appB_out_gga(T9, T18, T13)) → app3_bA_out_ggga(T9, [], T18, T13)
app3_bA_in_ggga(T9, .(T47, T48), T49, T13) → U2_ggga(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
pC_in_ggagga(T48, T49, T52, T9, T47, T13) → U5_ggagga(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
appD_in_gga([], T59, T59) → appD_out_gga([], T59, T59)
appD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appD_out_gga(T67, T68, X74)) → appD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U6_ggagga(T48, T49, T52, T9, T47, T13, appB_out_gga(T9, .(T47, T52), T13)) → pC_out_ggagga(T48, T49, T52, T9, T47, T13)
U2_ggga(T9, T47, T48, T49, T13, pC_out_ggagga(T48, T49, X50, T9, T47, T13)) → app3_bA_out_ggga(T9, .(T47, T48), T49, T13)
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPD_IN_GGA(T67, T68, X74)
APPD_IN_GGA(.(T66, T67), T68) → APPD_IN_GGA(T67, T68)
From the DPs we obtained the following set of size-change graphs:
APPB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPB_IN_GGA(T35, T36, T38)
app3_bA_in_ggga(T9, [], T18, T13) → U1_ggga(T9, T18, T13, appB_in_gga(T9, T18, T13))
appB_in_gga([], T25, T25) → appB_out_gga([], T25, T25)
appB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appB_out_gga(T35, T36, T38)) → appB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T9, T18, T13, appB_out_gga(T9, T18, T13)) → app3_bA_out_ggga(T9, [], T18, T13)
app3_bA_in_ggga(T9, .(T47, T48), T49, T13) → U2_ggga(T9, T47, T48, T49, T13, pC_in_ggagga(T48, T49, X50, T9, T47, T13))
pC_in_ggagga(T48, T49, T52, T9, T47, T13) → U5_ggagga(T48, T49, T52, T9, T47, T13, appD_in_gga(T48, T49, T52))
appD_in_gga([], T59, T59) → appD_out_gga([], T59, T59)
appD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appD_out_gga(T67, T68, X74)) → appD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T9, T47, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T9, T47, T13, appB_in_gga(T9, .(T47, T52), T13))
U6_ggagga(T48, T49, T52, T9, T47, T13, appB_out_gga(T9, .(T47, T52), T13)) → pC_out_ggagga(T48, T49, T52, T9, T47, T13)
U2_ggga(T9, T47, T48, T49, T13, pC_out_ggagga(T48, T49, X50, T9, T47, T13)) → app3_bA_out_ggga(T9, .(T47, T48), T49, T13)
APPB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPB_IN_GGA(T35, T36, T38)
APPB_IN_GGA(.(T34, T35), T36) → APPB_IN_GGA(T35, T36)
From the DPs we obtained the following set of size-change graphs: