0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇐)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔)
↳18 PiDP
↳19 PiDPToQDPProof (⇐)
↳20 QDP
↳21 QDPSizeChangeProof (⇔)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔)
↳25 PiDP
↳26 PiDPToQDPProof (⇐)
↳27 QDP
↳28 Rewriting (⇔)
↳29 QDP
↳30 UsableRulesProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 NonTerminationProof (⇔)
↳35 NO
↳36 PiDP
↳37 UsableRulesProof (⇔)
↳38 PiDP
↳39 PiDPToQDPProof (⇐)
↳40 QDP
↳41 Narrowing (⇐)
↳42 QDP
↳43 Narrowing (⇐)
↳44 QDP
↳45 Narrowing (⇐)
↳46 QDP
↳47 Instantiation (⇔)
↳48 QDP
↳49 Instantiation (⇔)
↳50 QDP
↳51 Instantiation (⇔)
↳52 QDP
↳53 Instantiation (⇔)
↳54 QDP
↳55 ForwardInstantiation (⇔)
↳56 QDP
↳57 ForwardInstantiation (⇔)
↳58 QDP
↳59 ForwardInstantiation (⇔)
↳60 QDP
↳61 NonTerminationProof (⇔)
↳62 NO
↳63 PrologToPiTRSProof (⇐)
↳64 PiTRS
↳65 DependencyPairsProof (⇔)
↳66 PiDP
↳67 DependencyGraphProof (⇔)
↳68 AND
↳69 PiDP
↳70 UsableRulesProof (⇔)
↳71 PiDP
↳72 PiDPToQDPProof (⇐)
↳73 QDP
↳74 QDPSizeChangeProof (⇔)
↳75 YES
↳76 PiDP
↳77 UsableRulesProof (⇔)
↳78 PiDP
↳79 PiDPToQDPProof (⇐)
↳80 QDP
↳81 QDPSizeChangeProof (⇔)
↳82 YES
↳83 PiDP
↳84 UsableRulesProof (⇔)
↳85 PiDP
↳86 PiDPToQDPProof (⇐)
↳87 QDP
↳88 Rewriting (⇔)
↳89 QDP
↳90 UsableRulesProof (⇔)
↳91 QDP
↳92 QReductionProof (⇔)
↳93 QDP
↳94 NonTerminationProof (⇔)
↳95 NO
↳96 PiDP
↳97 UsableRulesProof (⇔)
↳98 PiDP
↳99 PiDPToQDPProof (⇐)
↳100 QDP
↳101 Narrowing (⇐)
↳102 QDP
↳103 Narrowing (⇐)
↳104 QDP
↳105 Narrowing (⇐)
↳106 QDP
↳107 Instantiation (⇔)
↳108 QDP
↳109 Instantiation (⇔)
↳110 QDP
↳111 Instantiation (⇔)
↳112 QDP
↳113 Instantiation (⇔)
↳114 QDP
↳115 ForwardInstantiation (⇔)
↳116 QDP
↳117 ForwardInstantiation (⇔)
↳118 QDP
↳119 ForwardInstantiation (⇔)
↳120 QDP
↳121 NonTerminationProof (⇔)
↳122 NO
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → U14_GA(T23, T24, T16, in11_in_a(T24))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → IN11_IN_A(T24)
IN11_IN_A(tree(T54, T55, T53)) → U1_A(T54, T55, T53, less23_in_a(T54))
IN11_IN_A(tree(T54, T55, T53)) → LESS23_IN_A(T54)
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → U3_A(T54, T58, T53, in11_in_a(T58))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → U15_GA(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T100) → U6_GAA(T97, T99, T100, less43_in_ga(T97, T99))
P41_IN_GAA(T97, T99, T100) → LESS43_IN_GA(T97, T99)
LESS43_IN_GA(s(T115), s(T117)) → U4_GA(T115, T117, less43_in_ga(T115, T117))
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → U8_GAA(T97, T99, T103, in1_in_ga(s(T97), T103))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T139)) → U16_GA(T134, T138, T136, T139, less56_in_ag(T138, T134))
IN1_IN_GA(T134, tree(T138, T136, T139)) → LESS56_IN_AG(T138, T134)
LESS56_IN_AG(s(T156), s(T155)) → U5_AG(T156, T155, less56_in_ag(T156, T155))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_GA(T134, T138, T136, T142, in1_in_ga(T134, T142))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → U19_GA(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → U9_AGA(T179, T180, in1_in_ga(s(T179), T180))
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(0, tree(s(T220), T221, T213)) → U20_GA(T220, T221, T213, in11_in_a(T221))
IN1_IN_GA(s(T234), tree(s(T236), T237, T213)) → U21_GA(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
IN1_IN_GA(T248, tree(T252, T250, T253)) → U22_GA(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
P66_IN_AGA(s(T193), s(T192), T194) → U10_AGA(T193, T192, T194, p73_in_aga(T193, T192, T194))
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
P73_IN_AGA(T193, T192, T194) → U11_AGA(T193, T192, T194, less56_in_ag(T193, T192))
P73_IN_AGA(T193, T192, T194) → LESS56_IN_AG(T193, T192)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → U13_AGA(T193, T192, T197, in1_in_ga(s(T192), T197))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → U23_GA(T270, T262, T271, in1_in_ga(s(T270), T271))
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → U24_GA(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → U14_GA(T23, T24, T16, in11_in_a(T24))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → IN11_IN_A(T24)
IN11_IN_A(tree(T54, T55, T53)) → U1_A(T54, T55, T53, less23_in_a(T54))
IN11_IN_A(tree(T54, T55, T53)) → LESS23_IN_A(T54)
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → U3_A(T54, T58, T53, in11_in_a(T58))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → U15_GA(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T100) → U6_GAA(T97, T99, T100, less43_in_ga(T97, T99))
P41_IN_GAA(T97, T99, T100) → LESS43_IN_GA(T97, T99)
LESS43_IN_GA(s(T115), s(T117)) → U4_GA(T115, T117, less43_in_ga(T115, T117))
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → U8_GAA(T97, T99, T103, in1_in_ga(s(T97), T103))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T139)) → U16_GA(T134, T138, T136, T139, less56_in_ag(T138, T134))
IN1_IN_GA(T134, tree(T138, T136, T139)) → LESS56_IN_AG(T138, T134)
LESS56_IN_AG(s(T156), s(T155)) → U5_AG(T156, T155, less56_in_ag(T156, T155))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_GA(T134, T138, T136, T142, in1_in_ga(T134, T142))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → U19_GA(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → U9_AGA(T179, T180, in1_in_ga(s(T179), T180))
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(0, tree(s(T220), T221, T213)) → U20_GA(T220, T221, T213, in11_in_a(T221))
IN1_IN_GA(s(T234), tree(s(T236), T237, T213)) → U21_GA(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
IN1_IN_GA(T248, tree(T252, T250, T253)) → U22_GA(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
P66_IN_AGA(s(T193), s(T192), T194) → U10_AGA(T193, T192, T194, p73_in_aga(T193, T192, T194))
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
P73_IN_AGA(T193, T192, T194) → U11_AGA(T193, T192, T194, less56_in_ag(T193, T192))
P73_IN_AGA(T193, T192, T194) → LESS56_IN_AG(T193, T192)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → U13_AGA(T193, T192, T197, in1_in_ga(s(T192), T197))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → U23_GA(T270, T262, T271, in1_in_ga(s(T270), T271))
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → U24_GA(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
LESS56_IN_AG(s(T155)) → LESS56_IN_AG(T155)
From the DPs we obtained the following set of size-change graphs:
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
LESS43_IN_GA(s(T115)) → LESS43_IN_GA(T115)
From the DPs we obtained the following set of size-change graphs:
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
less23_in_a(s(T65)) → less23_out_a(s(T65))
IN11_IN_A → U2_A(less23_in_a)
U2_A(less23_out_a) → IN11_IN_A
less23_in_a → less23_out_a
less23_in_a
IN11_IN_A → U2_A(less23_out_a)
U2_A(less23_out_a) → IN11_IN_A
IN11_IN_A → U2_A(less23_out_a)
less23_in_a → less23_out_a
less23_in_a
U2_A(less23_out_a) → IN11_IN_A
IN11_IN_A → U2_A(less23_out_a)
less23_in_a
less23_in_a
U2_A(less23_out_a) → IN11_IN_A
IN11_IN_A → U2_A(less23_out_a)
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
P41_IN_GAA(T97) → U7_GAA(T97, less43_in_ga(T97))
U7_GAA(T97, less43_out_ga(T97)) → IN1_IN_GA(s(T97))
IN1_IN_GA(T134) → U17_GA(T134, less56_in_ag(T134))
U17_GA(T134, less56_out_ag(T138, T134)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P73_IN_AGA(T192) → U12_AGA(T192, less56_in_ag(T192))
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U7_GAA(T97, less43_out_ga(T97)) → IN1_IN_GA(s(T97))
IN1_IN_GA(T134) → U17_GA(T134, less56_in_ag(T134))
U17_GA(T134, less56_out_ag(T138, T134)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P73_IN_AGA(T192) → U12_AGA(T192, less56_in_ag(T192))
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U7_GAA(T97, less43_out_ga(T97)) → IN1_IN_GA(s(T97))
U17_GA(T134, less56_out_ag(T138, T134)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P73_IN_AGA(T192) → U12_AGA(T192, less56_in_ag(T192))
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U7_GAA(T97, less43_out_ga(T97)) → IN1_IN_GA(s(T97))
U17_GA(T134, less56_out_ag(T138, T134)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U17_GA(T134, less56_out_ag(T138, T134)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
U12_AGA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(s(z0)))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
IN1_IN_GA(s(s(y_0))) → P73_IN_AGA(s(y_0))
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
IN1_IN_GA(s(s(y_0))) → P73_IN_AGA(s(y_0))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
P66_IN_AGA(s(s(y_0))) → P73_IN_AGA(s(y_0))
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga(0))
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(x0, less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0, s(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(x0, less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0, s(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(x0, less56_in_ag(x0)))
U7_GAA(0, less43_out_ga(0)) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga(s(z0))) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0, s(z0))) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1, s(z0))) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
IN1_IN_GA(s(s(y_0))) → P73_IN_AGA(s(y_0))
P66_IN_AGA(s(s(y_0))) → P73_IN_AGA(s(y_0))
less43_in_ga(0) → less43_out_ga(0)
less43_in_ga(s(T115)) → U4_ga(T115, less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T155)) → U5_ag(T155, less56_in_ag(T155))
U4_ga(T115, less43_out_ga(T115)) → less43_out_ga(s(T115))
U5_ag(T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0, x1)
U5_ag(x0, x1)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → U14_GA(T23, T24, T16, in11_in_a(T24))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → IN11_IN_A(T24)
IN11_IN_A(tree(T54, T55, T53)) → U1_A(T54, T55, T53, less23_in_a(T54))
IN11_IN_A(tree(T54, T55, T53)) → LESS23_IN_A(T54)
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → U3_A(T54, T58, T53, in11_in_a(T58))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → U15_GA(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T100) → U6_GAA(T97, T99, T100, less43_in_ga(T97, T99))
P41_IN_GAA(T97, T99, T100) → LESS43_IN_GA(T97, T99)
LESS43_IN_GA(s(T115), s(T117)) → U4_GA(T115, T117, less43_in_ga(T115, T117))
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → U8_GAA(T97, T99, T103, in1_in_ga(s(T97), T103))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T139)) → U16_GA(T134, T138, T136, T139, less56_in_ag(T138, T134))
IN1_IN_GA(T134, tree(T138, T136, T139)) → LESS56_IN_AG(T138, T134)
LESS56_IN_AG(s(T156), s(T155)) → U5_AG(T156, T155, less56_in_ag(T156, T155))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_GA(T134, T138, T136, T142, in1_in_ga(T134, T142))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → U19_GA(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → U9_AGA(T179, T180, in1_in_ga(s(T179), T180))
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(0, tree(s(T220), T221, T213)) → U20_GA(T220, T221, T213, in11_in_a(T221))
IN1_IN_GA(s(T234), tree(s(T236), T237, T213)) → U21_GA(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
IN1_IN_GA(T248, tree(T252, T250, T253)) → U22_GA(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
P66_IN_AGA(s(T193), s(T192), T194) → U10_AGA(T193, T192, T194, p73_in_aga(T193, T192, T194))
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
P73_IN_AGA(T193, T192, T194) → U11_AGA(T193, T192, T194, less56_in_ag(T193, T192))
P73_IN_AGA(T193, T192, T194) → LESS56_IN_AG(T193, T192)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → U13_AGA(T193, T192, T197, in1_in_ga(s(T192), T197))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → U23_GA(T270, T262, T271, in1_in_ga(s(T270), T271))
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → U24_GA(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → U14_GA(T23, T24, T16, in11_in_a(T24))
IN1_IN_GA(0, tree(s(T23), T24, T16)) → IN11_IN_A(T24)
IN11_IN_A(tree(T54, T55, T53)) → U1_A(T54, T55, T53, less23_in_a(T54))
IN11_IN_A(tree(T54, T55, T53)) → LESS23_IN_A(T54)
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → U3_A(T54, T58, T53, in11_in_a(T58))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → U15_GA(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T100) → U6_GAA(T97, T99, T100, less43_in_ga(T97, T99))
P41_IN_GAA(T97, T99, T100) → LESS43_IN_GA(T97, T99)
LESS43_IN_GA(s(T115), s(T117)) → U4_GA(T115, T117, less43_in_ga(T115, T117))
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → U8_GAA(T97, T99, T103, in1_in_ga(s(T97), T103))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T139)) → U16_GA(T134, T138, T136, T139, less56_in_ag(T138, T134))
IN1_IN_GA(T134, tree(T138, T136, T139)) → LESS56_IN_AG(T138, T134)
LESS56_IN_AG(s(T156), s(T155)) → U5_AG(T156, T155, less56_in_ag(T156, T155))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_GA(T134, T138, T136, T142, in1_in_ga(T134, T142))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → U19_GA(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → U9_AGA(T179, T180, in1_in_ga(s(T179), T180))
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(0, tree(s(T220), T221, T213)) → U20_GA(T220, T221, T213, in11_in_a(T221))
IN1_IN_GA(s(T234), tree(s(T236), T237, T213)) → U21_GA(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
IN1_IN_GA(T248, tree(T252, T250, T253)) → U22_GA(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
P66_IN_AGA(s(T193), s(T192), T194) → U10_AGA(T193, T192, T194, p73_in_aga(T193, T192, T194))
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
P73_IN_AGA(T193, T192, T194) → U11_AGA(T193, T192, T194, less56_in_ag(T193, T192))
P73_IN_AGA(T193, T192, T194) → LESS56_IN_AG(T193, T192)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → U13_AGA(T193, T192, T197, in1_in_ga(s(T192), T197))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → U23_GA(T270, T262, T271, in1_in_ga(s(T270), T271))
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → U24_GA(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
LESS56_IN_AG(s(T156), s(T155)) → LESS56_IN_AG(T156, T155)
LESS56_IN_AG(s(T155)) → LESS56_IN_AG(T155)
From the DPs we obtained the following set of size-change graphs:
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
LESS43_IN_GA(s(T115), s(T117)) → LESS43_IN_GA(T115, T117)
LESS43_IN_GA(s(T115)) → LESS43_IN_GA(T115)
From the DPs we obtained the following set of size-change graphs:
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN11_IN_A(tree(T54, T58, T53)) → U2_A(T54, T58, T53, less23_in_a(T54))
U2_A(T54, T58, T53, less23_out_a(T54)) → IN11_IN_A(T58)
less23_in_a(s(T65)) → less23_out_a(s(T65))
IN11_IN_A → U2_A(less23_in_a)
U2_A(less23_out_a) → IN11_IN_A
less23_in_a → less23_out_a
less23_in_a
IN11_IN_A → U2_A(less23_out_a)
U2_A(less23_out_a) → IN11_IN_A
IN11_IN_A → U2_A(less23_out_a)
less23_in_a → less23_out_a
less23_in_a
U2_A(less23_out_a) → IN11_IN_A
IN11_IN_A → U2_A(less23_out_a)
less23_in_a
less23_in_a
U2_A(less23_out_a) → IN11_IN_A
IN11_IN_A → U2_A(less23_out_a)
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
in1_in_ga(T6, tree(T6, T7, T8)) → in1_out_ga(T6, tree(T6, T7, T8))
in1_in_ga(0, tree(s(T23), T24, T16)) → U14_ga(T23, T24, T16, in11_in_a(T24))
in11_in_a(tree(0, T37, T38)) → in11_out_a(tree(0, T37, T38))
in11_in_a(tree(T54, T55, T53)) → U1_a(T54, T55, T53, less23_in_a(T54))
less23_in_a(s(T65)) → less23_out_a(s(T65))
U1_a(T54, T55, T53, less23_out_a(T54)) → in11_out_a(tree(T54, T55, T53))
in11_in_a(tree(T54, T58, T53)) → U2_a(T54, T58, T53, less23_in_a(T54))
U2_a(T54, T58, T53, less23_out_a(T54)) → U3_a(T54, T58, T53, in11_in_a(T58))
U3_a(T54, T58, T53, in11_out_a(T58)) → in11_out_a(tree(T54, T58, T53))
U14_ga(T23, T24, T16, in11_out_a(T24)) → in1_out_ga(0, tree(s(T23), T24, T16))
in1_in_ga(s(T97), tree(s(T99), T100, T16)) → U15_ga(T97, T99, T100, T16, p41_in_gaa(T97, T99, T100))
p41_in_gaa(T97, T99, T100) → U6_gaa(T97, T99, T100, less43_in_ga(T97, T99))
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U6_gaa(T97, T99, T100, less43_out_ga(T97, T99)) → p41_out_gaa(T97, T99, T100)
p41_in_gaa(T97, T99, T103) → U7_gaa(T97, T99, T103, less43_in_ga(T97, T99))
U7_gaa(T97, T99, T103, less43_out_ga(T97, T99)) → U8_gaa(T97, T99, T103, in1_in_ga(s(T97), T103))
in1_in_ga(T134, tree(T138, T136, T139)) → U16_ga(T134, T138, T136, T139, less56_in_ag(T138, T134))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
U16_ga(T134, T138, T136, T139, less56_out_ag(T138, T134)) → in1_out_ga(T134, tree(T138, T136, T139))
in1_in_ga(T134, tree(T138, T136, T142)) → U17_ga(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_ga(T134, T138, T136, T142, less56_out_ag(T138, T134)) → U18_ga(T134, T138, T136, T142, in1_in_ga(T134, T142))
in1_in_ga(T169, tree(T173, T171, T174)) → U19_ga(T169, T173, T171, T174, p66_in_aga(T173, T169, T174))
p66_in_aga(0, s(T179), T180) → U9_aga(T179, T180, in1_in_ga(s(T179), T180))
in1_in_ga(0, tree(s(T220), T221, T213)) → U20_ga(T220, T221, T213, in11_in_a(T221))
U20_ga(T220, T221, T213, in11_out_a(T221)) → in1_out_ga(0, tree(s(T220), T221, T213))
in1_in_ga(s(T234), tree(s(T236), T237, T213)) → U21_ga(T234, T236, T237, T213, p41_in_gaa(T234, T236, T237))
U21_ga(T234, T236, T237, T213, p41_out_gaa(T234, T236, T237)) → in1_out_ga(s(T234), tree(s(T236), T237, T213))
in1_in_ga(T248, tree(T252, T250, T253)) → U22_ga(T248, T252, T250, T253, p66_in_aga(T252, T248, T253))
p66_in_aga(s(T193), s(T192), T194) → U10_aga(T193, T192, T194, p73_in_aga(T193, T192, T194))
p73_in_aga(T193, T192, T194) → U11_aga(T193, T192, T194, less56_in_ag(T193, T192))
U11_aga(T193, T192, T194, less56_out_ag(T193, T192)) → p73_out_aga(T193, T192, T194)
p73_in_aga(T193, T192, T197) → U12_aga(T193, T192, T197, less56_in_ag(T193, T192))
U12_aga(T193, T192, T197, less56_out_ag(T193, T192)) → U13_aga(T193, T192, T197, in1_in_ga(s(T192), T197))
in1_in_ga(s(T270), tree(0, T262, T271)) → U23_ga(T270, T262, T271, in1_in_ga(s(T270), T271))
in1_in_ga(s(T283), tree(s(T284), T262, T285)) → U24_ga(T283, T284, T262, T285, p73_in_aga(T284, T283, T285))
U24_ga(T283, T284, T262, T285, p73_out_aga(T284, T283, T285)) → in1_out_ga(s(T283), tree(s(T284), T262, T285))
U23_ga(T270, T262, T271, in1_out_ga(s(T270), T271)) → in1_out_ga(s(T270), tree(0, T262, T271))
U13_aga(T193, T192, T197, in1_out_ga(s(T192), T197)) → p73_out_aga(T193, T192, T197)
U10_aga(T193, T192, T194, p73_out_aga(T193, T192, T194)) → p66_out_aga(s(T193), s(T192), T194)
U22_ga(T248, T252, T250, T253, p66_out_aga(T252, T248, T253)) → in1_out_ga(T248, tree(T252, T250, T253))
U9_aga(T179, T180, in1_out_ga(s(T179), T180)) → p66_out_aga(0, s(T179), T180)
U19_ga(T169, T173, T171, T174, p66_out_aga(T173, T169, T174)) → in1_out_ga(T169, tree(T173, T171, T174))
U18_ga(T134, T138, T136, T142, in1_out_ga(T134, T142)) → in1_out_ga(T134, tree(T138, T136, T142))
U8_gaa(T97, T99, T103, in1_out_ga(s(T97), T103)) → p41_out_gaa(T97, T99, T103)
U15_ga(T97, T99, T100, T16, p41_out_gaa(T97, T99, T100)) → in1_out_ga(s(T97), tree(s(T99), T100, T16))
IN1_IN_GA(s(T97), tree(s(T99), T100, T16)) → P41_IN_GAA(T97, T99, T100)
P41_IN_GAA(T97, T99, T103) → U7_GAA(T97, T99, T103, less43_in_ga(T97, T99))
U7_GAA(T97, T99, T103, less43_out_ga(T97, T99)) → IN1_IN_GA(s(T97), T103)
IN1_IN_GA(T134, tree(T138, T136, T142)) → U17_GA(T134, T138, T136, T142, less56_in_ag(T138, T134))
U17_GA(T134, T138, T136, T142, less56_out_ag(T138, T134)) → IN1_IN_GA(T134, T142)
IN1_IN_GA(T169, tree(T173, T171, T174)) → P66_IN_AGA(T173, T169, T174)
P66_IN_AGA(0, s(T179), T180) → IN1_IN_GA(s(T179), T180)
IN1_IN_GA(s(T270), tree(0, T262, T271)) → IN1_IN_GA(s(T270), T271)
IN1_IN_GA(s(T283), tree(s(T284), T262, T285)) → P73_IN_AGA(T284, T283, T285)
P73_IN_AGA(T193, T192, T197) → U12_AGA(T193, T192, T197, less56_in_ag(T193, T192))
U12_AGA(T193, T192, T197, less56_out_ag(T193, T192)) → IN1_IN_GA(s(T192), T197)
P66_IN_AGA(s(T193), s(T192), T194) → P73_IN_AGA(T193, T192, T194)
less43_in_ga(0, s(T110)) → less43_out_ga(0, s(T110))
less43_in_ga(s(T115), s(T117)) → U4_ga(T115, T117, less43_in_ga(T115, T117))
less56_in_ag(0, s(T149)) → less56_out_ag(0, s(T149))
less56_in_ag(s(T156), s(T155)) → U5_ag(T156, T155, less56_in_ag(T156, T155))
U4_ga(T115, T117, less43_out_ga(T115, T117)) → less43_out_ga(s(T115), s(T117))
U5_ag(T156, T155, less56_out_ag(T156, T155)) → less56_out_ag(s(T156), s(T155))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
P41_IN_GAA(T97) → U7_GAA(T97, less43_in_ga(T97))
U7_GAA(T97, less43_out_ga) → IN1_IN_GA(s(T97))
IN1_IN_GA(T134) → U17_GA(T134, less56_in_ag(T134))
U17_GA(T134, less56_out_ag(T138)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P73_IN_AGA(T192) → U12_AGA(T192, less56_in_ag(T192))
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U7_GAA(T97, less43_out_ga) → IN1_IN_GA(s(T97))
IN1_IN_GA(T134) → U17_GA(T134, less56_in_ag(T134))
U17_GA(T134, less56_out_ag(T138)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P73_IN_AGA(T192) → U12_AGA(T192, less56_in_ag(T192))
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U7_GAA(T97, less43_out_ga) → IN1_IN_GA(s(T97))
U17_GA(T134, less56_out_ag(T138)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P73_IN_AGA(T192) → U12_AGA(T192, less56_in_ag(T192))
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U7_GAA(T97, less43_out_ga) → IN1_IN_GA(s(T97))
U17_GA(T134, less56_out_ag(T138)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
U17_GA(T134, less56_out_ag(T138)) → IN1_IN_GA(T134)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
IN1_IN_GA(T169) → P66_IN_AGA(T169)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
U12_AGA(T192, less56_out_ag(T193)) → IN1_IN_GA(s(T192))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
U12_AGA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(T97)) → P41_IN_GAA(T97)
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(s(z0)))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
IN1_IN_GA(s(T283)) → P73_IN_AGA(T283)
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
IN1_IN_GA(s(s(y_0))) → P73_IN_AGA(s(y_0))
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
P66_IN_AGA(s(T192)) → P73_IN_AGA(T192)
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
IN1_IN_GA(s(s(y_0))) → P73_IN_AGA(s(y_0))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)
P66_IN_AGA(s(s(y_0))) → P73_IN_AGA(s(y_0))
P66_IN_AGA(s(T179)) → IN1_IN_GA(s(T179))
IN1_IN_GA(s(T270)) → IN1_IN_GA(s(T270))
P41_IN_GAA(0) → U7_GAA(0, less43_out_ga)
P41_IN_GAA(s(x0)) → U7_GAA(s(x0), U4_ga(less43_in_ga(x0)))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), less56_out_ag(0))
IN1_IN_GA(s(x0)) → U17_GA(s(x0), U5_ag(less56_in_ag(x0)))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), less56_out_ag(0))
P73_IN_AGA(s(x0)) → U12_AGA(s(x0), U5_ag(less56_in_ag(x0)))
U7_GAA(0, less43_out_ga) → IN1_IN_GA(s(0))
U7_GAA(s(z0), less43_out_ga) → IN1_IN_GA(s(s(z0)))
U17_GA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(z0))
U17_GA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(z0))
IN1_IN_GA(s(z0)) → P66_IN_AGA(s(z0))
IN1_IN_GA(s(0)) → P66_IN_AGA(s(0))
IN1_IN_GA(s(s(z0))) → P66_IN_AGA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(0)) → IN1_IN_GA(s(s(z0)))
U12_AGA(s(z0), less56_out_ag(x1)) → IN1_IN_GA(s(s(z0)))
IN1_IN_GA(s(0)) → P41_IN_GAA(0)
IN1_IN_GA(s(s(y_0))) → P41_IN_GAA(s(y_0))
IN1_IN_GA(s(s(y_0))) → P73_IN_AGA(s(y_0))
P66_IN_AGA(s(s(y_0))) → P73_IN_AGA(s(y_0))
less43_in_ga(0) → less43_out_ga
less43_in_ga(s(T115)) → U4_ga(less43_in_ga(T115))
less56_in_ag(s(T149)) → less56_out_ag(0)
less56_in_ag(s(T155)) → U5_ag(less56_in_ag(T155))
U4_ga(less43_out_ga) → less43_out_ga
U5_ag(less56_out_ag(T156)) → less56_out_ag(s(T156))
less43_in_ga(x0)
less56_in_ag(x0)
U4_ga(x0)
U5_ag(x0)