0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 165 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 41 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 14 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_gg(.(T23, T24), .(T25, T26)) → U1_gg(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
pB_in_gggaag(T23, T25, T26, T31, T32, T24) → U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
row2colC_in_ggaa([], [], [], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
transpose_auxE_in_ggg(.(T110, T111), T112, .(T113, T114)) → U4_ggg(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
U4_ggg(T110, T111, T112, T113, T114, pB_out_gggaag(T110, T113, T114, X185, X186, T111)) → transpose_auxE_out_ggg(.(T110, T111), T112, .(T113, T114))
transpose_auxE_in_ggg([], T121, T121) → transpose_auxE_out_ggg([], T121, T121)
U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_out_ggg(T24, T32, T31)) → pB_out_gggaag(T23, T25, T26, T31, T32, T24)
U1_gg(T23, T24, T25, T26, pB_out_gggaag(T23, T25, T26, X35, X36, T24)) → transposeA_out_gg(.(T23, T24), .(T25, T26))
transposeA_in_gg([], []) → transposeA_out_gg([], [])
TRANSPOSEA_IN_GG(.(T23, T24), .(T25, T26)) → U1_GG(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
TRANSPOSEA_IN_GG(.(T23, T24), .(T25, T26)) → PB_IN_GGGAAG(T23, T25, T26, X35, X36, T24)
PB_IN_GGGAAG(T23, T25, T26, T31, T32, T24) → U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
PB_IN_GGGAAG(T23, T25, T26, T31, T32, T24) → ROW2COLD_IN_GGGAA(T23, T25, T26, T31, T32)
ROW2COLD_IN_GGGAA(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_GGGAA(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
ROW2COLD_IN_GGGAA(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → ROW2COLC_IN_GGAA(T54, T56, X91, X92)
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_GGAA(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → ROW2COLC_IN_GGAA(T78, T80, X139, X140)
U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_GGGAAG(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → TRANSPOSE_AUXE_IN_GGG(T24, T32, T31)
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → U4_GGG(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → PB_IN_GGGAAG(T110, T113, T114, X185, X186, T111)
transposeA_in_gg(.(T23, T24), .(T25, T26)) → U1_gg(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
pB_in_gggaag(T23, T25, T26, T31, T32, T24) → U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
row2colC_in_ggaa([], [], [], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
transpose_auxE_in_ggg(.(T110, T111), T112, .(T113, T114)) → U4_ggg(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
U4_ggg(T110, T111, T112, T113, T114, pB_out_gggaag(T110, T113, T114, X185, X186, T111)) → transpose_auxE_out_ggg(.(T110, T111), T112, .(T113, T114))
transpose_auxE_in_ggg([], T121, T121) → transpose_auxE_out_ggg([], T121, T121)
U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_out_ggg(T24, T32, T31)) → pB_out_gggaag(T23, T25, T26, T31, T32, T24)
U1_gg(T23, T24, T25, T26, pB_out_gggaag(T23, T25, T26, X35, X36, T24)) → transposeA_out_gg(.(T23, T24), .(T25, T26))
transposeA_in_gg([], []) → transposeA_out_gg([], [])
TRANSPOSEA_IN_GG(.(T23, T24), .(T25, T26)) → U1_GG(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
TRANSPOSEA_IN_GG(.(T23, T24), .(T25, T26)) → PB_IN_GGGAAG(T23, T25, T26, X35, X36, T24)
PB_IN_GGGAAG(T23, T25, T26, T31, T32, T24) → U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
PB_IN_GGGAAG(T23, T25, T26, T31, T32, T24) → ROW2COLD_IN_GGGAA(T23, T25, T26, T31, T32)
ROW2COLD_IN_GGGAA(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_GGGAA(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
ROW2COLD_IN_GGGAA(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → ROW2COLC_IN_GGAA(T54, T56, X91, X92)
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_GGAA(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → ROW2COLC_IN_GGAA(T78, T80, X139, X140)
U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_GGGAAG(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → TRANSPOSE_AUXE_IN_GGG(T24, T32, T31)
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → U4_GGG(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → PB_IN_GGGAAG(T110, T113, T114, X185, X186, T111)
transposeA_in_gg(.(T23, T24), .(T25, T26)) → U1_gg(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
pB_in_gggaag(T23, T25, T26, T31, T32, T24) → U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
row2colC_in_ggaa([], [], [], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
transpose_auxE_in_ggg(.(T110, T111), T112, .(T113, T114)) → U4_ggg(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
U4_ggg(T110, T111, T112, T113, T114, pB_out_gggaag(T110, T113, T114, X185, X186, T111)) → transpose_auxE_out_ggg(.(T110, T111), T112, .(T113, T114))
transpose_auxE_in_ggg([], T121, T121) → transpose_auxE_out_ggg([], T121, T121)
U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_out_ggg(T24, T32, T31)) → pB_out_gggaag(T23, T25, T26, T31, T32, T24)
U1_gg(T23, T24, T25, T26, pB_out_gggaag(T23, T25, T26, X35, X36, T24)) → transposeA_out_gg(.(T23, T24), .(T25, T26))
transposeA_in_gg([], []) → transposeA_out_gg([], [])
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → ROW2COLC_IN_GGAA(T78, T80, X139, X140)
transposeA_in_gg(.(T23, T24), .(T25, T26)) → U1_gg(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
pB_in_gggaag(T23, T25, T26, T31, T32, T24) → U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
row2colC_in_ggaa([], [], [], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
transpose_auxE_in_ggg(.(T110, T111), T112, .(T113, T114)) → U4_ggg(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
U4_ggg(T110, T111, T112, T113, T114, pB_out_gggaag(T110, T113, T114, X185, X186, T111)) → transpose_auxE_out_ggg(.(T110, T111), T112, .(T113, T114))
transpose_auxE_in_ggg([], T121, T121) → transpose_auxE_out_ggg([], T121, T121)
U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_out_ggg(T24, T32, T31)) → pB_out_gggaag(T23, T25, T26, T31, T32, T24)
U1_gg(T23, T24, T25, T26, pB_out_gggaag(T23, T25, T26, X35, X36, T24)) → transposeA_out_gg(.(T23, T24), .(T25, T26))
transposeA_in_gg([], []) → transposeA_out_gg([], [])
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → ROW2COLC_IN_GGAA(T78, T80, X139, X140)
ROW2COLC_IN_GGAA(.(T77, T78), .(.(T77, T79), T80)) → ROW2COLC_IN_GGAA(T78, T80)
From the DPs we obtained the following set of size-change graphs:
U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → TRANSPOSE_AUXE_IN_GGG(T24, T32, T31)
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → PB_IN_GGGAAG(T110, T113, T114, X185, X186, T111)
PB_IN_GGGAAG(T23, T25, T26, T31, T32, T24) → U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
transposeA_in_gg(.(T23, T24), .(T25, T26)) → U1_gg(T23, T24, T25, T26, pB_in_gggaag(T23, T25, T26, X35, X36, T24))
pB_in_gggaag(T23, T25, T26, T31, T32, T24) → U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
row2colC_in_ggaa([], [], [], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
U5_gggaag(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_in_ggg(T24, T32, T31))
transpose_auxE_in_ggg(.(T110, T111), T112, .(T113, T114)) → U4_ggg(T110, T111, T112, T113, T114, pB_in_gggaag(T110, T113, T114, X185, X186, T111))
U4_ggg(T110, T111, T112, T113, T114, pB_out_gggaag(T110, T113, T114, X185, X186, T111)) → transpose_auxE_out_ggg(.(T110, T111), T112, .(T113, T114))
transpose_auxE_in_ggg([], T121, T121) → transpose_auxE_out_ggg([], T121, T121)
U6_gggaag(T23, T25, T26, T31, T32, T24, transpose_auxE_out_ggg(T24, T32, T31)) → pB_out_gggaag(T23, T25, T26, T31, T32, T24)
U1_gg(T23, T24, T25, T26, pB_out_gggaag(T23, T25, T26, X35, X36, T24)) → transposeA_out_gg(.(T23, T24), .(T25, T26))
transposeA_in_gg([], []) → transposeA_out_gg([], [])
U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → TRANSPOSE_AUXE_IN_GGG(T24, T32, T31)
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → PB_IN_GGGAAG(T110, T113, T114, X185, X186, T111)
PB_IN_GGGAAG(T23, T25, T26, T31, T32, T24) → U5_GGGAAG(T23, T25, T26, T31, T32, T24, row2colD_in_gggaa(T23, T25, T26, T31, T32))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92)) → U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_in_ggaa(T54, T56, X91, X92))
U3_gggaa(T53, T54, T55, T56, X91, X92, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140)) → U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_in_ggaa(T78, T80, X139, X140))
row2colC_in_ggaa([], [], [], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, X139, X140, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
U5_GGGAAG(T23, T25, T26, T24, row2colD_out_gggaa(T23, T25, T26, T31, T32)) → TRANSPOSE_AUXE_IN_GGG(T24, T32, T31)
TRANSPOSE_AUXE_IN_GGG(.(T110, T111), T112, .(T113, T114)) → PB_IN_GGGAAG(T110, T113, T114, T111)
PB_IN_GGGAAG(T23, T25, T26, T24) → U5_GGGAAG(T23, T25, T26, T24, row2colD_in_gggaa(T23, T25, T26))
row2colD_in_gggaa(.(T53, T54), .(T53, T55), T56) → U3_gggaa(T53, T54, T55, T56, row2colC_in_ggaa(T54, T56))
U3_gggaa(T53, T54, T55, T56, row2colC_out_ggaa(T54, T56, X91, X92)) → row2colD_out_gggaa(.(T53, T54), .(T53, T55), T56, .(T55, X91), .([], X92))
row2colC_in_ggaa(.(T77, T78), .(.(T77, T79), T80)) → U2_ggaa(T77, T78, T79, T80, row2colC_in_ggaa(T78, T80))
row2colC_in_ggaa([], []) → row2colC_out_ggaa([], [], [], [])
U2_ggaa(T77, T78, T79, T80, row2colC_out_ggaa(T78, T80, X139, X140)) → row2colC_out_ggaa(.(T77, T78), .(.(T77, T79), T80), .(T79, X139), .([], X140))
row2colD_in_gggaa(x0, x1, x2)
U3_gggaa(x0, x1, x2, x3, x4)
row2colC_in_ggaa(x0, x1)
U2_ggaa(x0, x1, x2, x3, x4)
From the DPs we obtained the following set of size-change graphs: