0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 97 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 13 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 9 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 QDPOrderProof (⇔, 15 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 2 ms)
↳22 TRUE
perm1A_in_ga([], []) → perm1A_out_ga([], [])
perm1A_in_ga(.(T27, T28), .(T27, T29)) → U1_ga(T27, T28, T29, perm1A_in_ga(T28, T29))
perm1A_in_ga(.(T37, T38), .(T39, T40)) → U2_ga(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
pB_in_agaga(T39, T38, T45, T37, T46) → U4_agaga(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
selectC_in_aga(T59, .(T59, T60), T60) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(T70, .(T68, T69), .(T68, X78)) → U3_aga(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
U3_aga(T70, T68, T69, X78, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
U4_agaga(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_agaga(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U5_agaga(T39, T38, T45, T37, T46, perm1A_out_ga(.(T37, T45), T46)) → pB_out_agaga(T39, T38, T45, T37, T46)
U2_ga(T37, T38, T39, T40, pB_out_agaga(T39, T38, X45, T37, T40)) → perm1A_out_ga(.(T37, T38), .(T39, T40))
U1_ga(T27, T28, T29, perm1A_out_ga(T28, T29)) → perm1A_out_ga(.(T27, T28), .(T27, T29))
PERM1A_IN_GA(.(T27, T28), .(T27, T29)) → U1_GA(T27, T28, T29, perm1A_in_ga(T28, T29))
PERM1A_IN_GA(.(T27, T28), .(T27, T29)) → PERM1A_IN_GA(T28, T29)
PERM1A_IN_GA(.(T37, T38), .(T39, T40)) → U2_GA(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
PERM1A_IN_GA(.(T37, T38), .(T39, T40)) → PB_IN_AGAGA(T39, T38, X45, T37, T40)
PB_IN_AGAGA(T39, T38, T45, T37, T46) → U4_AGAGA(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
PB_IN_AGAGA(T39, T38, T45, T37, T46) → SELECTC_IN_AGA(T39, T38, T45)
SELECTC_IN_AGA(T70, .(T68, T69), .(T68, X78)) → U3_AGA(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
SELECTC_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTC_IN_AGA(T70, T69, X78)
U4_AGAGA(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_AGAGA(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U4_AGAGA(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → PERM1A_IN_GA(.(T37, T45), T46)
perm1A_in_ga([], []) → perm1A_out_ga([], [])
perm1A_in_ga(.(T27, T28), .(T27, T29)) → U1_ga(T27, T28, T29, perm1A_in_ga(T28, T29))
perm1A_in_ga(.(T37, T38), .(T39, T40)) → U2_ga(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
pB_in_agaga(T39, T38, T45, T37, T46) → U4_agaga(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
selectC_in_aga(T59, .(T59, T60), T60) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(T70, .(T68, T69), .(T68, X78)) → U3_aga(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
U3_aga(T70, T68, T69, X78, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
U4_agaga(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_agaga(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U5_agaga(T39, T38, T45, T37, T46, perm1A_out_ga(.(T37, T45), T46)) → pB_out_agaga(T39, T38, T45, T37, T46)
U2_ga(T37, T38, T39, T40, pB_out_agaga(T39, T38, X45, T37, T40)) → perm1A_out_ga(.(T37, T38), .(T39, T40))
U1_ga(T27, T28, T29, perm1A_out_ga(T28, T29)) → perm1A_out_ga(.(T27, T28), .(T27, T29))
PERM1A_IN_GA(.(T27, T28), .(T27, T29)) → U1_GA(T27, T28, T29, perm1A_in_ga(T28, T29))
PERM1A_IN_GA(.(T27, T28), .(T27, T29)) → PERM1A_IN_GA(T28, T29)
PERM1A_IN_GA(.(T37, T38), .(T39, T40)) → U2_GA(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
PERM1A_IN_GA(.(T37, T38), .(T39, T40)) → PB_IN_AGAGA(T39, T38, X45, T37, T40)
PB_IN_AGAGA(T39, T38, T45, T37, T46) → U4_AGAGA(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
PB_IN_AGAGA(T39, T38, T45, T37, T46) → SELECTC_IN_AGA(T39, T38, T45)
SELECTC_IN_AGA(T70, .(T68, T69), .(T68, X78)) → U3_AGA(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
SELECTC_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTC_IN_AGA(T70, T69, X78)
U4_AGAGA(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_AGAGA(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U4_AGAGA(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → PERM1A_IN_GA(.(T37, T45), T46)
perm1A_in_ga([], []) → perm1A_out_ga([], [])
perm1A_in_ga(.(T27, T28), .(T27, T29)) → U1_ga(T27, T28, T29, perm1A_in_ga(T28, T29))
perm1A_in_ga(.(T37, T38), .(T39, T40)) → U2_ga(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
pB_in_agaga(T39, T38, T45, T37, T46) → U4_agaga(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
selectC_in_aga(T59, .(T59, T60), T60) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(T70, .(T68, T69), .(T68, X78)) → U3_aga(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
U3_aga(T70, T68, T69, X78, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
U4_agaga(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_agaga(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U5_agaga(T39, T38, T45, T37, T46, perm1A_out_ga(.(T37, T45), T46)) → pB_out_agaga(T39, T38, T45, T37, T46)
U2_ga(T37, T38, T39, T40, pB_out_agaga(T39, T38, X45, T37, T40)) → perm1A_out_ga(.(T37, T38), .(T39, T40))
U1_ga(T27, T28, T29, perm1A_out_ga(T28, T29)) → perm1A_out_ga(.(T27, T28), .(T27, T29))
SELECTC_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTC_IN_AGA(T70, T69, X78)
perm1A_in_ga([], []) → perm1A_out_ga([], [])
perm1A_in_ga(.(T27, T28), .(T27, T29)) → U1_ga(T27, T28, T29, perm1A_in_ga(T28, T29))
perm1A_in_ga(.(T37, T38), .(T39, T40)) → U2_ga(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
pB_in_agaga(T39, T38, T45, T37, T46) → U4_agaga(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
selectC_in_aga(T59, .(T59, T60), T60) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(T70, .(T68, T69), .(T68, X78)) → U3_aga(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
U3_aga(T70, T68, T69, X78, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
U4_agaga(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_agaga(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U5_agaga(T39, T38, T45, T37, T46, perm1A_out_ga(.(T37, T45), T46)) → pB_out_agaga(T39, T38, T45, T37, T46)
U2_ga(T37, T38, T39, T40, pB_out_agaga(T39, T38, X45, T37, T40)) → perm1A_out_ga(.(T37, T38), .(T39, T40))
U1_ga(T27, T28, T29, perm1A_out_ga(T28, T29)) → perm1A_out_ga(.(T27, T28), .(T27, T29))
SELECTC_IN_AGA(T70, .(T68, T69), .(T68, X78)) → SELECTC_IN_AGA(T70, T69, X78)
SELECTC_IN_AGA(.(T68, T69)) → SELECTC_IN_AGA(T69)
From the DPs we obtained the following set of size-change graphs:
PERM1A_IN_GA(.(T37, T38), .(T39, T40)) → PB_IN_AGAGA(T39, T38, X45, T37, T40)
PB_IN_AGAGA(T39, T38, T45, T37, T46) → U4_AGAGA(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
U4_AGAGA(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → PERM1A_IN_GA(.(T37, T45), T46)
PERM1A_IN_GA(.(T27, T28), .(T27, T29)) → PERM1A_IN_GA(T28, T29)
perm1A_in_ga([], []) → perm1A_out_ga([], [])
perm1A_in_ga(.(T27, T28), .(T27, T29)) → U1_ga(T27, T28, T29, perm1A_in_ga(T28, T29))
perm1A_in_ga(.(T37, T38), .(T39, T40)) → U2_ga(T37, T38, T39, T40, pB_in_agaga(T39, T38, X45, T37, T40))
pB_in_agaga(T39, T38, T45, T37, T46) → U4_agaga(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
selectC_in_aga(T59, .(T59, T60), T60) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(T70, .(T68, T69), .(T68, X78)) → U3_aga(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
U3_aga(T70, T68, T69, X78, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
U4_agaga(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → U5_agaga(T39, T38, T45, T37, T46, perm1A_in_ga(.(T37, T45), T46))
U5_agaga(T39, T38, T45, T37, T46, perm1A_out_ga(.(T37, T45), T46)) → pB_out_agaga(T39, T38, T45, T37, T46)
U2_ga(T37, T38, T39, T40, pB_out_agaga(T39, T38, X45, T37, T40)) → perm1A_out_ga(.(T37, T38), .(T39, T40))
U1_ga(T27, T28, T29, perm1A_out_ga(T28, T29)) → perm1A_out_ga(.(T27, T28), .(T27, T29))
PERM1A_IN_GA(.(T37, T38), .(T39, T40)) → PB_IN_AGAGA(T39, T38, X45, T37, T40)
PB_IN_AGAGA(T39, T38, T45, T37, T46) → U4_AGAGA(T39, T38, T45, T37, T46, selectC_in_aga(T39, T38, T45))
U4_AGAGA(T39, T38, T45, T37, T46, selectC_out_aga(T39, T38, T45)) → PERM1A_IN_GA(.(T37, T45), T46)
PERM1A_IN_GA(.(T27, T28), .(T27, T29)) → PERM1A_IN_GA(T28, T29)
selectC_in_aga(T59, .(T59, T60), T60) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(T70, .(T68, T69), .(T68, X78)) → U3_aga(T70, T68, T69, X78, selectC_in_aga(T70, T69, X78))
U3_aga(T70, T68, T69, X78, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
PERM1A_IN_GA(.(T37, T38)) → PB_IN_AGAGA(T38, T37)
PB_IN_AGAGA(T38, T37) → U4_AGAGA(T38, T37, selectC_in_aga(T38))
U4_AGAGA(T38, T37, selectC_out_aga(T39, T38, T45)) → PERM1A_IN_GA(.(T37, T45))
PERM1A_IN_GA(.(T27, T28)) → PERM1A_IN_GA(T28)
selectC_in_aga(.(T59, T60)) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(.(T68, T69)) → U3_aga(T68, T69, selectC_in_aga(T69))
U3_aga(T68, T69, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
selectC_in_aga(x0)
U3_aga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PB_IN_AGAGA(T38, T37) → U4_AGAGA(T38, T37, selectC_in_aga(T38))
PERM1A_IN_GA(.(T27, T28)) → PERM1A_IN_GA(T28)
POL(.(x1, x2)) = 1 + x2
POL(PB_IN_AGAGA(x1, x2)) = 1 + x1
POL(PERM1A_IN_GA(x1)) = x1
POL(U3_aga(x1, x2, x3)) = 1 + x3
POL(U4_AGAGA(x1, x2, x3)) = x3
POL(selectC_in_aga(x1)) = x1
POL(selectC_out_aga(x1, x2, x3)) = 1 + x3
selectC_in_aga(.(T59, T60)) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(.(T68, T69)) → U3_aga(T68, T69, selectC_in_aga(T69))
U3_aga(T68, T69, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
PERM1A_IN_GA(.(T37, T38)) → PB_IN_AGAGA(T38, T37)
U4_AGAGA(T38, T37, selectC_out_aga(T39, T38, T45)) → PERM1A_IN_GA(.(T37, T45))
selectC_in_aga(.(T59, T60)) → selectC_out_aga(T59, .(T59, T60), T60)
selectC_in_aga(.(T68, T69)) → U3_aga(T68, T69, selectC_in_aga(T69))
U3_aga(T68, T69, selectC_out_aga(T70, T69, X78)) → selectC_out_aga(T70, .(T68, T69), .(T68, X78))
selectC_in_aga(x0)
U3_aga(x0, x1, x2)