0 Prolog
↳1 PrologToPiTRSProof (⇐)
↳2 PiTRS
↳3 DependencyPairsProof (⇔)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔)
↳9 PiDP
↳10 PiDPToQDPProof (⇐)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 PiDP
↳15 UsableRulesProof (⇔)
↳16 PiDP
↳17 PiDPToQDPProof (⇐)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 PiDP
↳22 UsableRulesProof (⇔)
↳23 PiDP
↳24 PiDPToQDPProof (⇐)
↳25 QDP
↳26 NonTerminationProof (⇔)
↳27 FALSE
↳28 PiDP
↳29 UsableRulesProof (⇔)
↳30 PiDP
↳31 PiDPToQDPProof (⇐)
↳32 QDP
↳33 Narrowing (⇐)
↳34 QDP
↳35 Narrowing (⇐)
↳36 QDP
↳37 Instantiation (⇔)
↳38 QDP
↳39 DependencyGraphProof (⇔)
↳40 AND
↳41 QDP
↳42 UsableRulesProof (⇔)
↳43 QDP
↳44 QReductionProof (⇔)
↳45 QDP
↳46 NonTerminationProof (⇔)
↳47 FALSE
↳48 QDP
↳49 Instantiation (⇔)
↳50 QDP
↳51 NonTerminationProof (⇔)
↳52 FALSE
↳53 PrologToPiTRSProof (⇐)
↳54 PiTRS
↳55 DependencyPairsProof (⇔)
↳56 PiDP
↳57 DependencyGraphProof (⇔)
↳58 AND
↳59 PiDP
↳60 UsableRulesProof (⇔)
↳61 PiDP
↳62 PiDPToQDPProof (⇐)
↳63 QDP
↳64 QDPSizeChangeProof (⇔)
↳65 TRUE
↳66 PiDP
↳67 UsableRulesProof (⇔)
↳68 PiDP
↳69 PiDPToQDPProof (⇐)
↳70 QDP
↳71 QDPSizeChangeProof (⇔)
↳72 TRUE
↳73 PiDP
↳74 UsableRulesProof (⇔)
↳75 PiDP
↳76 PiDPToQDPProof (⇐)
↳77 QDP
↳78 NonTerminationProof (⇔)
↳79 FALSE
↳80 PiDP
↳81 UsableRulesProof (⇔)
↳82 PiDP
↳83 PiDPToQDPProof (⇐)
↳84 QDP
↳85 Narrowing (⇐)
↳86 QDP
↳87 Narrowing (⇐)
↳88 QDP
↳89 Instantiation (⇔)
↳90 QDP
↳91 DependencyGraphProof (⇔)
↳92 AND
↳93 QDP
↳94 UsableRulesProof (⇔)
↳95 QDP
↳96 QReductionProof (⇔)
↳97 QDP
↳98 NonTerminationProof (⇔)
↳99 FALSE
↳100 QDP
↳101 Instantiation (⇔)
↳102 QDP
↳103 NonTerminationProof (⇔)
↳104 FALSE
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_GAA(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → DELMIN_IN_AAA(Right, Y, Right1)
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_AAA(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U7_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_GAA(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → LESS_IN_AG(Y, X)
LESS_IN_AG(s(X), s(Y)) → U7_AG(X, Y, less_in_ag(X, Y))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_GAA(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_GAA(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → DELMIN_IN_AAA(Right, Y, Right1)
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_AAA(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U7_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_GAA(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → LESS_IN_AG(Y, X)
LESS_IN_AG(s(X), s(Y)) → U7_AG(X, Y, less_in_ag(X, Y))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_GAA(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
LESS_IN_AG(s(Y)) → LESS_IN_AG(Y)
From the DPs we obtained the following set of size-change graphs:
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X)) → LESS_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
DELMIN_IN_AAA → DELMIN_IN_AAA
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
DELETE_IN_GAA(X) → U2_GAA(X, less_in_ga(X))
U2_GAA(X, less_out_ga(X)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(X) → U4_GAA(X, less_in_ag(X))
U4_GAA(X, less_out_ag(Y, X)) → DELETE_IN_GAA(X)
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(x0, less_in_ga(x0)))
U2_GAA(X, less_out_ga(X)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(X) → U4_GAA(X, less_in_ag(X))
U4_GAA(X, less_out_ag(Y, X)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(x0, less_in_ga(x0)))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0, s(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(x0, less_in_ag(x0)))
U2_GAA(X, less_out_ga(X)) → DELETE_IN_GAA(X)
U4_GAA(X, less_out_ag(Y, X)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(x0, less_in_ga(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0, s(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(x0, less_in_ag(x0)))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
U2_GAA(0, less_out_ga(0)) → DELETE_IN_GAA(0)
U2_GAA(s(z0), less_out_ga(s(z0))) → DELETE_IN_GAA(s(z0))
U4_GAA(X, less_out_ag(Y, X)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(x0, less_in_ga(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0, s(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(x0, less_in_ag(x0)))
U2_GAA(0, less_out_ga(0)) → DELETE_IN_GAA(0)
U2_GAA(s(z0), less_out_ga(s(z0))) → DELETE_IN_GAA(s(z0))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
U2_GAA(0, less_out_ga(0)) → DELETE_IN_GAA(0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
U2_GAA(0, less_out_ga(0)) → DELETE_IN_GAA(0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
U2_GAA(0, less_out_ga(0)) → DELETE_IN_GAA(0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga(0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(x0, less_in_ga(x0)))
U2_GAA(s(z0), less_out_ga(s(z0))) → DELETE_IN_GAA(s(z0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0, s(x0)))
U4_GAA(X, less_out_ag(Y, X)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(x0, less_in_ag(x0)))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
U4_GAA(s(z0), less_out_ag(0, s(z0))) → DELETE_IN_GAA(s(z0))
U4_GAA(s(z0), less_out_ag(x1, s(z0))) → DELETE_IN_GAA(s(z0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(x0, less_in_ga(x0)))
U2_GAA(s(z0), less_out_ga(s(z0))) → DELETE_IN_GAA(s(z0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0, s(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(x0, less_in_ag(x0)))
U4_GAA(s(z0), less_out_ag(0, s(z0))) → DELETE_IN_GAA(s(z0))
U4_GAA(s(z0), less_out_ag(x1, s(z0))) → DELETE_IN_GAA(s(z0))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U7_ga(X, less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(Y)) → U7_ag(Y, less_in_ag(Y))
U7_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U7_ag(Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0, x1)
U7_ag(x0, x1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_GAA(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → DELMIN_IN_AAA(Right, Y, Right1)
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_AAA(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U7_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_GAA(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → LESS_IN_AG(Y, X)
LESS_IN_AG(s(X), s(Y)) → U7_AG(X, Y, less_in_ag(X, Y))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_GAA(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_GAA(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
DELETE_IN_GAA(X, tree(X, Left, Right), tree(Y, Left, Right1)) → DELMIN_IN_AAA(Right, Y, Right1)
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_AAA(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U7_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_GAA(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → LESS_IN_AG(Y, X)
LESS_IN_AG(s(X), s(Y)) → U7_AG(X, Y, less_in_ag(X, Y))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_GAA(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
LESS_IN_AG(s(X), s(Y)) → LESS_IN_AG(X, Y)
LESS_IN_AG(s(Y)) → LESS_IN_AG(Y)
From the DPs we obtained the following set of size-change graphs:
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X)) → LESS_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELMIN_IN_AAA(tree(X, Left, X1), Y, tree(X, Left1, X2)) → DELMIN_IN_AAA(Left, Y, Left1)
DELMIN_IN_AAA → DELMIN_IN_AAA
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
delete_in_gaa(X, tree(X, void, Right), Right) → delete_out_gaa(X, tree(X, void, Right), Right)
delete_in_gaa(X, tree(X, Left, void), Left) → delete_out_gaa(X, tree(X, Left, void), Left)
delete_in_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1)) → U1_gaa(X, Left, Right, Y, Right1, delmin_in_aaa(Right, Y, Right1))
delmin_in_aaa(tree(Y, void, Right), Y, Right) → delmin_out_aaa(tree(Y, void, Right), Y, Right)
delmin_in_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2)) → U6_aaa(X, Left, X1, Y, Left1, X2, delmin_in_aaa(Left, Y, Left1))
U6_aaa(X, Left, X1, Y, Left1, X2, delmin_out_aaa(Left, Y, Left1)) → delmin_out_aaa(tree(X, Left, X1), Y, tree(X, Left1, X2))
U1_gaa(X, Left, Right, Y, Right1, delmin_out_aaa(Right, Y, Right1)) → delete_out_gaa(X, tree(X, Left, Right), tree(Y, Left, Right1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_gaa(X, Y, Left, Right, Left1, less_in_ga(X, Y))
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U2_gaa(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → U3_gaa(X, Y, Left, Right, Left1, delete_in_gaa(X, Left, Left1))
delete_in_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_gaa(X, Y, Left, Right, Right1, less_in_ag(Y, X))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
U4_gaa(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → U5_gaa(X, Y, Left, Right, Right1, delete_in_gaa(X, Right, Right1))
U5_gaa(X, Y, Left, Right, Right1, delete_out_gaa(X, Right, Right1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left, Right1))
U3_gaa(X, Y, Left, Right, Left1, delete_out_gaa(X, Left, Left1)) → delete_out_gaa(X, tree(Y, Left, Right), tree(Y, Left1, Right))
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left1, Right)) → U2_GAA(X, Y, Left, Right, Left1, less_in_ga(X, Y))
U2_GAA(X, Y, Left, Right, Left1, less_out_ga(X, Y)) → DELETE_IN_GAA(X, Left, Left1)
DELETE_IN_GAA(X, tree(Y, Left, Right), tree(Y, Left, Right1)) → U4_GAA(X, Y, Left, Right, Right1, less_in_ag(Y, X))
U4_GAA(X, Y, Left, Right, Right1, less_out_ag(Y, X)) → DELETE_IN_GAA(X, Right, Right1)
less_in_ga(0, s(X3)) → less_out_ga(0, s(X3))
less_in_ga(s(X), s(Y)) → U7_ga(X, Y, less_in_ga(X, Y))
less_in_ag(0, s(X3)) → less_out_ag(0, s(X3))
less_in_ag(s(X), s(Y)) → U7_ag(X, Y, less_in_ag(X, Y))
U7_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U7_ag(X, Y, less_out_ag(X, Y)) → less_out_ag(s(X), s(Y))
DELETE_IN_GAA(X) → U2_GAA(X, less_in_ga(X))
U2_GAA(X, less_out_ga) → DELETE_IN_GAA(X)
DELETE_IN_GAA(X) → U4_GAA(X, less_in_ag(X))
U4_GAA(X, less_out_ag(Y)) → DELETE_IN_GAA(X)
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(less_in_ga(x0)))
U2_GAA(X, less_out_ga) → DELETE_IN_GAA(X)
DELETE_IN_GAA(X) → U4_GAA(X, less_in_ag(X))
U4_GAA(X, less_out_ag(Y)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(less_in_ga(x0)))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(less_in_ag(x0)))
U2_GAA(X, less_out_ga) → DELETE_IN_GAA(X)
U4_GAA(X, less_out_ag(Y)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(less_in_ga(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(less_in_ag(x0)))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
U2_GAA(0, less_out_ga) → DELETE_IN_GAA(0)
U2_GAA(s(z0), less_out_ga) → DELETE_IN_GAA(s(z0))
U4_GAA(X, less_out_ag(Y)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(less_in_ga(x0)))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(less_in_ag(x0)))
U2_GAA(0, less_out_ga) → DELETE_IN_GAA(0)
U2_GAA(s(z0), less_out_ga) → DELETE_IN_GAA(s(z0))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
U2_GAA(0, less_out_ga) → DELETE_IN_GAA(0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
U2_GAA(0, less_out_ga) → DELETE_IN_GAA(0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
U2_GAA(0, less_out_ga) → DELETE_IN_GAA(0)
DELETE_IN_GAA(0) → U2_GAA(0, less_out_ga)
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(less_in_ga(x0)))
U2_GAA(s(z0), less_out_ga) → DELETE_IN_GAA(s(z0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0))
U4_GAA(X, less_out_ag(Y)) → DELETE_IN_GAA(X)
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(less_in_ag(x0)))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)
U4_GAA(s(z0), less_out_ag(0)) → DELETE_IN_GAA(s(z0))
U4_GAA(s(z0), less_out_ag(x1)) → DELETE_IN_GAA(s(z0))
DELETE_IN_GAA(s(x0)) → U2_GAA(s(x0), U7_ga(less_in_ga(x0)))
U2_GAA(s(z0), less_out_ga) → DELETE_IN_GAA(s(z0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), less_out_ag(0))
DELETE_IN_GAA(s(x0)) → U4_GAA(s(x0), U7_ag(less_in_ag(x0)))
U4_GAA(s(z0), less_out_ag(0)) → DELETE_IN_GAA(s(z0))
U4_GAA(s(z0), less_out_ag(x1)) → DELETE_IN_GAA(s(z0))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U7_ga(less_in_ga(X))
less_in_ag(s(X3)) → less_out_ag(0)
less_in_ag(s(Y)) → U7_ag(less_in_ag(Y))
U7_ga(less_out_ga) → less_out_ga
U7_ag(less_out_ag(X)) → less_out_ag(s(X))
less_in_ga(x0)
less_in_ag(x0)
U7_ga(x0)
U7_ag(x0)