0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 148 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 59 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 27 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
transposeA_in_ga(.(T24, T25), .(T28, T29)) → U1_ga(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
pB_in_gaaaag(T24, T28, T29, T34, T35, T25) → U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
row2colD_in_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
row2colC_in_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
row2colC_in_gaaa([], [], [], []) → row2colC_out_gaaa([], [], [], [])
U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_out_gaaa(T82, T85, X139, X140)) → row2colC_out_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140))
U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_out_gaaa(T57, T60, X91, X92)) → row2colD_out_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92))
U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
transpose_auxE_in_gga(.(T115, T116), T117, .(T120, T121)) → U4_gga(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
U4_gga(T115, T116, T117, T120, T121, pB_out_gaaaag(T115, T120, T121, X185, X186, T116)) → transpose_auxE_out_gga(.(T115, T116), T117, .(T120, T121))
transpose_auxE_in_gga([], T128, T128) → transpose_auxE_out_gga([], T128, T128)
U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_out_gga(T25, T35, T34)) → pB_out_gaaaag(T24, T28, T29, T34, T35, T25)
U1_ga(T24, T25, T28, T29, pB_out_gaaaag(T24, T28, T29, X35, X36, T25)) → transposeA_out_ga(.(T24, T25), .(T28, T29))
transposeA_in_ga([], []) → transposeA_out_ga([], [])
TRANSPOSEA_IN_GA(.(T24, T25), .(T28, T29)) → U1_GA(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
TRANSPOSEA_IN_GA(.(T24, T25), .(T28, T29)) → PB_IN_GAAAAG(T24, T28, T29, X35, X36, T25)
PB_IN_GAAAAG(T24, T28, T29, T34, T35, T25) → U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
PB_IN_GAAAAG(T24, T28, T29, T34, T35, T25) → ROW2COLD_IN_GAAAA(T24, T28, T29, T34, T35)
ROW2COLD_IN_GAAAA(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_GAAAA(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
ROW2COLD_IN_GAAAA(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → ROW2COLC_IN_GAAA(T57, T60, X91, X92)
ROW2COLC_IN_GAAA(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_GAAA(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
ROW2COLC_IN_GAAA(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → ROW2COLC_IN_GAAA(T82, T85, X139, X140)
U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_GAAAAG(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → TRANSPOSE_AUXE_IN_GGA(T25, T35, T34)
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117, .(T120, T121)) → U4_GGA(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117, .(T120, T121)) → PB_IN_GAAAAG(T115, T120, T121, X185, X186, T116)
transposeA_in_ga(.(T24, T25), .(T28, T29)) → U1_ga(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
pB_in_gaaaag(T24, T28, T29, T34, T35, T25) → U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
row2colD_in_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
row2colC_in_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
row2colC_in_gaaa([], [], [], []) → row2colC_out_gaaa([], [], [], [])
U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_out_gaaa(T82, T85, X139, X140)) → row2colC_out_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140))
U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_out_gaaa(T57, T60, X91, X92)) → row2colD_out_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92))
U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
transpose_auxE_in_gga(.(T115, T116), T117, .(T120, T121)) → U4_gga(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
U4_gga(T115, T116, T117, T120, T121, pB_out_gaaaag(T115, T120, T121, X185, X186, T116)) → transpose_auxE_out_gga(.(T115, T116), T117, .(T120, T121))
transpose_auxE_in_gga([], T128, T128) → transpose_auxE_out_gga([], T128, T128)
U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_out_gga(T25, T35, T34)) → pB_out_gaaaag(T24, T28, T29, T34, T35, T25)
U1_ga(T24, T25, T28, T29, pB_out_gaaaag(T24, T28, T29, X35, X36, T25)) → transposeA_out_ga(.(T24, T25), .(T28, T29))
transposeA_in_ga([], []) → transposeA_out_ga([], [])
TRANSPOSEA_IN_GA(.(T24, T25), .(T28, T29)) → U1_GA(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
TRANSPOSEA_IN_GA(.(T24, T25), .(T28, T29)) → PB_IN_GAAAAG(T24, T28, T29, X35, X36, T25)
PB_IN_GAAAAG(T24, T28, T29, T34, T35, T25) → U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
PB_IN_GAAAAG(T24, T28, T29, T34, T35, T25) → ROW2COLD_IN_GAAAA(T24, T28, T29, T34, T35)
ROW2COLD_IN_GAAAA(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_GAAAA(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
ROW2COLD_IN_GAAAA(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → ROW2COLC_IN_GAAA(T57, T60, X91, X92)
ROW2COLC_IN_GAAA(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_GAAA(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
ROW2COLC_IN_GAAA(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → ROW2COLC_IN_GAAA(T82, T85, X139, X140)
U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_GAAAAG(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → TRANSPOSE_AUXE_IN_GGA(T25, T35, T34)
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117, .(T120, T121)) → U4_GGA(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117, .(T120, T121)) → PB_IN_GAAAAG(T115, T120, T121, X185, X186, T116)
transposeA_in_ga(.(T24, T25), .(T28, T29)) → U1_ga(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
pB_in_gaaaag(T24, T28, T29, T34, T35, T25) → U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
row2colD_in_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
row2colC_in_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
row2colC_in_gaaa([], [], [], []) → row2colC_out_gaaa([], [], [], [])
U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_out_gaaa(T82, T85, X139, X140)) → row2colC_out_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140))
U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_out_gaaa(T57, T60, X91, X92)) → row2colD_out_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92))
U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
transpose_auxE_in_gga(.(T115, T116), T117, .(T120, T121)) → U4_gga(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
U4_gga(T115, T116, T117, T120, T121, pB_out_gaaaag(T115, T120, T121, X185, X186, T116)) → transpose_auxE_out_gga(.(T115, T116), T117, .(T120, T121))
transpose_auxE_in_gga([], T128, T128) → transpose_auxE_out_gga([], T128, T128)
U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_out_gga(T25, T35, T34)) → pB_out_gaaaag(T24, T28, T29, T34, T35, T25)
U1_ga(T24, T25, T28, T29, pB_out_gaaaag(T24, T28, T29, X35, X36, T25)) → transposeA_out_ga(.(T24, T25), .(T28, T29))
transposeA_in_ga([], []) → transposeA_out_ga([], [])
ROW2COLC_IN_GAAA(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → ROW2COLC_IN_GAAA(T82, T85, X139, X140)
transposeA_in_ga(.(T24, T25), .(T28, T29)) → U1_ga(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
pB_in_gaaaag(T24, T28, T29, T34, T35, T25) → U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
row2colD_in_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
row2colC_in_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
row2colC_in_gaaa([], [], [], []) → row2colC_out_gaaa([], [], [], [])
U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_out_gaaa(T82, T85, X139, X140)) → row2colC_out_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140))
U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_out_gaaa(T57, T60, X91, X92)) → row2colD_out_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92))
U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
transpose_auxE_in_gga(.(T115, T116), T117, .(T120, T121)) → U4_gga(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
U4_gga(T115, T116, T117, T120, T121, pB_out_gaaaag(T115, T120, T121, X185, X186, T116)) → transpose_auxE_out_gga(.(T115, T116), T117, .(T120, T121))
transpose_auxE_in_gga([], T128, T128) → transpose_auxE_out_gga([], T128, T128)
U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_out_gga(T25, T35, T34)) → pB_out_gaaaag(T24, T28, T29, T34, T35, T25)
U1_ga(T24, T25, T28, T29, pB_out_gaaaag(T24, T28, T29, X35, X36, T25)) → transposeA_out_ga(.(T24, T25), .(T28, T29))
transposeA_in_ga([], []) → transposeA_out_ga([], [])
ROW2COLC_IN_GAAA(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → ROW2COLC_IN_GAAA(T82, T85, X139, X140)
ROW2COLC_IN_GAAA(.(T81, T82)) → ROW2COLC_IN_GAAA(T82)
From the DPs we obtained the following set of size-change graphs:
U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → TRANSPOSE_AUXE_IN_GGA(T25, T35, T34)
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117, .(T120, T121)) → PB_IN_GAAAAG(T115, T120, T121, X185, X186, T116)
PB_IN_GAAAAG(T24, T28, T29, T34, T35, T25) → U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
transposeA_in_ga(.(T24, T25), .(T28, T29)) → U1_ga(T24, T25, T28, T29, pB_in_gaaaag(T24, T28, T29, X35, X36, T25))
pB_in_gaaaag(T24, T28, T29, T34, T35, T25) → U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
row2colD_in_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
row2colC_in_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
row2colC_in_gaaa([], [], [], []) → row2colC_out_gaaa([], [], [], [])
U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_out_gaaa(T82, T85, X139, X140)) → row2colC_out_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140))
U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_out_gaaa(T57, T60, X91, X92)) → row2colD_out_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92))
U5_gaaaag(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_in_gga(T25, T35, T34))
transpose_auxE_in_gga(.(T115, T116), T117, .(T120, T121)) → U4_gga(T115, T116, T117, T120, T121, pB_in_gaaaag(T115, T120, T121, X185, X186, T116))
U4_gga(T115, T116, T117, T120, T121, pB_out_gaaaag(T115, T120, T121, X185, X186, T116)) → transpose_auxE_out_gga(.(T115, T116), T117, .(T120, T121))
transpose_auxE_in_gga([], T128, T128) → transpose_auxE_out_gga([], T128, T128)
U6_gaaaag(T24, T28, T29, T34, T35, T25, transpose_auxE_out_gga(T25, T35, T34)) → pB_out_gaaaag(T24, T28, T29, T34, T35, T25)
U1_ga(T24, T25, T28, T29, pB_out_gaaaag(T24, T28, T29, X35, X36, T25)) → transposeA_out_ga(.(T24, T25), .(T28, T29))
transposeA_in_ga([], []) → transposeA_out_ga([], [])
U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_out_gaaaa(T24, T28, T29, T34, T35)) → TRANSPOSE_AUXE_IN_GGA(T25, T35, T34)
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117, .(T120, T121)) → PB_IN_GAAAAG(T115, T120, T121, X185, X186, T116)
PB_IN_GAAAAG(T24, T28, T29, T34, T35, T25) → U5_GAAAAG(T24, T28, T29, T34, T35, T25, row2colD_in_gaaaa(T24, T28, T29, T34, T35))
row2colD_in_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92)) → U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_in_gaaa(T57, T60, X91, X92))
U3_gaaaa(T56, T57, T58, T60, X91, X92, row2colC_out_gaaa(T57, T60, X91, X92)) → row2colD_out_gaaaa(.(T56, T57), .(T56, T58), T60, .(T58, X91), .([], X92))
row2colC_in_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140)) → U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_in_gaaa(T82, T85, X139, X140))
row2colC_in_gaaa([], [], [], []) → row2colC_out_gaaa([], [], [], [])
U2_gaaa(T81, T82, T83, T85, X139, X140, row2colC_out_gaaa(T82, T85, X139, X140)) → row2colC_out_gaaa(.(T81, T82), .(.(T81, T83), T85), .(T83, X139), .([], X140))
U5_GAAAAG(T24, T25, row2colD_out_gaaaa(T24, T35)) → TRANSPOSE_AUXE_IN_GGA(T25, T35)
TRANSPOSE_AUXE_IN_GGA(.(T115, T116), T117) → PB_IN_GAAAAG(T115, T116)
PB_IN_GAAAAG(T24, T25) → U5_GAAAAG(T24, T25, row2colD_in_gaaaa(T24))
row2colD_in_gaaaa(.(T56, T57)) → U3_gaaaa(T56, T57, row2colC_in_gaaa(T57))
U3_gaaaa(T56, T57, row2colC_out_gaaa(T57, X92)) → row2colD_out_gaaaa(.(T56, T57), .([], X92))
row2colC_in_gaaa(.(T81, T82)) → U2_gaaa(T81, T82, row2colC_in_gaaa(T82))
row2colC_in_gaaa([]) → row2colC_out_gaaa([], [])
U2_gaaa(T81, T82, row2colC_out_gaaa(T82, X140)) → row2colC_out_gaaa(.(T81, T82), .([], X140))
row2colD_in_gaaaa(x0)
U3_gaaaa(x0, x1, x2)
row2colC_in_gaaa(x0)
U2_gaaa(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: