ORDER_PP(
  8let((8P,
        8seq_head(
          8seq_sort(8fn(8P, 8Q, 8greater(8tuple_at_1(8P),
                                         8tuple_at_1(8Q))),
                    8seq_map(8fn(8N,
                                 8pair(8N, 8seq_size(8hailstone(8N)))),
                             8seq_iota(1, 8nat(1,0,0,0,0,0)))))),
       8pair(8to_lit(8tuple_at_0(8P)), 8to_lit(8tuple_at_1(8P)))) )