#define ORDER_PP_DEF_1int_is_positive \
    ORDER_PP_FN(8fn(8X, 8is_0(8tuple_at_0(8X))))

#define ORDER_PP_DEF_1int_get_unsigned \
    ORDER_PP_FN(8fn(8X, 8tuple_at_1(8X)))

#define ORDER_PP_DEF_1int_add_impl \
    ORDER_PP_FN(8fn(8A, 8B, 8S, 8int(8S, 8add(8A, 8B))))

#define ORDER_PP_DEF_1int_sub_impl \
    ORDER_PP_FN(8fn(8A, 8B, \
                    8if(8greater(8A, 8B), \
                        8int(0, 8sub(8A, 8B)), \
                        8int(1, 8sub(8B, 8A)))))

#define ORDER_PP_DEF_8int_add \
    ORDER_PP_FN(8fn(8A, 8B, \
                    8cond((8and(1int_is_positive(8A), 1int_is_positive(8B)), \
                                1int_add_impl(1int_get_unsigned(8A), 1int_get_unsigned(8B), 0)) \
                          (8and(1int_is_positive(8A), 8not(1int_is_positive(8B))), \
                                1int_sub_impl(1int_get_unsigned(8A), 1int_get_unsigned(8B))) \
                          (8and(8not(1int_is_positive(8A)), 1int_is_positive(8B)), \
                                1int_sub_impl(1int_get_unsigned(8B), 1int_get_unsigned(8A))) \
                          (8and(8not(1int_is_positive(8A)), 8not(1int_is_positive(8B))), \
                                1int_add_impl(1int_get_unsigned(8A), 1int_get_unsigned(8B), 1)))))

#define ORDER_PP_DEF_8int_to_lit \
    ORDER_PP_FN(8fn(8X, \
                    8if(1int_is_positive(8X), \
                        8to_lit(1int_get_unsigned(8X)), \
                        8adjacent(8(-), 8to_lit(1int_get_unsigned(8X))))))

#define ORDER_PP_DEF_8int \
    ORDER_PP_FN(8fn(8S, 8N, 8pair(8S, 8N)))

ORDER_PP(8int_to_lit(8int_add(A, B)))