# Generated by tools/translator: qualified upstream name -> MoonBit name.
POW_2_SQRT pow_2_sqrt
POW_2_SQRT_ABS pow_2_sqrt_abs
REAL_ABS_0 real_abs_0
REAL_ABS_1 real_abs_1
REAL_ABS_ABS real_abs_abs
REAL_ABS_BETWEEN real_abs_between
REAL_ABS_BETWEEN1 real_abs_between1
REAL_ABS_BETWEEN2 real_abs_between2
REAL_ABS_BOUND real_abs_bound
REAL_ABS_BOUNDS real_abs_bounds
REAL_ABS_CASES real_abs_cases
REAL_ABS_CIRCLE real_abs_circle
REAL_ABS_DIV real_abs_div
REAL_ABS_INV real_abs_inv
REAL_ABS_LE real_abs_le
REAL_ABS_LE_SQRT real_abs_le_sqrt
REAL_ABS_LE_SQRT_POS real_abs_le_sqrt_pos
REAL_ABS_MUL real_abs_mul
REAL_ABS_NZ real_abs_nz
REAL_ABS_POS real_abs_pos
REAL_ABS_POW real_abs_pow
REAL_ABS_REFL real_abs_refl
REAL_ABS_SGN real_abs_sgn
REAL_ABS_SIGN real_abs_sign
REAL_ABS_SIGN2 real_abs_sign2
REAL_ABS_SQRT real_abs_sqrt
REAL_ABS_STILLNZ real_abs_stillnz
REAL_ABS_SUB real_abs_sub
REAL_ABS_SUB_ABS real_abs_sub_abs
REAL_ABS_TRIANGLE real_abs_triangle
REAL_ABS_TRIANGLE_LE real_abs_triangle_le
REAL_ABS_TRIANGLE_LT real_abs_triangle_lt
REAL_ABS_ZERO real_abs_zero
REAL_ADD2_SUB2 real_add2_sub2
REAL_ADD_RDISTRIB real_add_rdistrib
REAL_ADD_SUB real_add_sub
REAL_ADD_SUB2 real_add_sub2
REAL_ARCH real_arch
REAL_ARCH_INV real_arch_inv
REAL_ARCH_LT real_arch_lt
REAL_ARCH_POW real_arch_pow
REAL_ARCH_POW2 real_arch_pow2
REAL_ARCH_POW_INV real_arch_pow_inv
REAL_ARCH_SIMPLE real_arch_simple
REAL_ARITH_TAC real_arith_tac
REAL_BOUNDS_LE real_bounds_le
REAL_BOUNDS_LT real_bounds_lt
REAL_CONVEX_BOUND2_LE real_convex_bound2_le
REAL_CONVEX_BOUND2_LT real_convex_bound2_lt
REAL_CONVEX_BOUNDS_LE real_convex_bounds_le
REAL_CONVEX_BOUNDS_LT real_convex_bounds_lt
REAL_CONVEX_BOUND_GE real_convex_bound_ge
REAL_CONVEX_BOUND_GT real_convex_bound_gt
REAL_CONVEX_BOUND_LE real_convex_bound_le
REAL_CONVEX_BOUND_LT real_convex_bound_lt
REAL_DIFFSQ real_diffsq
REAL_DIV_1 real_div_1
REAL_DIV_EQ_0 real_div_eq_0
REAL_DIV_EQ_1 real_div_eq_1
REAL_DIV_LMUL real_div_lmul
REAL_DIV_POW2 real_div_pow2
REAL_DIV_POW2_ALT real_div_pow2_alt
REAL_DIV_REFL real_div_refl
REAL_DIV_RMUL real_div_rmul
REAL_DIV_SQRT real_div_sqrt
REAL_DOWN real_down
REAL_DOWN2 real_down2
REAL_EQ_ADD_LCANCEL_0 real_eq_add_lcancel_0
REAL_EQ_ADD_RCANCEL_0 real_eq_add_rcancel_0
REAL_EQ_IMP_LE real_eq_imp_le
REAL_EQ_INV2 real_eq_inv2
REAL_EQ_LCANCEL_IMP real_eq_lcancel_imp
REAL_EQ_LDIV_EQ real_eq_ldiv_eq
REAL_EQ_MUL_LCANCEL real_eq_mul_lcancel
REAL_EQ_MUL_RCANCEL real_eq_mul_rcancel
REAL_EQ_NEG2 real_eq_neg2
REAL_EQ_RCANCEL_IMP real_eq_rcancel_imp
REAL_EQ_RDIV_EQ real_eq_rdiv_eq
REAL_EQ_SGN_ABS real_eq_sgn_abs
REAL_EQ_SQUARE_ABS real_eq_square_abs
REAL_EQ_SUB_LADD real_eq_sub_ladd
REAL_EQ_SUB_RADD real_eq_sub_radd
REAL_EVENPOW_ABS real_evenpow_abs
REAL_INV_1 real_inv_1
REAL_INV_1_LE real_inv_1_le
REAL_INV_1_LT real_inv_1_lt
REAL_INV_DIV real_inv_div
REAL_INV_EQ_0 real_inv_eq_0
REAL_INV_EQ_1 real_inv_eq_1
REAL_INV_INV real_inv_inv
REAL_INV_LE_1 real_inv_le_1
REAL_INV_LT_1 real_inv_lt_1
REAL_INV_MUL real_inv_mul
REAL_INV_NEG real_inv_neg
REAL_INV_POW real_inv_pow
REAL_INV_SGN real_inv_sgn
REAL_LET_ADD2 real_let_add2
REAL_LET_ANTISYM real_let_antisym
REAL_LET_IMP real_let_imp
REAL_LE_01 real_le_01
REAL_LE_ADD2 real_le_add2
REAL_LE_ADDL real_le_addl
REAL_LE_ADDR real_le_addr
REAL_LE_DIV real_le_div
REAL_LE_DIV2_EQ real_le_div2_eq
REAL_LE_DOUBLE real_le_double
REAL_LE_IMP real_le_imp
REAL_LE_INV real_le_inv
REAL_LE_INV2 real_le_inv2
REAL_LE_INV_EQ real_le_inv_eq
REAL_LE_LADD real_le_ladd
REAL_LE_LCANCEL_IMP real_le_lcancel_imp
REAL_LE_LDIV_EQ real_le_ldiv_eq
REAL_LE_LINV real_le_linv
REAL_LE_LMUL real_le_lmul
REAL_LE_LMUL_EQ real_le_lmul_eq
REAL_LE_LSQRT real_le_lsqrt
REAL_LE_MAX real_le_max
REAL_LE_MIN real_le_min
REAL_LE_MUL2 real_le_mul2
REAL_LE_MUL_EQ real_le_mul_eq
REAL_LE_NEGL real_le_negl
REAL_LE_NEGR real_le_negr
REAL_LE_POW2 real_le_pow2
REAL_LE_POW_2 real_le_pow_2
REAL_LE_RADD real_le_radd
REAL_LE_RCANCEL_IMP real_le_rcancel_imp
REAL_LE_RDIV_EQ real_le_rdiv_eq
REAL_LE_RINV real_le_rinv
REAL_LE_RMUL real_le_rmul
REAL_LE_RMUL_EQ real_le_rmul_eq
REAL_LE_RSQRT real_le_rsqrt
REAL_LE_SQUARE_ABS real_le_square_abs
REAL_LE_SUB_LADD real_le_sub_ladd
REAL_LE_SUB_RADD real_le_sub_radd
REAL_LNEG_UNIQ real_lneg_uniq
REAL_LSQRT_LE real_lsqrt_le
REAL_LTE_ADD2 real_lte_add2
REAL_LT_01 real_lt_01
REAL_LT_ADD1 real_lt_add1
REAL_LT_ADD2 real_lt_add2
REAL_LT_ADDL real_lt_addl
REAL_LT_ADDNEG real_lt_addneg
REAL_LT_ADDNEG2 real_lt_addneg2
REAL_LT_ADDR real_lt_addr
REAL_LT_ADD_SUB real_lt_add_sub
REAL_LT_ANTISYM real_lt_antisym
REAL_LT_DIV real_lt_div
REAL_LT_DIV2_EQ real_lt_div2_eq
REAL_LT_GT real_lt_gt
REAL_LT_IMP_NE real_lt_imp_ne
REAL_LT_IMP_NZ real_lt_imp_nz
REAL_LT_INV real_lt_inv
REAL_LT_INV2 real_lt_inv2
REAL_LT_INV_EQ real_lt_inv_eq
REAL_LT_LADD real_lt_ladd
REAL_LT_LADD_IMP real_lt_ladd_imp
REAL_LT_LCANCEL_IMP real_lt_lcancel_imp
REAL_LT_LDIV_EQ real_lt_ldiv_eq
REAL_LT_LINV real_lt_linv
REAL_LT_LMUL real_lt_lmul
REAL_LT_LMUL_EQ real_lt_lmul_eq
REAL_LT_LNEG real_lt_lneg
REAL_LT_LSQRT real_lt_lsqrt
REAL_LT_MAX real_lt_max
REAL_LT_MIN real_lt_min
REAL_LT_MUL real_lt_mul
REAL_LT_MUL2 real_lt_mul2
REAL_LT_MUL_EQ real_lt_mul_eq
REAL_LT_NEG2 real_lt_neg2
REAL_LT_NEGTOTAL real_lt_negtotal
REAL_LT_POW2 real_lt_pow2
REAL_LT_POW_2 real_lt_pow_2
REAL_LT_RADD real_lt_radd
REAL_LT_RCANCEL_IMP real_lt_rcancel_imp
REAL_LT_RDIV_EQ real_lt_rdiv_eq
REAL_LT_RINV real_lt_rinv
REAL_LT_RMUL real_lt_rmul
REAL_LT_RMUL_EQ real_lt_rmul_eq
REAL_LT_RNEG real_lt_rneg
REAL_LT_RSQRT real_lt_rsqrt
REAL_LT_SQUARE real_lt_square
REAL_LT_SQUARE_ABS real_lt_square_abs
REAL_LT_SUB_LADD real_lt_sub_ladd
REAL_LT_SUB_RADD real_lt_sub_radd
REAL_LT_TOTAL real_lt_total
REAL_MAX_ACI real_max_aci
REAL_MAX_ASSOC real_max_assoc
REAL_MAX_LE real_max_le
REAL_MAX_LT real_max_lt
REAL_MAX_MAX real_max_max
REAL_MAX_MIN real_max_min
REAL_MAX_SYM real_max_sym
REAL_MIN_ACI real_min_aci
REAL_MIN_ASSOC real_min_assoc
REAL_MIN_LE real_min_le
REAL_MIN_LT real_min_lt
REAL_MIN_MAX real_min_max
REAL_MIN_MIN real_min_min
REAL_MIN_SYM real_min_sym
REAL_MUL_2 real_mul_2
REAL_MUL_AC real_mul_ac
REAL_MUL_LINV_UNIQ real_mul_linv_uniq
REAL_MUL_POS_LE real_mul_pos_le
REAL_MUL_POS_LT real_mul_pos_lt
REAL_MUL_RINV real_mul_rinv
REAL_MUL_RINV_UNIQ real_mul_rinv_uniq
REAL_NEG_EQ real_neg_eq
REAL_NEG_EQ_0 real_neg_eq_0
REAL_NEG_GE0 real_neg_ge0
REAL_NEG_GT0 real_neg_gt0
REAL_NEG_LE0 real_neg_le0
REAL_NEG_LMUL real_neg_lmul
REAL_NEG_LT0 real_neg_lt0
REAL_NEG_MINUS1 real_neg_minus1
REAL_NEG_MUL2 real_neg_mul2
REAL_NEG_RMUL real_neg_rmul
REAL_NOT_EQ real_not_eq
REAL_NOT_LE real_not_le
REAL_OF_NUM_CLAUSES real_of_num_clauses
REAL_OF_NUM_DIV real_of_num_div
REAL_OF_NUM_GE real_of_num_ge
REAL_OF_NUM_GT real_of_num_gt
REAL_OF_NUM_LT real_of_num_lt
REAL_OF_NUM_MAX real_of_num_max
REAL_OF_NUM_MIN real_of_num_min
REAL_OF_NUM_MOD real_of_num_mod
REAL_OF_NUM_SUB real_of_num_sub
REAL_OF_NUM_SUB_CASES real_of_num_sub_cases
REAL_OF_NUM_SUC real_of_num_suc
REAL_POS_EQ_SQUARE real_pos_eq_square
REAL_POW2_ABS real_pow2_abs
REAL_POW_1 real_pow_1
REAL_POW_1_LE real_pow_1_le
REAL_POW_1_LT real_pow_1_lt
REAL_POW_ADD real_pow_add
REAL_POW_DIV real_pow_div
REAL_POW_EQ real_pow_eq
REAL_POW_EQ_0 real_pow_eq_0
REAL_POW_EQ_1 real_pow_eq_1
REAL_POW_EQ_1_IMP real_pow_eq_1_imp
REAL_POW_EQ_ABS real_pow_eq_abs
REAL_POW_EQ_EQ real_pow_eq_eq
REAL_POW_EQ_ODD real_pow_eq_odd
REAL_POW_EQ_ODD_EQ real_pow_eq_odd_eq
REAL_POW_INV real_pow_inv
REAL_POW_LBOUND real_pow_lbound
REAL_POW_LE real_pow_le
REAL_POW_LE2 real_pow_le2
REAL_POW_LE2_ODD real_pow_le2_odd
REAL_POW_LE2_ODD_EQ real_pow_le2_odd_eq
REAL_POW_LE2_REV real_pow_le2_rev
REAL_POW_LE_1 real_pow_le_1
REAL_POW_LT real_pow_lt
REAL_POW_LT2 real_pow_lt2
REAL_POW_LT2_ODD real_pow_lt2_odd
REAL_POW_LT2_ODD_EQ real_pow_lt2_odd_eq
REAL_POW_LT2_REV real_pow_lt2_rev
REAL_POW_LT_1 real_pow_lt_1
REAL_POW_MONO real_pow_mono
REAL_POW_MONO_INV real_pow_mono_inv
REAL_POW_MONO_LT real_pow_mono_lt
REAL_POW_MUL real_pow_mul
REAL_POW_NZ real_pow_nz
REAL_POW_ONE real_pow_one
REAL_POW_POW real_pow_pow
REAL_POW_SUB real_pow_sub
REAL_POW_ZERO real_pow_zero
REAL_RNEG_UNIQ real_rneg_uniq
REAL_RSQRT_LE real_rsqrt_le
REAL_SGN real_sgn_v1
REAL_SGNS_EQ real_sgns_eq
REAL_SGNS_EQ_ALT real_sgns_eq_alt
REAL_SGN_0 real_sgn_0
REAL_SGN_ABS real_sgn_abs
REAL_SGN_ABS_ALT real_sgn_abs_alt
REAL_SGN_CASES real_sgn_cases
REAL_SGN_DIV real_sgn_div
REAL_SGN_EQ real_sgn_eq
REAL_SGN_EQ_INEQ real_sgn_eq_ineq
REAL_SGN_INEQS real_sgn_ineqs
REAL_SGN_INV real_sgn_inv
REAL_SGN_MUL real_sgn_mul
REAL_SGN_NEG real_sgn_neg
REAL_SGN_POW real_sgn_pow
REAL_SGN_POW_2 real_sgn_pow_2
REAL_SGN_REAL_SGN real_sgn_real_sgn
REAL_SGN_SQRT real_sgn_sqrt
REAL_SOS_EQ_0 real_sos_eq_0
REAL_SQRT_POW_2 real_sqrt_pow_2
REAL_SUB_ABS real_sub_abs
REAL_SUB_ADD real_sub_add
REAL_SUB_ADD2 real_sub_add2
REAL_SUB_INV real_sub_inv
REAL_SUB_LDISTRIB real_sub_ldistrib
REAL_SUB_LNEG real_sub_lneg
REAL_SUB_LZERO real_sub_lzero
REAL_SUB_NEG2 real_sub_neg2
REAL_SUB_RDISTRIB real_sub_rdistrib
REAL_SUB_REFL real_sub_refl
REAL_SUB_RNEG real_sub_rneg
REAL_SUB_RZERO real_sub_rzero
REAL_SUB_SUB real_sub_sub
REAL_SUB_SUB2 real_sub_sub2
REAL_SUB_TRIANGLE real_sub_triangle
REAL_WLOG_LE real_wlog_le
REAL_WLOG_LE_3 real_wlog_le_3
REAL_WLOG_LT real_wlog_lt
SQRT_0 sqrt_0
SQRT_1 sqrt_1
SQRT_DIV sqrt_div
SQRT_EQ_0 sqrt_eq_0
SQRT_EQ_1 sqrt_eq_1
SQRT_EVEN_POW2 sqrt_even_pow2
SQRT_INJ sqrt_inj
SQRT_INV sqrt_inv
SQRT_LE_0 sqrt_le_0
SQRT_LT_0 sqrt_lt_0
SQRT_MONO_LE sqrt_mono_le
SQRT_MONO_LE_EQ sqrt_mono_le_eq
SQRT_MONO_LT sqrt_mono_lt
SQRT_MONO_LT_EQ sqrt_mono_lt_eq
SQRT_MUL sqrt_mul
SQRT_NEG sqrt_neg
SQRT_POS_LE sqrt_pos_le
SQRT_POS_LT sqrt_pos_lt
SQRT_POW2 sqrt_pow2
SQRT_POW_2 sqrt_pow_2
SQRT_UNIQUE sqrt_unique
SQRT_UNIQUE_GEN sqrt_unique_gen
SQRT_WORKS sqrt_works
SQRT_WORKS_GEN sqrt_works_gen
real_sgn real_sgn
sqrt sqrt
