0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 123 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 24 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 12 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 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_aA_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appB_in_gga(T18, T11, 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(T18, T11, T13, appB_out_gga(T18, T11, T13)) → app3_aA_out_ggga([], T18, T11, T13)
app3_aA_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → app3_aA_out_ggga(.(T47, T48), T49, T11, T13)
APP3_AA_IN_GGGA([], T18, T11, T13) → U1_GGGA(T18, T11, T13, appB_in_gga(T18, T11, T13))
APP3_AA_IN_GGGA([], T18, T11, T13) → APPB_IN_GGA(T18, T11, 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_AA_IN_GGGA(.(T47, T48), T49, T11, T13) → U2_GGGA(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
APP3_AA_IN_GGGA(.(T47, T48), T49, T11, T13) → PC_IN_GGAGGA(T48, T49, X50, T47, T11, T13)
PC_IN_GGAGGA(T48, T49, T52, T47, T11, T13) → U5_GGAGGA(T48, T49, T52, T47, T11, T13, appD_in_gga(T48, T49, T52))
PC_IN_GGAGGA(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_GGAGGA(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U5_GGAGGA(T48, T49, T52, T47, T11, T13, appD_out_gga(T48, T49, T52)) → APPB_IN_GGA(.(T47, T52), T11, T13)
app3_aA_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appB_in_gga(T18, T11, 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(T18, T11, T13, appB_out_gga(T18, T11, T13)) → app3_aA_out_ggga([], T18, T11, T13)
app3_aA_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → app3_aA_out_ggga(.(T47, T48), T49, T11, T13)
APP3_AA_IN_GGGA([], T18, T11, T13) → U1_GGGA(T18, T11, T13, appB_in_gga(T18, T11, T13))
APP3_AA_IN_GGGA([], T18, T11, T13) → APPB_IN_GGA(T18, T11, 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_AA_IN_GGGA(.(T47, T48), T49, T11, T13) → U2_GGGA(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
APP3_AA_IN_GGGA(.(T47, T48), T49, T11, T13) → PC_IN_GGAGGA(T48, T49, X50, T47, T11, T13)
PC_IN_GGAGGA(T48, T49, T52, T47, T11, T13) → U5_GGAGGA(T48, T49, T52, T47, T11, T13, appD_in_gga(T48, T49, T52))
PC_IN_GGAGGA(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_GGAGGA(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U5_GGAGGA(T48, T49, T52, T47, T11, T13, appD_out_gga(T48, T49, T52)) → APPB_IN_GGA(.(T47, T52), T11, T13)
app3_aA_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appB_in_gga(T18, T11, 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(T18, T11, T13, appB_out_gga(T18, T11, T13)) → app3_aA_out_ggga([], T18, T11, T13)
app3_aA_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → app3_aA_out_ggga(.(T47, T48), T49, T11, T13)
APPD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPD_IN_GGA(T67, T68, X74)
app3_aA_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appB_in_gga(T18, T11, 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(T18, T11, T13, appB_out_gga(T18, T11, T13)) → app3_aA_out_ggga([], T18, T11, T13)
app3_aA_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → app3_aA_out_ggga(.(T47, T48), T49, T11, 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_aA_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appB_in_gga(T18, T11, 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(T18, T11, T13, appB_out_gga(T18, T11, T13)) → app3_aA_out_ggga([], T18, T11, T13)
app3_aA_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, 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, T47, T11, T13, appD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → app3_aA_out_ggga(.(T47, T48), T49, T11, 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: