0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 64 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 52 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 8 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
preorderA_in_ga(T5, T7) → U1_ga(T5, T7, preorder_dlB_in_ga(T5, T7))
preorder_dlB_in_ga(nil, []) → preorder_dlB_out_ga(nil, [])
preorder_dlB_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
pC_in_gaag(T21, T25, T28, T23) → U4_gaag(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaag(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_gaag(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U5_gaag(T21, T25, T28, T23, preorder_dlB_out_ga(T23, T28)) → pC_out_gaag(T21, T25, T28, T23)
U2_ga(T21, T22, T23, T25, pC_out_gaag(T21, T25, X26, T23)) → preorder_dlB_out_ga(tree(T21, T22, T23), .(T22, T25))
U1_ga(T5, T7, preorder_dlB_out_ga(T5, T7)) → preorderA_out_ga(T5, T7)
PREORDERA_IN_GA(T5, T7) → U1_GA(T5, T7, preorder_dlB_in_ga(T5, T7))
PREORDERA_IN_GA(T5, T7) → PREORDER_DLB_IN_GA(T5, T7)
PREORDER_DLB_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
PREORDER_DLB_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PC_IN_GAAG(T21, T25, X26, T23)
PC_IN_GAAG(T21, T25, T28, T23) → U4_GAAG(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
PC_IN_GAAG(T21, T25, T28, T23) → PREORDER_DLD_IN_GAA(T21, T25, T28)
PREORDER_DLD_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U3_GAA(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
PREORDER_DLD_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PE_IN_GAAGA(T44, T48, X54, T46, X55)
PE_IN_GAAGA(T44, T48, T51, T46, X55) → U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
PE_IN_GAAGA(T44, T48, T51, T46, X55) → PREORDER_DLD_IN_GAA(T44, T48, T51)
U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → PREORDER_DLD_IN_GAA(T46, T51, X55)
U4_GAAG(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_GAAG(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U4_GAAG(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → PREORDER_DLB_IN_GA(T23, T28)
preorderA_in_ga(T5, T7) → U1_ga(T5, T7, preorder_dlB_in_ga(T5, T7))
preorder_dlB_in_ga(nil, []) → preorder_dlB_out_ga(nil, [])
preorder_dlB_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
pC_in_gaag(T21, T25, T28, T23) → U4_gaag(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaag(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_gaag(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U5_gaag(T21, T25, T28, T23, preorder_dlB_out_ga(T23, T28)) → pC_out_gaag(T21, T25, T28, T23)
U2_ga(T21, T22, T23, T25, pC_out_gaag(T21, T25, X26, T23)) → preorder_dlB_out_ga(tree(T21, T22, T23), .(T22, T25))
U1_ga(T5, T7, preorder_dlB_out_ga(T5, T7)) → preorderA_out_ga(T5, T7)
PREORDERA_IN_GA(T5, T7) → U1_GA(T5, T7, preorder_dlB_in_ga(T5, T7))
PREORDERA_IN_GA(T5, T7) → PREORDER_DLB_IN_GA(T5, T7)
PREORDER_DLB_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
PREORDER_DLB_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PC_IN_GAAG(T21, T25, X26, T23)
PC_IN_GAAG(T21, T25, T28, T23) → U4_GAAG(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
PC_IN_GAAG(T21, T25, T28, T23) → PREORDER_DLD_IN_GAA(T21, T25, T28)
PREORDER_DLD_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U3_GAA(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
PREORDER_DLD_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PE_IN_GAAGA(T44, T48, X54, T46, X55)
PE_IN_GAAGA(T44, T48, T51, T46, X55) → U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
PE_IN_GAAGA(T44, T48, T51, T46, X55) → PREORDER_DLD_IN_GAA(T44, T48, T51)
U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → PREORDER_DLD_IN_GAA(T46, T51, X55)
U4_GAAG(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_GAAG(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U4_GAAG(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → PREORDER_DLB_IN_GA(T23, T28)
preorderA_in_ga(T5, T7) → U1_ga(T5, T7, preorder_dlB_in_ga(T5, T7))
preorder_dlB_in_ga(nil, []) → preorder_dlB_out_ga(nil, [])
preorder_dlB_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
pC_in_gaag(T21, T25, T28, T23) → U4_gaag(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaag(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_gaag(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U5_gaag(T21, T25, T28, T23, preorder_dlB_out_ga(T23, T28)) → pC_out_gaag(T21, T25, T28, T23)
U2_ga(T21, T22, T23, T25, pC_out_gaag(T21, T25, X26, T23)) → preorder_dlB_out_ga(tree(T21, T22, T23), .(T22, T25))
U1_ga(T5, T7, preorder_dlB_out_ga(T5, T7)) → preorderA_out_ga(T5, T7)
PREORDER_DLD_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PE_IN_GAAGA(T44, T48, X54, T46, X55)
PE_IN_GAAGA(T44, T48, T51, T46, X55) → U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → PREORDER_DLD_IN_GAA(T46, T51, X55)
PE_IN_GAAGA(T44, T48, T51, T46, X55) → PREORDER_DLD_IN_GAA(T44, T48, T51)
preorderA_in_ga(T5, T7) → U1_ga(T5, T7, preorder_dlB_in_ga(T5, T7))
preorder_dlB_in_ga(nil, []) → preorder_dlB_out_ga(nil, [])
preorder_dlB_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
pC_in_gaag(T21, T25, T28, T23) → U4_gaag(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaag(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_gaag(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U5_gaag(T21, T25, T28, T23, preorder_dlB_out_ga(T23, T28)) → pC_out_gaag(T21, T25, T28, T23)
U2_ga(T21, T22, T23, T25, pC_out_gaag(T21, T25, X26, T23)) → preorder_dlB_out_ga(tree(T21, T22, T23), .(T22, T25))
U1_ga(T5, T7, preorder_dlB_out_ga(T5, T7)) → preorderA_out_ga(T5, T7)
PREORDER_DLD_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PE_IN_GAAGA(T44, T48, X54, T46, X55)
PE_IN_GAAGA(T44, T48, T51, T46, X55) → U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_GAAGA(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → PREORDER_DLD_IN_GAA(T46, T51, X55)
PE_IN_GAAGA(T44, T48, T51, T46, X55) → PREORDER_DLD_IN_GAA(T44, T48, T51)
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
PREORDER_DLD_IN_GAA(tree(T44, T45, T46)) → PE_IN_GAAGA(T44, T46)
PE_IN_GAAGA(T44, T46) → U6_GAAGA(T44, T46, preorder_dlD_in_gaa(T44))
U6_GAAGA(T44, T46, preorder_dlD_out_gaa(T44)) → PREORDER_DLD_IN_GAA(T46)
PE_IN_GAAGA(T44, T46) → PREORDER_DLD_IN_GAA(T44)
preorder_dlD_in_gaa(nil) → preorder_dlD_out_gaa(nil)
preorder_dlD_in_gaa(tree(T44, T45, T46)) → U3_gaa(T44, T45, T46, pE_in_gaaga(T44, T46))
U3_gaa(T44, T45, T46, pE_out_gaaga(T44, T46)) → preorder_dlD_out_gaa(tree(T44, T45, T46))
pE_in_gaaga(T44, T46) → U6_gaaga(T44, T46, preorder_dlD_in_gaa(T44))
U6_gaaga(T44, T46, preorder_dlD_out_gaa(T44)) → U7_gaaga(T44, T46, preorder_dlD_in_gaa(T46))
U7_gaaga(T44, T46, preorder_dlD_out_gaa(T46)) → pE_out_gaaga(T44, T46)
preorder_dlD_in_gaa(x0)
U3_gaa(x0, x1, x2, x3)
pE_in_gaaga(x0, x1)
U6_gaaga(x0, x1, x2)
U7_gaaga(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
PREORDER_DLB_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PC_IN_GAAG(T21, T25, X26, T23)
PC_IN_GAAG(T21, T25, T28, T23) → U4_GAAG(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
U4_GAAG(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → PREORDER_DLB_IN_GA(T23, T28)
preorderA_in_ga(T5, T7) → U1_ga(T5, T7, preorder_dlB_in_ga(T5, T7))
preorder_dlB_in_ga(nil, []) → preorder_dlB_out_ga(nil, [])
preorder_dlB_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, pC_in_gaag(T21, T25, X26, T23))
pC_in_gaag(T21, T25, T28, T23) → U4_gaag(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaag(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → U5_gaag(T21, T25, T28, T23, preorder_dlB_in_ga(T23, T28))
U5_gaag(T21, T25, T28, T23, preorder_dlB_out_ga(T23, T28)) → pC_out_gaag(T21, T25, T28, T23)
U2_ga(T21, T22, T23, T25, pC_out_gaag(T21, T25, X26, T23)) → preorder_dlB_out_ga(tree(T21, T22, T23), .(T22, T25))
U1_ga(T5, T7, preorder_dlB_out_ga(T5, T7)) → preorderA_out_ga(T5, T7)
PREORDER_DLB_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PC_IN_GAAG(T21, T25, X26, T23)
PC_IN_GAAG(T21, T25, T28, T23) → U4_GAAG(T21, T25, T28, T23, preorder_dlD_in_gaa(T21, T25, T28))
U4_GAAG(T21, T25, T28, T23, preorder_dlD_out_gaa(T21, T25, T28)) → PREORDER_DLB_IN_GA(T23, T28)
preorder_dlD_in_gaa(nil, T35, T35) → preorder_dlD_out_gaa(nil, T35, T35)
preorder_dlD_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U3_gaa(T44, T45, T46, T48, X55, pE_in_gaaga(T44, T48, X54, T46, X55))
U3_gaa(T44, T45, T46, T48, X55, pE_out_gaaga(T44, T48, X54, T46, X55)) → preorder_dlD_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
pE_in_gaaga(T44, T48, T51, T46, X55) → U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T44, T48, T51))
U6_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T44, T48, T51)) → U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_in_gaa(T46, T51, X55))
U7_gaaga(T44, T48, T51, T46, X55, preorder_dlD_out_gaa(T46, T51, X55)) → pE_out_gaaga(T44, T48, T51, T46, X55)
PREORDER_DLB_IN_GA(tree(T21, T22, T23)) → PC_IN_GAAG(T21, T23)
PC_IN_GAAG(T21, T23) → U4_GAAG(T21, T23, preorder_dlD_in_gaa(T21))
U4_GAAG(T21, T23, preorder_dlD_out_gaa(T21)) → PREORDER_DLB_IN_GA(T23)
preorder_dlD_in_gaa(nil) → preorder_dlD_out_gaa(nil)
preorder_dlD_in_gaa(tree(T44, T45, T46)) → U3_gaa(T44, T45, T46, pE_in_gaaga(T44, T46))
U3_gaa(T44, T45, T46, pE_out_gaaga(T44, T46)) → preorder_dlD_out_gaa(tree(T44, T45, T46))
pE_in_gaaga(T44, T46) → U6_gaaga(T44, T46, preorder_dlD_in_gaa(T44))
U6_gaaga(T44, T46, preorder_dlD_out_gaa(T44)) → U7_gaaga(T44, T46, preorder_dlD_in_gaa(T46))
U7_gaaga(T44, T46, preorder_dlD_out_gaa(T46)) → pE_out_gaaga(T44, T46)
preorder_dlD_in_gaa(x0)
U3_gaa(x0, x1, x2, x3)
pE_in_gaaga(x0, x1)
U6_gaaga(x0, x1, x2)
U7_gaaga(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: