mCRL2
Loading...
Searching...
No Matches
mcrl2::data::sort_nat Namespace Reference

Namespace for system defined sort nat. More...

Typedefs

typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
 

Functions

const core::identifier_stringnat_name ()
 
const basic_sortnat ()
 Constructor for sort expression Nat.
 
bool is_nat (const sort_expression &e)
 Recogniser for sort expression Nat.
 
const core::identifier_stringnatpair_name ()
 
const basic_sortnatpair ()
 Constructor for sort expression @NatPair.
 
bool is_natpair (const sort_expression &e)
 Recogniser for sort expression @NatPair.
 
const core::identifier_stringc0_name ()
 Generate identifier @c0.
 
const function_symbolc0 ()
 Constructor for function symbol @c0.
 
bool is_c0_function_symbol (const atermpp::aterm &e)
 Recogniser for function @c0.
 
const core::identifier_stringcnat_name ()
 Generate identifier @cNat.
 
const function_symbolcnat ()
 Constructor for function symbol @cNat.
 
bool is_cnat_function_symbol (const atermpp::aterm &e)
 Recogniser for function @cNat.
 
application cnat (const data_expression &arg0)
 Application of function symbol @cNat.
 
void make_cnat (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @cNat.
 
bool is_cnat_application (const atermpp::aterm &e)
 Recogniser for application of @cNat.
 
const core::identifier_stringcpair_name ()
 Generate identifier @cPair.
 
const function_symbolcpair ()
 Constructor for function symbol @cPair.
 
bool is_cpair_function_symbol (const atermpp::aterm &e)
 Recogniser for function @cPair.
 
application cpair (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @cPair.
 
void make_cpair (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @cPair.
 
bool is_cpair_application (const atermpp::aterm &e)
 Recogniser for application of @cPair.
 
function_symbol_vector nat_generate_constructors_code ()
 Give all system defined constructors for nat.
 
function_symbol_vector nat_mCRL2_usable_constructors ()
 Give all defined constructors which can be used in mCRL2 specs for nat.
 
implementation_map nat_cpp_implementable_constructors ()
 Give all system defined constructors which have an implementation in C++ and not in rewrite rules for nat.
 
const core::identifier_stringpos2nat_name ()
 Generate identifier Pos2Nat.
 
const function_symbolpos2nat ()
 Constructor for function symbol Pos2Nat.
 
bool is_pos2nat_function_symbol (const atermpp::aterm &e)
 Recogniser for function Pos2Nat.
 
application pos2nat (const data_expression &arg0)
 Application of function symbol Pos2Nat.
 
void make_pos2nat (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Pos2Nat.
 
bool is_pos2nat_application (const atermpp::aterm &e)
 Recogniser for application of Pos2Nat.
 
const core::identifier_stringnat2pos_name ()
 Generate identifier Nat2Pos.
 
const function_symbolnat2pos ()
 Constructor for function symbol Nat2Pos.
 
bool is_nat2pos_function_symbol (const atermpp::aterm &e)
 Recogniser for function Nat2Pos.
 
application nat2pos (const data_expression &arg0)
 Application of function symbol Nat2Pos.
 
void make_nat2pos (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Nat2Pos.
 
bool is_nat2pos_application (const atermpp::aterm &e)
 Recogniser for application of Nat2Pos.
 
const core::identifier_stringmaximum_name ()
 Generate identifier max.
 
function_symbol maximum (const sort_expression &s0, const sort_expression &s1)
 
bool is_maximum_function_symbol (const atermpp::aterm &e)
 Recogniser for function max.
 
application maximum (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol max.
 
void make_maximum (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol max.
 
bool is_maximum_application (const atermpp::aterm &e)
 Recogniser for application of max.
 
const core::identifier_stringminimum_name ()
 Generate identifier min.
 
function_symbol minimum (const sort_expression &s0, const sort_expression &s1)
 
bool is_minimum_function_symbol (const atermpp::aterm &e)
 Recogniser for function min.
 
application minimum (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol min.
 
void make_minimum (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol min.
 
bool is_minimum_application (const atermpp::aterm &e)
 Recogniser for application of min.
 
const core::identifier_stringsucc_name ()
 Generate identifier succ.
 
function_symbol succ (const sort_expression &s0)
 
bool is_succ_function_symbol (const atermpp::aterm &e)
 Recogniser for function succ.
 
application succ (const data_expression &arg0)
 Application of function symbol succ.
 
void make_succ (data_expression &result, const data_expression &arg0)
 Make an application of function symbol succ.
 
bool is_succ_application (const atermpp::aterm &e)
 Recogniser for application of succ.
 
const core::identifier_stringpred_name ()
 Generate identifier pred.
 
const function_symbolpred ()
 Constructor for function symbol pred.
 
bool is_pred_function_symbol (const atermpp::aterm &e)
 Recogniser for function pred.
 
application pred (const data_expression &arg0)
 Application of function symbol pred.
 
void make_pred (data_expression &result, const data_expression &arg0)
 Make an application of function symbol pred.
 
bool is_pred_application (const atermpp::aterm &e)
 Recogniser for application of pred.
 
const core::identifier_stringdub_name ()
 Generate identifier @dub.
 
const function_symboldub ()
 Constructor for function symbol @dub.
 
bool is_dub_function_symbol (const atermpp::aterm &e)
 Recogniser for function @dub.
 
application dub (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @dub.
 
void make_dub (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @dub.
 
bool is_dub_application (const atermpp::aterm &e)
 Recogniser for application of @dub.
 
const core::identifier_stringdubsucc_name ()
 Generate identifier @dubsucc.
 
const function_symboldubsucc ()
 Constructor for function symbol @dubsucc.
 
bool is_dubsucc_function_symbol (const atermpp::aterm &e)
 Recogniser for function @dubsucc.
 
application dubsucc (const data_expression &arg0)
 Application of function symbol @dubsucc.
 
void make_dubsucc (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @dubsucc.
 
bool is_dubsucc_application (const atermpp::aterm &e)
 Recogniser for application of @dubsucc.
 
const core::identifier_stringplus_name ()
 Generate identifier +.
 
function_symbol plus (const sort_expression &s0, const sort_expression &s1)
 
bool is_plus_function_symbol (const atermpp::aterm &e)
 Recogniser for function +.
 
application plus (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol +.
 
void make_plus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol +.
 
bool is_plus_application (const atermpp::aterm &e)
 Recogniser for application of +.
 
const core::identifier_stringgte_subtract_with_borrow_name ()
 Generate identifier @gtesubtb.
 
const function_symbolgte_subtract_with_borrow ()
 Constructor for function symbol @gtesubtb.
 
bool is_gte_subtract_with_borrow_function_symbol (const atermpp::aterm &e)
 Recogniser for function @gtesubtb.
 
application gte_subtract_with_borrow (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @gtesubtb.
 
void make_gte_subtract_with_borrow (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @gtesubtb.
 
bool is_gte_subtract_with_borrow_application (const atermpp::aterm &e)
 Recogniser for application of @gtesubtb.
 
const core::identifier_stringtimes_name ()
 Generate identifier *.
 
function_symbol times (const sort_expression &s0, const sort_expression &s1)
 
bool is_times_function_symbol (const atermpp::aterm &e)
 Recogniser for function *.
 
application times (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol *.
 
void make_times (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol *.
 
bool is_times_application (const atermpp::aterm &e)
 Recogniser for application of *.
 
const core::identifier_stringdiv_name ()
 Generate identifier div.
 
const function_symboldiv ()
 Constructor for function symbol div.
 
bool is_div_function_symbol (const atermpp::aterm &e)
 Recogniser for function div.
 
application div (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol div.
 
void make_div (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol div.
 
bool is_div_application (const atermpp::aterm &e)
 Recogniser for application of div.
 
const core::identifier_stringmod_name ()
 Generate identifier mod.
 
const function_symbolmod ()
 Constructor for function symbol mod.
 
bool is_mod_function_symbol (const atermpp::aterm &e)
 Recogniser for function mod.
 
application mod (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol mod.
 
void make_mod (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol mod.
 
bool is_mod_application (const atermpp::aterm &e)
 Recogniser for application of mod.
 
const core::identifier_stringexp_name ()
 Generate identifier exp.
 
function_symbol exp (const sort_expression &s0, const sort_expression &s1)
 
bool is_exp_function_symbol (const atermpp::aterm &e)
 Recogniser for function exp.
 
application exp (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol exp.
 
void make_exp (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol exp.
 
bool is_exp_application (const atermpp::aterm &e)
 Recogniser for application of exp.
 
const core::identifier_stringeven_name ()
 Generate identifier @even.
 
const function_symboleven ()
 Constructor for function symbol @even.
 
bool is_even_function_symbol (const atermpp::aterm &e)
 Recogniser for function @even.
 
application even (const data_expression &arg0)
 Application of function symbol @even.
 
void make_even (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @even.
 
bool is_even_application (const atermpp::aterm &e)
 Recogniser for application of @even.
 
const core::identifier_stringmonus_name ()
 Generate identifier @monus.
 
const function_symbolmonus ()
 Constructor for function symbol @monus.
 
bool is_monus_function_symbol (const atermpp::aterm &e)
 Recogniser for function @monus.
 
application monus (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @monus.
 
void make_monus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @monus.
 
bool is_monus_application (const atermpp::aterm &e)
 Recogniser for application of @monus.
 
const core::identifier_stringswap_zero_name ()
 Generate identifier @swap_zero.
 
const function_symbolswap_zero ()
 Constructor for function symbol @swap_zero.
 
bool is_swap_zero_function_symbol (const atermpp::aterm &e)
 Recogniser for function @swap_zero.
 
application swap_zero (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @swap_zero.
 
void make_swap_zero (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @swap_zero.
 
bool is_swap_zero_application (const atermpp::aterm &e)
 Recogniser for application of @swap_zero.
 
const core::identifier_stringswap_zero_add_name ()
 Generate identifier @swap_zero_add.
 
const function_symbolswap_zero_add ()
 Constructor for function symbol @swap_zero_add.
 
bool is_swap_zero_add_function_symbol (const atermpp::aterm &e)
 Recogniser for function @swap_zero_add.
 
application swap_zero_add (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @swap_zero_add.
 
void make_swap_zero_add (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @swap_zero_add.
 
bool is_swap_zero_add_application (const atermpp::aterm &e)
 Recogniser for application of @swap_zero_add.
 
const core::identifier_stringswap_zero_min_name ()
 Generate identifier @swap_zero_min.
 
const function_symbolswap_zero_min ()
 Constructor for function symbol @swap_zero_min.
 
bool is_swap_zero_min_function_symbol (const atermpp::aterm &e)
 Recogniser for function @swap_zero_min.
 
application swap_zero_min (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @swap_zero_min.
 
void make_swap_zero_min (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @swap_zero_min.
 
bool is_swap_zero_min_application (const atermpp::aterm &e)
 Recogniser for application of @swap_zero_min.
 
const core::identifier_stringswap_zero_monus_name ()
 Generate identifier @swap_zero_monus.
 
const function_symbolswap_zero_monus ()
 Constructor for function symbol @swap_zero_monus.
 
bool is_swap_zero_monus_function_symbol (const atermpp::aterm &e)
 Recogniser for function @swap_zero_monus.
 
application swap_zero_monus (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @swap_zero_monus.
 
void make_swap_zero_monus (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @swap_zero_monus.
 
bool is_swap_zero_monus_application (const atermpp::aterm &e)
 Recogniser for application of @swap_zero_monus.
 
const core::identifier_stringsqrt_name ()
 Generate identifier sqrt.
 
const function_symbolsqrt ()
 Constructor for function symbol sqrt.
 
bool is_sqrt_function_symbol (const atermpp::aterm &e)
 Recogniser for function sqrt.
 
application sqrt (const data_expression &arg0)
 Application of function symbol sqrt.
 
void make_sqrt (data_expression &result, const data_expression &arg0)
 Make an application of function symbol sqrt.
 
bool is_sqrt_application (const atermpp::aterm &e)
 Recogniser for application of sqrt.
 
const core::identifier_stringsqrt_nat_aux_func_name ()
 Generate identifier @sqrt_nat.
 
const function_symbolsqrt_nat_aux_func ()
 Constructor for function symbol @sqrt_nat.
 
bool is_sqrt_nat_aux_func_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_nat.
 
application sqrt_nat_aux_func (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @sqrt_nat.
 
void make_sqrt_nat_aux_func (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @sqrt_nat.
 
bool is_sqrt_nat_aux_func_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_nat.
 
const core::identifier_stringfirst_name ()
 Generate identifier @first.
 
const function_symbolfirst ()
 Constructor for function symbol @first.
 
bool is_first_function_symbol (const atermpp::aterm &e)
 Recogniser for function @first.
 
application first (const data_expression &arg0)
 Application of function symbol @first.
 
void make_first (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @first.
 
bool is_first_application (const atermpp::aterm &e)
 Recogniser for application of @first.
 
const core::identifier_stringlast_name ()
 Generate identifier @last.
 
const function_symbollast ()
 Constructor for function symbol @last.
 
bool is_last_function_symbol (const atermpp::aterm &e)
 Recogniser for function @last.
 
application last (const data_expression &arg0)
 Application of function symbol @last.
 
void make_last (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @last.
 
bool is_last_application (const atermpp::aterm &e)
 Recogniser for application of @last.
 
const core::identifier_stringdivmod_name ()
 Generate identifier @divmod.
 
const function_symboldivmod ()
 Constructor for function symbol @divmod.
 
bool is_divmod_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod.
 
application divmod (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @divmod.
 
void make_divmod (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @divmod.
 
bool is_divmod_application (const atermpp::aterm &e)
 Recogniser for application of @divmod.
 
const core::identifier_stringgeneralised_divmod_name ()
 Generate identifier @gdivmod.
 
const function_symbolgeneralised_divmod ()
 Constructor for function symbol @gdivmod.
 
bool is_generalised_divmod_function_symbol (const atermpp::aterm &e)
 Recogniser for function @gdivmod.
 
application generalised_divmod (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @gdivmod.
 
void make_generalised_divmod (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @gdivmod.
 
bool is_generalised_divmod_application (const atermpp::aterm &e)
 Recogniser for application of @gdivmod.
 
const core::identifier_stringdoubly_generalised_divmod_name ()
 Generate identifier @ggdivmod.
 
const function_symboldoubly_generalised_divmod ()
 Constructor for function symbol @ggdivmod.
 
bool is_doubly_generalised_divmod_function_symbol (const atermpp::aterm &e)
 Recogniser for function @ggdivmod.
 
application doubly_generalised_divmod (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @ggdivmod.
 
void make_doubly_generalised_divmod (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @ggdivmod.
 
bool is_doubly_generalised_divmod_application (const atermpp::aterm &e)
 Recogniser for application of @ggdivmod.
 
function_symbol_vector nat_generate_functions_code ()
 Give all system defined mappings for nat.
 
function_symbol_vector nat_generate_constructors_and_functions_code ()
 Give all system defined mappings and constructors for nat.
 
function_symbol_vector nat_mCRL2_usable_mappings ()
 Give all system defined mappings that can be used in mCRL2 specs for nat.
 
implementation_map nat_cpp_implementable_mappings ()
 Give all system defined mappings that are to be implemented in C++ code for nat.
 
const data_expressionarg (const data_expression &e)
 Function for projecting out argument. arg from an application.
 
const data_expressionarg1 (const data_expression &e)
 Function for projecting out argument. arg1 from an application.
 
const data_expressionarg2 (const data_expression &e)
 Function for projecting out argument. arg2 from an application.
 
const data_expressionleft (const data_expression &e)
 Function for projecting out argument. left from an application.
 
const data_expressionright (const data_expression &e)
 Function for projecting out argument. right from an application.
 
const data_expressionarg3 (const data_expression &e)
 Function for projecting out argument. arg3 from an application.
 
const data_expressionarg4 (const data_expression &e)
 Function for projecting out argument. arg4 from an application.
 
data_equation_vector nat_generate_equations_code ()
 Give all system defined equations for nat.
 
const core::identifier_stringnatnatpair_name ()
 
const basic_sortnatnatpair ()
 Constructor for sort expression @NatNatPair.
 
bool is_natnatpair (const sort_expression &e)
 Recogniser for sort expression @NatNatPair.
 
const core::identifier_stringsucc_nat_name ()
 Generate identifier @succ_nat.
 
const function_symbolsucc_nat ()
 Constructor for function symbol @succ_nat.
 
bool is_succ_nat_function_symbol (const atermpp::aterm &e)
 Recogniser for function @succ_nat.
 
application succ_nat (const data_expression &arg0)
 Application of function symbol @succ_nat.
 
void make_succ_nat (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @succ_nat.
 
bool is_succ_nat_application (const atermpp::aterm &e)
 Recogniser for application of @succ_nat.
 
const core::identifier_stringnnpair_name ()
 Generate identifier @nnPair.
 
const function_symbolnnpair ()
 Constructor for function symbol @nnPair.
 
bool is_nnpair_function_symbol (const atermpp::aterm &e)
 Recogniser for function @nnPair.
 
application nnpair (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @nnPair.
 
void make_nnpair (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @nnPair.
 
bool is_nnpair_application (const atermpp::aterm &e)
 Recogniser for application of @nnPair.
 
const core::identifier_stringmost_significant_digit_nat_name ()
 Generate identifier @most_significant_digitNat.
 
const function_symbolmost_significant_digit_nat ()
 Constructor for function symbol @most_significant_digitNat.
 
bool is_most_significant_digit_nat_function_symbol (const atermpp::aterm &e)
 Recogniser for function @most_significant_digitNat.
 
application most_significant_digit_nat (const data_expression &arg0)
 Application of function symbol @most_significant_digitNat.
 
void make_most_significant_digit_nat (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @most_significant_digitNat.
 
bool is_most_significant_digit_nat_application (const atermpp::aterm &e)
 Recogniser for application of @most_significant_digitNat.
 
const core::identifier_stringconcat_digit_name ()
 Generate identifier @concat_digit.
 
function_symbol concat_digit (const sort_expression &s0, const sort_expression &s1)
 
bool is_concat_digit_function_symbol (const atermpp::aterm &e)
 Recogniser for function @concat_digit.
 
application concat_digit (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @concat_digit.
 
void make_concat_digit (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @concat_digit.
 
bool is_concat_digit_application (const atermpp::aterm &e)
 Recogniser for application of @concat_digit.
 
const core::identifier_stringequals_zero_name ()
 Generate identifier @equals_zero.
 
const function_symbolequals_zero ()
 Constructor for function symbol @equals_zero.
 
bool is_equals_zero_function_symbol (const atermpp::aterm &e)
 Recogniser for function @equals_zero.
 
application equals_zero (const data_expression &arg0)
 Application of function symbol @equals_zero.
 
void make_equals_zero (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @equals_zero.
 
bool is_equals_zero_application (const atermpp::aterm &e)
 Recogniser for application of @equals_zero.
 
const core::identifier_stringnot_equals_zero_name ()
 Generate identifier @not_equals_zero.
 
const function_symbolnot_equals_zero ()
 Constructor for function symbol @not_equals_zero.
 
bool is_not_equals_zero_function_symbol (const atermpp::aterm &e)
 Recogniser for function @not_equals_zero.
 
application not_equals_zero (const data_expression &arg0)
 Application of function symbol @not_equals_zero.
 
void make_not_equals_zero (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @not_equals_zero.
 
bool is_not_equals_zero_application (const atermpp::aterm &e)
 Recogniser for application of @not_equals_zero.
 
const core::identifier_stringequals_one_name ()
 Generate identifier @equals_one.
 
function_symbol equals_one (const sort_expression &s0)
 
bool is_equals_one_function_symbol (const atermpp::aterm &e)
 Recogniser for function @equals_one.
 
application equals_one (const data_expression &arg0)
 Application of function symbol @equals_one.
 
void make_equals_one (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @equals_one.
 
bool is_equals_one_application (const atermpp::aterm &e)
 Recogniser for application of @equals_one.
 
const core::identifier_stringpred_whr_name ()
 Generate identifier @pred_whr.
 
const function_symbolpred_whr ()
 Constructor for function symbol @pred_whr.
 
bool is_pred_whr_function_symbol (const atermpp::aterm &e)
 Recogniser for function @pred_whr.
 
application pred_whr (const data_expression &arg0)
 Application of function symbol @pred_whr.
 
void make_pred_whr (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @pred_whr.
 
bool is_pred_whr_application (const atermpp::aterm &e)
 Recogniser for application of @pred_whr.
 
const core::identifier_stringadd_with_carry_name ()
 Generate identifier @add_with_carry.
 
function_symbol add_with_carry (const sort_expression &s0, const sort_expression &s1)
 
bool is_add_with_carry_function_symbol (const atermpp::aterm &e)
 Recogniser for function @add_with_carry.
 
application add_with_carry (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @add_with_carry.
 
void make_add_with_carry (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @add_with_carry.
 
bool is_add_with_carry_application (const atermpp::aterm &e)
 Recogniser for application of @add_with_carry.
 
const core::identifier_stringauxiliary_plus_nat_name ()
 Generate identifier @plus_nat.
 
const function_symbolauxiliary_plus_nat ()
 Constructor for function symbol @plus_nat.
 
bool is_auxiliary_plus_nat_function_symbol (const atermpp::aterm &e)
 Recogniser for function @plus_nat.
 
application auxiliary_plus_nat (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @plus_nat.
 
void make_auxiliary_plus_nat (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @plus_nat.
 
bool is_auxiliary_plus_nat_application (const atermpp::aterm &e)
 Recogniser for application of @plus_nat.
 
const core::identifier_stringtimes_ordered_name ()
 Generate identifier @times_ordered.
 
function_symbol times_ordered (const sort_expression &s0, const sort_expression &s1)
 
bool is_times_ordered_function_symbol (const atermpp::aterm &e)
 Recogniser for function @times_ordered.
 
application times_ordered (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @times_ordered.
 
void make_times_ordered (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @times_ordered.
 
bool is_times_ordered_application (const atermpp::aterm &e)
 Recogniser for application of @times_ordered.
 
const core::identifier_stringtimes_overflow_name ()
 Generate identifier @times_overflow.
 
function_symbol times_overflow (const sort_expression &s0, const sort_expression &s1, const sort_expression &s2)
 
bool is_times_overflow_function_symbol (const atermpp::aterm &e)
 Recogniser for function @times_overflow.
 
application times_overflow (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @times_overflow.
 
void make_times_overflow (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @times_overflow.
 
bool is_times_overflow_application (const atermpp::aterm &e)
 Recogniser for application of @times_overflow.
 
const core::identifier_stringnatpred_name ()
 Generate identifier @natpred.
 
const function_symbolnatpred ()
 Constructor for function symbol @natpred.
 
bool is_natpred_function_symbol (const atermpp::aterm &e)
 Recogniser for function @natpred.
 
application natpred (const data_expression &arg0)
 Application of function symbol @natpred.
 
void make_natpred (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @natpred.
 
bool is_natpred_application (const atermpp::aterm &e)
 Recogniser for application of @natpred.
 
const core::identifier_stringis_odd_name ()
 Generate identifier @is_odd.
 
const function_symbolis_odd ()
 Constructor for function symbol @is_odd.
 
bool is_is_odd_function_symbol (const atermpp::aterm &e)
 Recogniser for function @is_odd.
 
application is_odd (const data_expression &arg0)
 Application of function symbol @is_odd.
 
void make_is_odd (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @is_odd.
 
bool is_is_odd_application (const atermpp::aterm &e)
 Recogniser for application of @is_odd.
 
const core::identifier_stringdiv2_name ()
 Generate identifier @div2.
 
const function_symboldiv2 ()
 Constructor for function symbol @div2.
 
bool is_div2_function_symbol (const atermpp::aterm &e)
 Recogniser for function @div2.
 
application div2 (const data_expression &arg0)
 Application of function symbol @div2.
 
void make_div2 (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @div2.
 
bool is_div2_application (const atermpp::aterm &e)
 Recogniser for application of @div2.
 
const core::identifier_stringmonus_whr_name ()
 Generate identifier @monus_whr.
 
const function_symbolmonus_whr ()
 Constructor for function symbol @monus_whr.
 
bool is_monus_whr_function_symbol (const atermpp::aterm &e)
 Recogniser for function @monus_whr.
 
application monus_whr (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @monus_whr.
 
void make_monus_whr (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @monus_whr.
 
bool is_monus_whr_application (const atermpp::aterm &e)
 Recogniser for application of @monus_whr.
 
const core::identifier_stringexp_aux3p_name ()
 Generate identifier @exp_aux3p.
 
const function_symbolexp_aux3p ()
 Constructor for function symbol @exp_aux3p.
 
bool is_exp_aux3p_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_aux3p.
 
application exp_aux3p (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @exp_aux3p.
 
void make_exp_aux3p (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @exp_aux3p.
 
bool is_exp_aux3p_application (const atermpp::aterm &e)
 Recogniser for application of @exp_aux3p.
 
const core::identifier_stringexp_aux4p_name ()
 Generate identifier @exp_aux4p.
 
const function_symbolexp_aux4p ()
 Constructor for function symbol @exp_aux4p.
 
bool is_exp_aux4p_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_aux4p.
 
application exp_aux4p (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @exp_aux4p.
 
void make_exp_aux4p (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @exp_aux4p.
 
bool is_exp_aux4p_application (const atermpp::aterm &e)
 Recogniser for application of @exp_aux4p.
 
const core::identifier_stringexp_aux3n_name ()
 Generate identifier @exp_aux3n.
 
const function_symbolexp_aux3n ()
 Constructor for function symbol @exp_aux3n.
 
bool is_exp_aux3n_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_aux3n.
 
application exp_aux3n (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @exp_aux3n.
 
void make_exp_aux3n (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @exp_aux3n.
 
bool is_exp_aux3n_application (const atermpp::aterm &e)
 Recogniser for application of @exp_aux3n.
 
const core::identifier_stringexp_aux4n_name ()
 Generate identifier @exp_aux4n.
 
const function_symbolexp_aux4n ()
 Constructor for function symbol @exp_aux4n.
 
bool is_exp_aux4n_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_aux4n.
 
application exp_aux4n (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @exp_aux4n.
 
void make_exp_aux4n (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @exp_aux4n.
 
bool is_exp_aux4n_application (const atermpp::aterm &e)
 Recogniser for application of @exp_aux4n.
 
const core::identifier_stringexp_auxtruep_name ()
 Generate identifier @exp_auxtruep.
 
const function_symbolexp_auxtruep ()
 Constructor for function symbol @exp_auxtruep.
 
bool is_exp_auxtruep_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_auxtruep.
 
application exp_auxtruep (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @exp_auxtruep.
 
void make_exp_auxtruep (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @exp_auxtruep.
 
bool is_exp_auxtruep_application (const atermpp::aterm &e)
 Recogniser for application of @exp_auxtruep.
 
const core::identifier_stringexp_auxtruen_name ()
 Generate identifier @exp_auxtruen.
 
const function_symbolexp_auxtruen ()
 Constructor for function symbol @exp_auxtruen.
 
bool is_exp_auxtruen_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_auxtruen.
 
application exp_auxtruen (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @exp_auxtruen.
 
void make_exp_auxtruen (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @exp_auxtruen.
 
bool is_exp_auxtruen_application (const atermpp::aterm &e)
 Recogniser for application of @exp_auxtruen.
 
const core::identifier_stringexp_auxfalsep_name ()
 Generate identifier @exp_auxfalsep.
 
const function_symbolexp_auxfalsep ()
 Constructor for function symbol @exp_auxfalsep.
 
bool is_exp_auxfalsep_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_auxfalsep.
 
application exp_auxfalsep (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @exp_auxfalsep.
 
void make_exp_auxfalsep (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @exp_auxfalsep.
 
bool is_exp_auxfalsep_application (const atermpp::aterm &e)
 Recogniser for application of @exp_auxfalsep.
 
const core::identifier_stringexp_auxfalsen_name ()
 Generate identifier @exp_auxfalsen.
 
const function_symbolexp_auxfalsen ()
 Constructor for function symbol @exp_auxfalsen.
 
bool is_exp_auxfalsen_function_symbol (const atermpp::aterm &e)
 Recogniser for function @exp_auxfalsen.
 
application exp_auxfalsen (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @exp_auxfalsen.
 
void make_exp_auxfalsen (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @exp_auxfalsen.
 
bool is_exp_auxfalsen_application (const atermpp::aterm &e)
 Recogniser for application of @exp_auxfalsen.
 
const core::identifier_stringdiv_bold_name ()
 Generate identifier @div_bold.
 
const function_symboldiv_bold ()
 Constructor for function symbol @div_bold.
 
bool is_div_bold_function_symbol (const atermpp::aterm &e)
 Recogniser for function @div_bold.
 
application div_bold (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @div_bold.
 
void make_div_bold (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @div_bold.
 
bool is_div_bold_application (const atermpp::aterm &e)
 Recogniser for application of @div_bold.
 
const core::identifier_stringdiv_bold_whr_name ()
 Generate identifier @div_bold_whr.
 
const function_symboldiv_bold_whr ()
 Constructor for function symbol @div_bold_whr.
 
bool is_div_bold_whr_function_symbol (const atermpp::aterm &e)
 Recogniser for function @div_bold_whr.
 
application div_bold_whr (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4, const data_expression &arg5)
 Application of function symbol @div_bold_whr.
 
void make_div_bold_whr (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4, const data_expression &arg5)
 Make an application of function symbol @div_bold_whr.
 
bool is_div_bold_whr_application (const atermpp::aterm &e)
 Recogniser for application of @div_bold_whr.
 
const core::identifier_stringdiv_whr1_name ()
 Generate identifier @div_whr1.
 
const function_symboldiv_whr1 ()
 Constructor for function symbol @div_whr1.
 
bool is_div_whr1_function_symbol (const atermpp::aterm &e)
 Recogniser for function @div_whr1.
 
application div_whr1 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @div_whr1.
 
void make_div_whr1 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @div_whr1.
 
bool is_div_whr1_application (const atermpp::aterm &e)
 Recogniser for application of @div_whr1.
 
const core::identifier_stringdiv_whr2_name ()
 Generate identifier @div_whr2.
 
const function_symboldiv_whr2 ()
 Constructor for function symbol @div_whr2.
 
bool is_div_whr2_function_symbol (const atermpp::aterm &e)
 Recogniser for function @div_whr2.
 
application div_whr2 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @div_whr2.
 
void make_div_whr2 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @div_whr2.
 
bool is_div_whr2_application (const atermpp::aterm &e)
 Recogniser for application of @div_whr2.
 
const core::identifier_stringmod_whr1_name ()
 Generate identifier @mod_whr1.
 
const function_symbolmod_whr1 ()
 Constructor for function symbol @mod_whr1.
 
bool is_mod_whr1_function_symbol (const atermpp::aterm &e)
 Recogniser for function @mod_whr1.
 
application mod_whr1 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @mod_whr1.
 
void make_mod_whr1 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @mod_whr1.
 
bool is_mod_whr1_application (const atermpp::aterm &e)
 Recogniser for application of @mod_whr1.
 
const core::identifier_stringdivmod_aux_name ()
 Generate identifier @divmod_aux.
 
const function_symboldivmod_aux ()
 Constructor for function symbol @divmod_aux.
 
bool is_divmod_aux_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux.
 
application divmod_aux (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @divmod_aux.
 
void make_divmod_aux (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @divmod_aux.
 
bool is_divmod_aux_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux.
 
const core::identifier_stringdivmod_aux_whr1_name ()
 Generate identifier @divmod_aux_whr1.
 
const function_symboldivmod_aux_whr1 ()
 Constructor for function symbol @divmod_aux_whr1.
 
bool is_divmod_aux_whr1_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux_whr1.
 
application divmod_aux_whr1 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @divmod_aux_whr1.
 
void make_divmod_aux_whr1 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @divmod_aux_whr1.
 
bool is_divmod_aux_whr1_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux_whr1.
 
const core::identifier_stringdivmod_aux_whr2_name ()
 Generate identifier @divmod_aux_whr2.
 
const function_symboldivmod_aux_whr2 ()
 Constructor for function symbol @divmod_aux_whr2.
 
bool is_divmod_aux_whr2_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux_whr2.
 
application divmod_aux_whr2 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @divmod_aux_whr2.
 
void make_divmod_aux_whr2 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @divmod_aux_whr2.
 
bool is_divmod_aux_whr2_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux_whr2.
 
const core::identifier_stringdivmod_aux_whr3_name ()
 Generate identifier @divmod_aux_whr3.
 
const function_symboldivmod_aux_whr3 ()
 Constructor for function symbol @divmod_aux_whr3.
 
bool is_divmod_aux_whr3_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux_whr3.
 
application divmod_aux_whr3 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @divmod_aux_whr3.
 
void make_divmod_aux_whr3 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @divmod_aux_whr3.
 
bool is_divmod_aux_whr3_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux_whr3.
 
const core::identifier_stringdivmod_aux_whr4_name ()
 Generate identifier @divmod_aux_whr4.
 
const function_symboldivmod_aux_whr4 ()
 Constructor for function symbol @divmod_aux_whr4.
 
bool is_divmod_aux_whr4_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux_whr4.
 
application divmod_aux_whr4 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @divmod_aux_whr4.
 
void make_divmod_aux_whr4 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @divmod_aux_whr4.
 
bool is_divmod_aux_whr4_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux_whr4.
 
const core::identifier_stringdivmod_aux_whr5_name ()
 Generate identifier @divmod_aux_whr5.
 
const function_symboldivmod_aux_whr5 ()
 Constructor for function symbol @divmod_aux_whr5.
 
bool is_divmod_aux_whr5_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux_whr5.
 
application divmod_aux_whr5 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @divmod_aux_whr5.
 
void make_divmod_aux_whr5 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @divmod_aux_whr5.
 
bool is_divmod_aux_whr5_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux_whr5.
 
const core::identifier_stringdivmod_aux_whr6_name ()
 Generate identifier @divmod_aux_whr6.
 
const function_symboldivmod_aux_whr6 ()
 Constructor for function symbol @divmod_aux_whr6.
 
bool is_divmod_aux_whr6_function_symbol (const atermpp::aterm &e)
 Recogniser for function @divmod_aux_whr6.
 
application divmod_aux_whr6 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @divmod_aux_whr6.
 
void make_divmod_aux_whr6 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @divmod_aux_whr6.
 
bool is_divmod_aux_whr6_application (const atermpp::aterm &e)
 Recogniser for application of @divmod_aux_whr6.
 
const core::identifier_stringmsd_name ()
 Generate identifier @msd.
 
const function_symbolmsd ()
 Constructor for function symbol @msd.
 
bool is_msd_function_symbol (const atermpp::aterm &e)
 Recogniser for function @msd.
 
application msd (const data_expression &arg0)
 Application of function symbol @msd.
 
void make_msd (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @msd.
 
bool is_msd_application (const atermpp::aterm &e)
 Recogniser for application of @msd.
 
const core::identifier_stringsqrt_whr1_name ()
 Generate identifier @sqrt_whr1.
 
const function_symbolsqrt_whr1 ()
 Constructor for function symbol @sqrt_whr1.
 
bool is_sqrt_whr1_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_whr1.
 
application sqrt_whr1 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @sqrt_whr1.
 
void make_sqrt_whr1 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @sqrt_whr1.
 
bool is_sqrt_whr1_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_whr1.
 
const core::identifier_stringsqrt_whr2_name ()
 Generate identifier @sqrt_whr2.
 
const function_symbolsqrt_whr2 ()
 Constructor for function symbol @sqrt_whr2.
 
bool is_sqrt_whr2_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_whr2.
 
application sqrt_whr2 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @sqrt_whr2.
 
void make_sqrt_whr2 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @sqrt_whr2.
 
bool is_sqrt_whr2_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_whr2.
 
const core::identifier_stringsqrt_pair_name ()
 Generate identifier @sqrt_pair.
 
const function_symbolsqrt_pair ()
 Constructor for function symbol @sqrt_pair.
 
bool is_sqrt_pair_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair.
 
application sqrt_pair (const data_expression &arg0)
 Application of function symbol @sqrt_pair.
 
void make_sqrt_pair (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @sqrt_pair.
 
bool is_sqrt_pair_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair.
 
const core::identifier_stringsqrt_pair_whr1_name ()
 Generate identifier @sqrt_pair_whr1.
 
const function_symbolsqrt_pair_whr1 ()
 Constructor for function symbol @sqrt_pair_whr1.
 
bool is_sqrt_pair_whr1_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair_whr1.
 
application sqrt_pair_whr1 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @sqrt_pair_whr1.
 
void make_sqrt_pair_whr1 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @sqrt_pair_whr1.
 
bool is_sqrt_pair_whr1_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair_whr1.
 
const core::identifier_stringsqrt_pair_whr2_name ()
 Generate identifier @sqrt_pair_whr2.
 
const function_symbolsqrt_pair_whr2 ()
 Constructor for function symbol @sqrt_pair_whr2.
 
bool is_sqrt_pair_whr2_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair_whr2.
 
application sqrt_pair_whr2 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @sqrt_pair_whr2.
 
void make_sqrt_pair_whr2 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @sqrt_pair_whr2.
 
bool is_sqrt_pair_whr2_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair_whr2.
 
const core::identifier_stringsqrt_pair_whr3_name ()
 Generate identifier @sqrt_pair_whr3.
 
const function_symbolsqrt_pair_whr3 ()
 Constructor for function symbol @sqrt_pair_whr3.
 
bool is_sqrt_pair_whr3_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair_whr3.
 
application sqrt_pair_whr3 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @sqrt_pair_whr3.
 
void make_sqrt_pair_whr3 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @sqrt_pair_whr3.
 
bool is_sqrt_pair_whr3_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair_whr3.
 
const core::identifier_stringsqrt_pair_whr4_name ()
 Generate identifier @sqrt_pair_whr4.
 
const function_symbolsqrt_pair_whr4 ()
 Constructor for function symbol @sqrt_pair_whr4.
 
bool is_sqrt_pair_whr4_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair_whr4.
 
application sqrt_pair_whr4 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4, const data_expression &arg5)
 Application of function symbol @sqrt_pair_whr4.
 
void make_sqrt_pair_whr4 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4, const data_expression &arg5)
 Make an application of function symbol @sqrt_pair_whr4.
 
bool is_sqrt_pair_whr4_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair_whr4.
 
const core::identifier_stringsqrt_pair_whr5_name ()
 Generate identifier @sqrt_pair_whr5.
 
const function_symbolsqrt_pair_whr5 ()
 Constructor for function symbol @sqrt_pair_whr5.
 
bool is_sqrt_pair_whr5_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair_whr5.
 
application sqrt_pair_whr5 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Application of function symbol @sqrt_pair_whr5.
 
void make_sqrt_pair_whr5 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
 Make an application of function symbol @sqrt_pair_whr5.
 
bool is_sqrt_pair_whr5_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair_whr5.
 
const core::identifier_stringsqrt_pair_whr6_name ()
 Generate identifier @sqrt_pair_whr6.
 
const function_symbolsqrt_pair_whr6 ()
 Constructor for function symbol @sqrt_pair_whr6.
 
bool is_sqrt_pair_whr6_function_symbol (const atermpp::aterm &e)
 Recogniser for function @sqrt_pair_whr6.
 
application sqrt_pair_whr6 (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @sqrt_pair_whr6.
 
void make_sqrt_pair_whr6 (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @sqrt_pair_whr6.
 
bool is_sqrt_pair_whr6_application (const atermpp::aterm &e)
 Recogniser for application of @sqrt_pair_whr6.
 
const data_expressionarg5 (const data_expression &e)
 Function for projecting out argument. arg5 from an application.
 
const data_expressionarg6 (const data_expression &e)
 Function for projecting out argument. arg6 from an application.
 
template<typename T >
std::enable_if< std::is_integral< T >::value, data_expression >::type nat (T t)
 Constructs expression of type pos from an integral type.
 
data_expression nat (const std::string &n)
 Constructs expression of type Nat from a string.
 
bool is_natural_constant (const data_expression &n)
 Determines whether n is a natural constant.
 
std::string natural_constant_as_string (const data_expression &n_in)
 Return the string representation of a natural number.
 
template<class NUMERIC_TYPE >
NUMERIC_TYPE natural_constant_to_value (const data_expression &n)
 Return the NUMERIC_VALUE representation of a natural number.
 

Detailed Description

Namespace for system defined sort nat.

Typedef Documentation

◆ implementation_map

typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > mcrl2::data::sort_nat::implementation_map

Definition at line 277 of file nat1.h.

Function Documentation

◆ add_with_carry() [1/2]

application mcrl2::data::sort_nat::add_with_carry ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @add_with_carry.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @add_with_carry to a number of arguments.

Definition at line 1221 of file nat64.h.

◆ add_with_carry() [2/2]

function_symbol mcrl2::data::sort_nat::add_with_carry ( const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 1181 of file nat64.h.

◆ add_with_carry_name()

const core::identifier_string & mcrl2::data::sort_nat::add_with_carry_name ( )
inline

Generate identifier @add_with_carry.

Returns
Identifier @add_with_carry.

Definition at line 1173 of file nat64.h.

◆ arg()

const data_expression & mcrl2::data::sort_nat::arg ( const data_expression e)
inline

Function for projecting out argument. arg from an application.

Parameters
eA data expression.
Precondition
arg is defined for e.
Returns
The argument of e that corresponds to arg.

Definition at line 2209 of file nat1.h.

◆ arg1()

const data_expression & mcrl2::data::sort_nat::arg1 ( const data_expression e)
inline

Function for projecting out argument. arg1 from an application.

Parameters
eA data expression.
Precondition
arg1 is defined for e.
Returns
The argument of e that corresponds to arg1.

Definition at line 2221 of file nat1.h.

◆ arg2()

const data_expression & mcrl2::data::sort_nat::arg2 ( const data_expression e)
inline

Function for projecting out argument. arg2 from an application.

Parameters
eA data expression.
Precondition
arg2 is defined for e.
Returns
The argument of e that corresponds to arg2.

Definition at line 2233 of file nat1.h.

◆ arg3()

const data_expression & mcrl2::data::sort_nat::arg3 ( const data_expression e)
inline

Function for projecting out argument. arg3 from an application.

Parameters
eA data expression.
Precondition
arg3 is defined for e.
Returns
The argument of e that corresponds to arg3.

Definition at line 2269 of file nat1.h.

◆ arg4()

const data_expression & mcrl2::data::sort_nat::arg4 ( const data_expression e)
inline

Function for projecting out argument. arg4 from an application.

Parameters
eA data expression.
Precondition
arg4 is defined for e.
Returns
The argument of e that corresponds to arg4.

Definition at line 2281 of file nat1.h.

◆ arg5()

const data_expression & mcrl2::data::sort_nat::arg5 ( const data_expression e)
inline

Function for projecting out argument. arg5 from an application.

Parameters
eA data expression.
Precondition
arg5 is defined for e.
Returns
The argument of e that corresponds to arg5.

Definition at line 4816 of file nat64.h.

◆ arg6()

const data_expression & mcrl2::data::sort_nat::arg6 ( const data_expression e)
inline

Function for projecting out argument. arg6 from an application.

Parameters
eA data expression.
Precondition
arg6 is defined for e.
Returns
The argument of e that corresponds to arg6.

Definition at line 4828 of file nat64.h.

◆ auxiliary_plus_nat() [1/2]

const function_symbol & mcrl2::data::sort_nat::auxiliary_plus_nat ( )
inline

Constructor for function symbol @plus_nat.

Returns
Function symbol auxiliary_plus_nat.

Definition at line 1260 of file nat64.h.

◆ auxiliary_plus_nat() [2/2]

application mcrl2::data::sort_nat::auxiliary_plus_nat ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @plus_nat.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @plus_nat to a number of arguments.

Definition at line 1285 of file nat64.h.

◆ auxiliary_plus_nat_name()

const core::identifier_string & mcrl2::data::sort_nat::auxiliary_plus_nat_name ( )
inline

Generate identifier @plus_nat.

Returns
Identifier @plus_nat.

Definition at line 1250 of file nat64.h.

◆ c0()

const function_symbol & mcrl2::data::sort_nat::c0 ( )
inline

Constructor for function symbol @c0.

Returns
Function symbol c0.

Definition at line 108 of file nat1.h.

◆ c0_name()

const core::identifier_string & mcrl2::data::sort_nat::c0_name ( )
inline

Generate identifier @c0.

Returns
Identifier @c0.

Definition at line 98 of file nat1.h.

◆ cnat() [1/2]

const function_symbol & mcrl2::data::sort_nat::cnat ( )
inline

Constructor for function symbol @cNat.

Returns
Function symbol cnat.

Definition at line 140 of file nat1.h.

◆ cnat() [2/2]

application mcrl2::data::sort_nat::cnat ( const data_expression arg0)
inline

Application of function symbol @cNat.

Parameters
arg0A data expression.
Returns
Application of @cNat to a number of arguments.

Definition at line 164 of file nat1.h.

◆ cnat_name()

const core::identifier_string & mcrl2::data::sort_nat::cnat_name ( )
inline

Generate identifier @cNat.

Returns
Identifier @cNat.

Definition at line 130 of file nat1.h.

◆ concat_digit() [1/2]

application mcrl2::data::sort_nat::concat_digit ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @concat_digit.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @concat_digit to a number of arguments.

Definition at line 401 of file nat64.h.

◆ concat_digit() [2/2]

function_symbol mcrl2::data::sort_nat::concat_digit ( const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 361 of file nat64.h.

◆ concat_digit_name()

const core::identifier_string & mcrl2::data::sort_nat::concat_digit_name ( )
inline

Generate identifier @concat_digit.

Returns
Identifier @concat_digit.

Definition at line 353 of file nat64.h.

◆ cpair() [1/2]

const function_symbol & mcrl2::data::sort_nat::cpair ( )
inline

Constructor for function symbol @cPair.

Returns
Function symbol cpair.

Definition at line 202 of file nat1.h.

◆ cpair() [2/2]

application mcrl2::data::sort_nat::cpair ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @cPair.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @cPair to a number of arguments.

Definition at line 227 of file nat1.h.

◆ cpair_name()

const core::identifier_string & mcrl2::data::sort_nat::cpair_name ( )
inline

Generate identifier @cPair.

Returns
Identifier @cPair.

Definition at line 192 of file nat1.h.

◆ div() [1/2]

const function_symbol & mcrl2::data::sort_nat::div ( )
inline

Constructor for function symbol div.

Returns
Function symbol div.

Definition at line 1064 of file nat1.h.

◆ div() [2/2]

application mcrl2::data::sort_nat::div ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol div.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of div to a number of arguments.

Definition at line 1089 of file nat1.h.

◆ div2() [1/2]

const function_symbol & mcrl2::data::sort_nat::div2 ( )
inline

Constructor for function symbol @div2.

Returns
Function symbol div2.

Definition at line 1948 of file nat64.h.

◆ div2() [2/2]

application mcrl2::data::sort_nat::div2 ( const data_expression arg0)
inline

Application of function symbol @div2.

Parameters
arg0A data expression.
Returns
Application of @div2 to a number of arguments.

Definition at line 1972 of file nat64.h.

◆ div2_name()

const core::identifier_string & mcrl2::data::sort_nat::div2_name ( )
inline

Generate identifier @div2.

Returns
Identifier @div2.

Definition at line 1938 of file nat64.h.

◆ div_bold() [1/2]

const function_symbol & mcrl2::data::sort_nat::div_bold ( )
inline

Constructor for function symbol @div_bold.

Returns
Function symbol div_bold.

Definition at line 2676 of file nat64.h.

◆ div_bold() [2/2]

application mcrl2::data::sort_nat::div_bold ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @div_bold.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @div_bold to a number of arguments.

Definition at line 2701 of file nat64.h.

◆ div_bold_name()

const core::identifier_string & mcrl2::data::sort_nat::div_bold_name ( )
inline

Generate identifier @div_bold.

Returns
Identifier @div_bold.

Definition at line 2666 of file nat64.h.

◆ div_bold_whr() [1/2]

const function_symbol & mcrl2::data::sort_nat::div_bold_whr ( )
inline

Constructor for function symbol @div_bold_whr.

Returns
Function symbol div_bold_whr.

Definition at line 2740 of file nat64.h.

◆ div_bold_whr() [2/2]

application mcrl2::data::sort_nat::div_bold_whr ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4,
const data_expression arg5 
)
inline

Application of function symbol @div_bold_whr.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
arg5A data expression.
Returns
Application of @div_bold_whr to a number of arguments.

Definition at line 2769 of file nat64.h.

◆ div_bold_whr_name()

const core::identifier_string & mcrl2::data::sort_nat::div_bold_whr_name ( )
inline

Generate identifier @div_bold_whr.

Returns
Identifier @div_bold_whr.

Definition at line 2730 of file nat64.h.

◆ div_name()

const core::identifier_string & mcrl2::data::sort_nat::div_name ( )
inline

Generate identifier div.

Returns
Identifier div.

Definition at line 1054 of file nat1.h.

◆ div_whr1() [1/2]

const function_symbol & mcrl2::data::sort_nat::div_whr1 ( )
inline

Constructor for function symbol @div_whr1.

Returns
Function symbol div_whr1.

Definition at line 2812 of file nat64.h.

◆ div_whr1() [2/2]

application mcrl2::data::sort_nat::div_whr1 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @div_whr1.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @div_whr1 to a number of arguments.

Definition at line 2839 of file nat64.h.

◆ div_whr1_name()

const core::identifier_string & mcrl2::data::sort_nat::div_whr1_name ( )
inline

Generate identifier @div_whr1.

Returns
Identifier @div_whr1.

Definition at line 2802 of file nat64.h.

◆ div_whr2() [1/2]

const function_symbol & mcrl2::data::sort_nat::div_whr2 ( )
inline

Constructor for function symbol @div_whr2.

Returns
Function symbol div_whr2.

Definition at line 2880 of file nat64.h.

◆ div_whr2() [2/2]

application mcrl2::data::sort_nat::div_whr2 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Application of function symbol @div_whr2.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
Returns
Application of @div_whr2 to a number of arguments.

Definition at line 2908 of file nat64.h.

◆ div_whr2_name()

const core::identifier_string & mcrl2::data::sort_nat::div_whr2_name ( )
inline

Generate identifier @div_whr2.

Returns
Identifier @div_whr2.

Definition at line 2870 of file nat64.h.

◆ divmod() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod ( )
inline

Constructor for function symbol @divmod.

Returns
Function symbol divmod.

Definition at line 1915 of file nat1.h.

◆ divmod() [2/2]

application mcrl2::data::sort_nat::divmod ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @divmod.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @divmod to a number of arguments.

Definition at line 1940 of file nat1.h.

◆ divmod_aux() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux ( )
inline

Constructor for function symbol @divmod_aux.

Returns
Function symbol divmod_aux.

Definition at line 3018 of file nat64.h.

◆ divmod_aux() [2/2]

application mcrl2::data::sort_nat::divmod_aux ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @divmod_aux.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @divmod_aux to a number of arguments.

Definition at line 3043 of file nat64.h.

◆ divmod_aux_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_name ( )
inline

Generate identifier @divmod_aux.

Returns
Identifier @divmod_aux.

Definition at line 3008 of file nat64.h.

◆ divmod_aux_whr1() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux_whr1 ( )
inline

Constructor for function symbol @divmod_aux_whr1.

Returns
Function symbol divmod_aux_whr1.

Definition at line 3082 of file nat64.h.

◆ divmod_aux_whr1() [2/2]

application mcrl2::data::sort_nat::divmod_aux_whr1 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @divmod_aux_whr1.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @divmod_aux_whr1 to a number of arguments.

Definition at line 3109 of file nat64.h.

◆ divmod_aux_whr1_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_whr1_name ( )
inline

Generate identifier @divmod_aux_whr1.

Returns
Identifier @divmod_aux_whr1.

Definition at line 3072 of file nat64.h.

◆ divmod_aux_whr2() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux_whr2 ( )
inline

Constructor for function symbol @divmod_aux_whr2.

Returns
Function symbol divmod_aux_whr2.

Definition at line 3150 of file nat64.h.

◆ divmod_aux_whr2() [2/2]

application mcrl2::data::sort_nat::divmod_aux_whr2 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Application of function symbol @divmod_aux_whr2.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
Returns
Application of @divmod_aux_whr2 to a number of arguments.

Definition at line 3178 of file nat64.h.

◆ divmod_aux_whr2_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_whr2_name ( )
inline

Generate identifier @divmod_aux_whr2.

Returns
Identifier @divmod_aux_whr2.

Definition at line 3140 of file nat64.h.

◆ divmod_aux_whr3() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux_whr3 ( )
inline

Constructor for function symbol @divmod_aux_whr3.

Returns
Function symbol divmod_aux_whr3.

Definition at line 3220 of file nat64.h.

◆ divmod_aux_whr3() [2/2]

application mcrl2::data::sort_nat::divmod_aux_whr3 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Application of function symbol @divmod_aux_whr3.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
Returns
Application of @divmod_aux_whr3 to a number of arguments.

Definition at line 3248 of file nat64.h.

◆ divmod_aux_whr3_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_whr3_name ( )
inline

Generate identifier @divmod_aux_whr3.

Returns
Identifier @divmod_aux_whr3.

Definition at line 3210 of file nat64.h.

◆ divmod_aux_whr4() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux_whr4 ( )
inline

Constructor for function symbol @divmod_aux_whr4.

Returns
Function symbol divmod_aux_whr4.

Definition at line 3290 of file nat64.h.

◆ divmod_aux_whr4() [2/2]

application mcrl2::data::sort_nat::divmod_aux_whr4 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @divmod_aux_whr4.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @divmod_aux_whr4 to a number of arguments.

Definition at line 3317 of file nat64.h.

◆ divmod_aux_whr4_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_whr4_name ( )
inline

Generate identifier @divmod_aux_whr4.

Returns
Identifier @divmod_aux_whr4.

Definition at line 3280 of file nat64.h.

◆ divmod_aux_whr5() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux_whr5 ( )
inline

Constructor for function symbol @divmod_aux_whr5.

Returns
Function symbol divmod_aux_whr5.

Definition at line 3358 of file nat64.h.

◆ divmod_aux_whr5() [2/2]

application mcrl2::data::sort_nat::divmod_aux_whr5 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @divmod_aux_whr5.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @divmod_aux_whr5 to a number of arguments.

Definition at line 3385 of file nat64.h.

◆ divmod_aux_whr5_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_whr5_name ( )
inline

Generate identifier @divmod_aux_whr5.

Returns
Identifier @divmod_aux_whr5.

Definition at line 3348 of file nat64.h.

◆ divmod_aux_whr6() [1/2]

const function_symbol & mcrl2::data::sort_nat::divmod_aux_whr6 ( )
inline

Constructor for function symbol @divmod_aux_whr6.

Returns
Function symbol divmod_aux_whr6.

Definition at line 3426 of file nat64.h.

◆ divmod_aux_whr6() [2/2]

application mcrl2::data::sort_nat::divmod_aux_whr6 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Application of function symbol @divmod_aux_whr6.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
Returns
Application of @divmod_aux_whr6 to a number of arguments.

Definition at line 3454 of file nat64.h.

◆ divmod_aux_whr6_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_aux_whr6_name ( )
inline

Generate identifier @divmod_aux_whr6.

Returns
Identifier @divmod_aux_whr6.

Definition at line 3416 of file nat64.h.

◆ divmod_name()

const core::identifier_string & mcrl2::data::sort_nat::divmod_name ( )
inline

Generate identifier @divmod.

Returns
Identifier @divmod.

Definition at line 1905 of file nat1.h.

◆ doubly_generalised_divmod() [1/2]

const function_symbol & mcrl2::data::sort_nat::doubly_generalised_divmod ( )
inline

Constructor for function symbol @ggdivmod.

Returns
Function symbol doubly_generalised_divmod.

Definition at line 2045 of file nat1.h.

◆ doubly_generalised_divmod() [2/2]

application mcrl2::data::sort_nat::doubly_generalised_divmod ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @ggdivmod.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @ggdivmod to a number of arguments.

Definition at line 2071 of file nat1.h.

◆ doubly_generalised_divmod_name()

const core::identifier_string & mcrl2::data::sort_nat::doubly_generalised_divmod_name ( )
inline

Generate identifier @ggdivmod.

Returns
Identifier @ggdivmod.

Definition at line 2035 of file nat1.h.

◆ dub() [1/2]

const function_symbol & mcrl2::data::sort_nat::dub ( )
inline

Constructor for function symbol @dub.

Returns
Function symbol dub.

Definition at line 710 of file nat1.h.

◆ dub() [2/2]

application mcrl2::data::sort_nat::dub ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @dub.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @dub to a number of arguments.

Definition at line 735 of file nat1.h.

◆ dub_name()

const core::identifier_string & mcrl2::data::sort_nat::dub_name ( )
inline

Generate identifier @dub.

Returns
Identifier @dub.

Definition at line 700 of file nat1.h.

◆ dubsucc() [1/2]

const function_symbol & mcrl2::data::sort_nat::dubsucc ( )
inline

Constructor for function symbol @dubsucc.

Returns
Function symbol dubsucc.

Definition at line 774 of file nat1.h.

◆ dubsucc() [2/2]

application mcrl2::data::sort_nat::dubsucc ( const data_expression arg0)
inline

Application of function symbol @dubsucc.

Parameters
arg0A data expression.
Returns
Application of @dubsucc to a number of arguments.

Definition at line 798 of file nat1.h.

◆ dubsucc_name()

const core::identifier_string & mcrl2::data::sort_nat::dubsucc_name ( )
inline

Generate identifier @dubsucc.

Returns
Identifier @dubsucc.

Definition at line 764 of file nat1.h.

◆ equals_one() [1/2]

application mcrl2::data::sort_nat::equals_one ( const data_expression arg0)
inline

Application of function symbol @equals_one.

Parameters
arg0A data expression.
Returns
Application of @equals_one to a number of arguments.

Definition at line 588 of file nat64.h.

◆ equals_one() [2/2]

function_symbol mcrl2::data::sort_nat::equals_one ( const sort_expression s0)
inline

Definition at line 562 of file nat64.h.

◆ equals_one_name()

const core::identifier_string & mcrl2::data::sort_nat::equals_one_name ( )
inline

Generate identifier @equals_one.

Returns
Identifier @equals_one.

Definition at line 554 of file nat64.h.

◆ equals_zero() [1/2]

const function_symbol & mcrl2::data::sort_nat::equals_zero ( )
inline

Constructor for function symbol @equals_zero.

Returns
Function symbol equals_zero.

Definition at line 440 of file nat64.h.

◆ equals_zero() [2/2]

application mcrl2::data::sort_nat::equals_zero ( const data_expression arg0)
inline

Application of function symbol @equals_zero.

Parameters
arg0A data expression.
Returns
Application of @equals_zero to a number of arguments.

Definition at line 464 of file nat64.h.

◆ equals_zero_name()

const core::identifier_string & mcrl2::data::sort_nat::equals_zero_name ( )
inline

Generate identifier @equals_zero.

Returns
Identifier @equals_zero.

Definition at line 430 of file nat64.h.

◆ even() [1/2]

const function_symbol & mcrl2::data::sort_nat::even ( )
inline

Constructor for function symbol @even.

Returns
Function symbol even.

Definition at line 1269 of file nat1.h.

◆ even() [2/2]

application mcrl2::data::sort_nat::even ( const data_expression arg0)
inline

Application of function symbol @even.

Parameters
arg0A data expression.
Returns
Application of @even to a number of arguments.

Definition at line 1293 of file nat1.h.

◆ even_name()

const core::identifier_string & mcrl2::data::sort_nat::even_name ( )
inline

Generate identifier @even.

Returns
Identifier @even.

Definition at line 1259 of file nat1.h.

◆ exp() [1/2]

application mcrl2::data::sort_nat::exp ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol exp.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of exp to a number of arguments.

Definition at line 1230 of file nat1.h.

◆ exp() [2/2]

function_symbol mcrl2::data::sort_nat::exp ( const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 1190 of file nat1.h.

◆ exp_aux3n() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_aux3n ( )
inline

Constructor for function symbol @exp_aux3n.

Returns
Function symbol exp_aux3n.

Definition at line 2278 of file nat64.h.

◆ exp_aux3n() [2/2]

application mcrl2::data::sort_nat::exp_aux3n ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @exp_aux3n.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @exp_aux3n to a number of arguments.

Definition at line 2304 of file nat64.h.

◆ exp_aux3n_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_aux3n_name ( )
inline

Generate identifier @exp_aux3n.

Returns
Identifier @exp_aux3n.

Definition at line 2268 of file nat64.h.

◆ exp_aux3p() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_aux3p ( )
inline

Constructor for function symbol @exp_aux3p.

Returns
Function symbol exp_aux3p.

Definition at line 2144 of file nat64.h.

◆ exp_aux3p() [2/2]

application mcrl2::data::sort_nat::exp_aux3p ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @exp_aux3p.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @exp_aux3p to a number of arguments.

Definition at line 2170 of file nat64.h.

◆ exp_aux3p_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_aux3p_name ( )
inline

Generate identifier @exp_aux3p.

Returns
Identifier @exp_aux3p.

Definition at line 2134 of file nat64.h.

◆ exp_aux4n() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_aux4n ( )
inline

Constructor for function symbol @exp_aux4n.

Returns
Function symbol exp_aux4n.

Definition at line 2344 of file nat64.h.

◆ exp_aux4n() [2/2]

application mcrl2::data::sort_nat::exp_aux4n ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @exp_aux4n.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @exp_aux4n to a number of arguments.

Definition at line 2371 of file nat64.h.

◆ exp_aux4n_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_aux4n_name ( )
inline

Generate identifier @exp_aux4n.

Returns
Identifier @exp_aux4n.

Definition at line 2334 of file nat64.h.

◆ exp_aux4p() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_aux4p ( )
inline

Constructor for function symbol @exp_aux4p.

Returns
Function symbol exp_aux4p.

Definition at line 2210 of file nat64.h.

◆ exp_aux4p() [2/2]

application mcrl2::data::sort_nat::exp_aux4p ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @exp_aux4p.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @exp_aux4p to a number of arguments.

Definition at line 2237 of file nat64.h.

◆ exp_aux4p_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_aux4p_name ( )
inline

Generate identifier @exp_aux4p.

Returns
Identifier @exp_aux4p.

Definition at line 2200 of file nat64.h.

◆ exp_auxfalsen() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_auxfalsen ( )
inline

Constructor for function symbol @exp_auxfalsen.

Returns
Function symbol exp_auxfalsen.

Definition at line 2610 of file nat64.h.

◆ exp_auxfalsen() [2/2]

application mcrl2::data::sort_nat::exp_auxfalsen ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @exp_auxfalsen.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @exp_auxfalsen to a number of arguments.

Definition at line 2636 of file nat64.h.

◆ exp_auxfalsen_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_auxfalsen_name ( )
inline

Generate identifier @exp_auxfalsen.

Returns
Identifier @exp_auxfalsen.

Definition at line 2600 of file nat64.h.

◆ exp_auxfalsep() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_auxfalsep ( )
inline

Constructor for function symbol @exp_auxfalsep.

Returns
Function symbol exp_auxfalsep.

Definition at line 2544 of file nat64.h.

◆ exp_auxfalsep() [2/2]

application mcrl2::data::sort_nat::exp_auxfalsep ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @exp_auxfalsep.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @exp_auxfalsep to a number of arguments.

Definition at line 2570 of file nat64.h.

◆ exp_auxfalsep_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_auxfalsep_name ( )
inline

Generate identifier @exp_auxfalsep.

Returns
Identifier @exp_auxfalsep.

Definition at line 2534 of file nat64.h.

◆ exp_auxtruen() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_auxtruen ( )
inline

Constructor for function symbol @exp_auxtruen.

Returns
Function symbol exp_auxtruen.

Definition at line 2478 of file nat64.h.

◆ exp_auxtruen() [2/2]

application mcrl2::data::sort_nat::exp_auxtruen ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @exp_auxtruen.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @exp_auxtruen to a number of arguments.

Definition at line 2504 of file nat64.h.

◆ exp_auxtruen_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_auxtruen_name ( )
inline

Generate identifier @exp_auxtruen.

Returns
Identifier @exp_auxtruen.

Definition at line 2468 of file nat64.h.

◆ exp_auxtruep() [1/2]

const function_symbol & mcrl2::data::sort_nat::exp_auxtruep ( )
inline

Constructor for function symbol @exp_auxtruep.

Returns
Function symbol exp_auxtruep.

Definition at line 2412 of file nat64.h.

◆ exp_auxtruep() [2/2]

application mcrl2::data::sort_nat::exp_auxtruep ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @exp_auxtruep.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @exp_auxtruep to a number of arguments.

Definition at line 2438 of file nat64.h.

◆ exp_auxtruep_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_auxtruep_name ( )
inline

Generate identifier @exp_auxtruep.

Returns
Identifier @exp_auxtruep.

Definition at line 2402 of file nat64.h.

◆ exp_name()

const core::identifier_string & mcrl2::data::sort_nat::exp_name ( )
inline

Generate identifier exp.

Returns
Identifier exp.

Definition at line 1182 of file nat1.h.

◆ first() [1/2]

const function_symbol & mcrl2::data::sort_nat::first ( )
inline

Constructor for function symbol @first.

Returns
Function symbol first.

Definition at line 1791 of file nat1.h.

◆ first() [2/2]

application mcrl2::data::sort_nat::first ( const data_expression arg0)
inline

Application of function symbol @first.

Parameters
arg0A data expression.
Returns
Application of @first to a number of arguments.

Definition at line 1815 of file nat1.h.

◆ first_name()

const core::identifier_string & mcrl2::data::sort_nat::first_name ( )
inline

Generate identifier @first.

Returns
Identifier @first.

Definition at line 1781 of file nat1.h.

◆ generalised_divmod() [1/2]

const function_symbol & mcrl2::data::sort_nat::generalised_divmod ( )
inline

Constructor for function symbol @gdivmod.

Returns
Function symbol generalised_divmod.

Definition at line 1979 of file nat1.h.

◆ generalised_divmod() [2/2]

application mcrl2::data::sort_nat::generalised_divmod ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @gdivmod.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @gdivmod to a number of arguments.

Definition at line 2005 of file nat1.h.

◆ generalised_divmod_name()

const core::identifier_string & mcrl2::data::sort_nat::generalised_divmod_name ( )
inline

Generate identifier @gdivmod.

Returns
Identifier @gdivmod.

Definition at line 1969 of file nat1.h.

◆ gte_subtract_with_borrow() [1/2]

const function_symbol & mcrl2::data::sort_nat::gte_subtract_with_borrow ( )
inline

Constructor for function symbol @gtesubtb.

Returns
Function symbol gte_subtract_with_borrow.

Definition at line 921 of file nat1.h.

◆ gte_subtract_with_borrow() [2/2]

application mcrl2::data::sort_nat::gte_subtract_with_borrow ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @gtesubtb.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @gtesubtb to a number of arguments.

Definition at line 947 of file nat1.h.

◆ gte_subtract_with_borrow_name()

const core::identifier_string & mcrl2::data::sort_nat::gte_subtract_with_borrow_name ( )
inline

Generate identifier @gtesubtb.

Returns
Identifier @gtesubtb.

Definition at line 911 of file nat1.h.

◆ is_add_with_carry_application()

bool mcrl2::data::sort_nat::is_add_with_carry_application ( const atermpp::aterm e)
inline

Recogniser for application of @add_with_carry.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol add_with_carry to a number of arguments.

Definition at line 1242 of file nat64.h.

◆ is_add_with_carry_function_symbol()

bool mcrl2::data::sort_nat::is_add_with_carry_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @add_with_carry.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @add_with_carry.

Definition at line 1205 of file nat64.h.

◆ is_auxiliary_plus_nat_application()

bool mcrl2::data::sort_nat::is_auxiliary_plus_nat_application ( const atermpp::aterm e)
inline

Recogniser for application of @plus_nat.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol auxiliary_plus_nat to a number of arguments.

Definition at line 1306 of file nat64.h.

◆ is_auxiliary_plus_nat_function_symbol()

bool mcrl2::data::sort_nat::is_auxiliary_plus_nat_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @plus_nat.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @plus_nat.

Definition at line 1270 of file nat64.h.

◆ is_c0_function_symbol()

bool mcrl2::data::sort_nat::is_c0_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @c0.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @c0.

Definition at line 118 of file nat1.h.

◆ is_cnat_application()

bool mcrl2::data::sort_nat::is_cnat_application ( const atermpp::aterm e)
inline

Recogniser for application of @cNat.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol cnat to a number of arguments.

Definition at line 184 of file nat1.h.

◆ is_cnat_function_symbol()

bool mcrl2::data::sort_nat::is_cnat_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @cNat.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @cNat.

Definition at line 150 of file nat1.h.

◆ is_concat_digit_application()

bool mcrl2::data::sort_nat::is_concat_digit_application ( const atermpp::aterm e)
inline

Recogniser for application of @concat_digit.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol concat_digit to a number of arguments.

Definition at line 422 of file nat64.h.

◆ is_concat_digit_function_symbol()

bool mcrl2::data::sort_nat::is_concat_digit_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @concat_digit.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @concat_digit.

Definition at line 385 of file nat64.h.

◆ is_cpair_application()

bool mcrl2::data::sort_nat::is_cpair_application ( const atermpp::aterm e)
inline

Recogniser for application of @cPair.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol cpair to a number of arguments.

Definition at line 248 of file nat1.h.

◆ is_cpair_function_symbol()

bool mcrl2::data::sort_nat::is_cpair_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @cPair.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @cPair.

Definition at line 212 of file nat1.h.

◆ is_div2_application()

bool mcrl2::data::sort_nat::is_div2_application ( const atermpp::aterm e)
inline

Recogniser for application of @div2.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol div2 to a number of arguments.

Definition at line 1992 of file nat64.h.

◆ is_div2_function_symbol()

bool mcrl2::data::sort_nat::is_div2_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @div2.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @div2.

Definition at line 1958 of file nat64.h.

◆ is_div_application()

bool mcrl2::data::sort_nat::is_div_application ( const atermpp::aterm e)
inline

Recogniser for application of div.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol div to a number of arguments.

Definition at line 1110 of file nat1.h.

◆ is_div_bold_application()

bool mcrl2::data::sort_nat::is_div_bold_application ( const atermpp::aterm e)
inline

Recogniser for application of @div_bold.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol div_bold to a number of arguments.

Definition at line 2722 of file nat64.h.

◆ is_div_bold_function_symbol()

bool mcrl2::data::sort_nat::is_div_bold_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @div_bold.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @div_bold.

Definition at line 2686 of file nat64.h.

◆ is_div_bold_whr_application()

bool mcrl2::data::sort_nat::is_div_bold_whr_application ( const atermpp::aterm e)
inline

Recogniser for application of @div_bold_whr.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol div_bold_whr to a number of arguments.

Definition at line 2794 of file nat64.h.

◆ is_div_bold_whr_function_symbol()

bool mcrl2::data::sort_nat::is_div_bold_whr_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @div_bold_whr.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @div_bold_whr.

Definition at line 2750 of file nat64.h.

◆ is_div_function_symbol()

bool mcrl2::data::sort_nat::is_div_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function div.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching div.

Definition at line 1074 of file nat1.h.

◆ is_div_whr1_application()

bool mcrl2::data::sort_nat::is_div_whr1_application ( const atermpp::aterm e)
inline

Recogniser for application of @div_whr1.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol div_whr1 to a number of arguments.

Definition at line 2862 of file nat64.h.

◆ is_div_whr1_function_symbol()

bool mcrl2::data::sort_nat::is_div_whr1_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @div_whr1.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @div_whr1.

Definition at line 2822 of file nat64.h.

◆ is_div_whr2_application()

bool mcrl2::data::sort_nat::is_div_whr2_application ( const atermpp::aterm e)
inline

Recogniser for application of @div_whr2.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol div_whr2 to a number of arguments.

Definition at line 2932 of file nat64.h.

◆ is_div_whr2_function_symbol()

bool mcrl2::data::sort_nat::is_div_whr2_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @div_whr2.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @div_whr2.

Definition at line 2890 of file nat64.h.

◆ is_divmod_application()

bool mcrl2::data::sort_nat::is_divmod_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod to a number of arguments.

Definition at line 1961 of file nat1.h.

◆ is_divmod_aux_application()

bool mcrl2::data::sort_nat::is_divmod_aux_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux to a number of arguments.

Definition at line 3064 of file nat64.h.

◆ is_divmod_aux_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux.

Definition at line 3028 of file nat64.h.

◆ is_divmod_aux_whr1_application()

bool mcrl2::data::sort_nat::is_divmod_aux_whr1_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux_whr1.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux_whr1 to a number of arguments.

Definition at line 3132 of file nat64.h.

◆ is_divmod_aux_whr1_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_whr1_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux_whr1.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux_whr1.

Definition at line 3092 of file nat64.h.

◆ is_divmod_aux_whr2_application()

bool mcrl2::data::sort_nat::is_divmod_aux_whr2_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux_whr2.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux_whr2 to a number of arguments.

Definition at line 3202 of file nat64.h.

◆ is_divmod_aux_whr2_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_whr2_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux_whr2.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux_whr2.

Definition at line 3160 of file nat64.h.

◆ is_divmod_aux_whr3_application()

bool mcrl2::data::sort_nat::is_divmod_aux_whr3_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux_whr3.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux_whr3 to a number of arguments.

Definition at line 3272 of file nat64.h.

◆ is_divmod_aux_whr3_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_whr3_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux_whr3.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux_whr3.

Definition at line 3230 of file nat64.h.

◆ is_divmod_aux_whr4_application()

bool mcrl2::data::sort_nat::is_divmod_aux_whr4_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux_whr4.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux_whr4 to a number of arguments.

Definition at line 3340 of file nat64.h.

◆ is_divmod_aux_whr4_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_whr4_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux_whr4.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux_whr4.

Definition at line 3300 of file nat64.h.

◆ is_divmod_aux_whr5_application()

bool mcrl2::data::sort_nat::is_divmod_aux_whr5_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux_whr5.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux_whr5 to a number of arguments.

Definition at line 3408 of file nat64.h.

◆ is_divmod_aux_whr5_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_whr5_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux_whr5.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux_whr5.

Definition at line 3368 of file nat64.h.

◆ is_divmod_aux_whr6_application()

bool mcrl2::data::sort_nat::is_divmod_aux_whr6_application ( const atermpp::aterm e)
inline

Recogniser for application of @divmod_aux_whr6.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol divmod_aux_whr6 to a number of arguments.

Definition at line 3478 of file nat64.h.

◆ is_divmod_aux_whr6_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_aux_whr6_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod_aux_whr6.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod_aux_whr6.

Definition at line 3436 of file nat64.h.

◆ is_divmod_function_symbol()

bool mcrl2::data::sort_nat::is_divmod_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @divmod.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @divmod.

Definition at line 1925 of file nat1.h.

◆ is_doubly_generalised_divmod_application()

bool mcrl2::data::sort_nat::is_doubly_generalised_divmod_application ( const atermpp::aterm e)
inline

Recogniser for application of @ggdivmod.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol doubly_generalised_divmod to a number of arguments.

Definition at line 2093 of file nat1.h.

◆ is_doubly_generalised_divmod_function_symbol()

bool mcrl2::data::sort_nat::is_doubly_generalised_divmod_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @ggdivmod.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @ggdivmod.

Definition at line 2055 of file nat1.h.

◆ is_dub_application()

bool mcrl2::data::sort_nat::is_dub_application ( const atermpp::aterm e)
inline

Recogniser for application of @dub.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol dub to a number of arguments.

Definition at line 756 of file nat1.h.

◆ is_dub_function_symbol()

bool mcrl2::data::sort_nat::is_dub_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @dub.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @dub.

Definition at line 720 of file nat1.h.

◆ is_dubsucc_application()

bool mcrl2::data::sort_nat::is_dubsucc_application ( const atermpp::aterm e)
inline

Recogniser for application of @dubsucc.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol dubsucc to a number of arguments.

Definition at line 818 of file nat1.h.

◆ is_dubsucc_function_symbol()

bool mcrl2::data::sort_nat::is_dubsucc_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @dubsucc.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @dubsucc.

Definition at line 784 of file nat1.h.

◆ is_equals_one_application()

bool mcrl2::data::sort_nat::is_equals_one_application ( const atermpp::aterm e)
inline

Recogniser for application of @equals_one.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol equals_one to a number of arguments.

Definition at line 608 of file nat64.h.

◆ is_equals_one_function_symbol()

bool mcrl2::data::sort_nat::is_equals_one_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @equals_one.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @equals_one.

Definition at line 573 of file nat64.h.

◆ is_equals_zero_application()

bool mcrl2::data::sort_nat::is_equals_zero_application ( const atermpp::aterm e)
inline

Recogniser for application of @equals_zero.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol equals_zero to a number of arguments.

Definition at line 484 of file nat64.h.

◆ is_equals_zero_function_symbol()

bool mcrl2::data::sort_nat::is_equals_zero_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @equals_zero.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @equals_zero.

Definition at line 450 of file nat64.h.

◆ is_even_application()

bool mcrl2::data::sort_nat::is_even_application ( const atermpp::aterm e)
inline

Recogniser for application of @even.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol even to a number of arguments.

Definition at line 1313 of file nat1.h.

◆ is_even_function_symbol()

bool mcrl2::data::sort_nat::is_even_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @even.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @even.

Definition at line 1279 of file nat1.h.

◆ is_exp_application()

bool mcrl2::data::sort_nat::is_exp_application ( const atermpp::aterm e)
inline

Recogniser for application of exp.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp to a number of arguments.

Definition at line 1251 of file nat1.h.

◆ is_exp_aux3n_application()

bool mcrl2::data::sort_nat::is_exp_aux3n_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_aux3n.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_aux3n to a number of arguments.

Definition at line 2326 of file nat64.h.

◆ is_exp_aux3n_function_symbol()

bool mcrl2::data::sort_nat::is_exp_aux3n_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_aux3n.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_aux3n.

Definition at line 2288 of file nat64.h.

◆ is_exp_aux3p_application()

bool mcrl2::data::sort_nat::is_exp_aux3p_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_aux3p.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_aux3p to a number of arguments.

Definition at line 2192 of file nat64.h.

◆ is_exp_aux3p_function_symbol()

bool mcrl2::data::sort_nat::is_exp_aux3p_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_aux3p.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_aux3p.

Definition at line 2154 of file nat64.h.

◆ is_exp_aux4n_application()

bool mcrl2::data::sort_nat::is_exp_aux4n_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_aux4n.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_aux4n to a number of arguments.

Definition at line 2394 of file nat64.h.

◆ is_exp_aux4n_function_symbol()

bool mcrl2::data::sort_nat::is_exp_aux4n_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_aux4n.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_aux4n.

Definition at line 2354 of file nat64.h.

◆ is_exp_aux4p_application()

bool mcrl2::data::sort_nat::is_exp_aux4p_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_aux4p.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_aux4p to a number of arguments.

Definition at line 2260 of file nat64.h.

◆ is_exp_aux4p_function_symbol()

bool mcrl2::data::sort_nat::is_exp_aux4p_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_aux4p.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_aux4p.

Definition at line 2220 of file nat64.h.

◆ is_exp_auxfalsen_application()

bool mcrl2::data::sort_nat::is_exp_auxfalsen_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_auxfalsen.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_auxfalsen to a number of arguments.

Definition at line 2658 of file nat64.h.

◆ is_exp_auxfalsen_function_symbol()

bool mcrl2::data::sort_nat::is_exp_auxfalsen_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_auxfalsen.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_auxfalsen.

Definition at line 2620 of file nat64.h.

◆ is_exp_auxfalsep_application()

bool mcrl2::data::sort_nat::is_exp_auxfalsep_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_auxfalsep.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_auxfalsep to a number of arguments.

Definition at line 2592 of file nat64.h.

◆ is_exp_auxfalsep_function_symbol()

bool mcrl2::data::sort_nat::is_exp_auxfalsep_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_auxfalsep.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_auxfalsep.

Definition at line 2554 of file nat64.h.

◆ is_exp_auxtruen_application()

bool mcrl2::data::sort_nat::is_exp_auxtruen_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_auxtruen.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_auxtruen to a number of arguments.

Definition at line 2526 of file nat64.h.

◆ is_exp_auxtruen_function_symbol()

bool mcrl2::data::sort_nat::is_exp_auxtruen_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_auxtruen.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_auxtruen.

Definition at line 2488 of file nat64.h.

◆ is_exp_auxtruep_application()

bool mcrl2::data::sort_nat::is_exp_auxtruep_application ( const atermpp::aterm e)
inline

Recogniser for application of @exp_auxtruep.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol exp_auxtruep to a number of arguments.

Definition at line 2460 of file nat64.h.

◆ is_exp_auxtruep_function_symbol()

bool mcrl2::data::sort_nat::is_exp_auxtruep_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @exp_auxtruep.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @exp_auxtruep.

Definition at line 2422 of file nat64.h.

◆ is_exp_function_symbol()

bool mcrl2::data::sort_nat::is_exp_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function exp.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching exp.

Definition at line 1214 of file nat1.h.

◆ is_first_application()

bool mcrl2::data::sort_nat::is_first_application ( const atermpp::aterm e)
inline

Recogniser for application of @first.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol first to a number of arguments.

Definition at line 1835 of file nat1.h.

◆ is_first_function_symbol()

bool mcrl2::data::sort_nat::is_first_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @first.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @first.

Definition at line 1801 of file nat1.h.

◆ is_generalised_divmod_application()

bool mcrl2::data::sort_nat::is_generalised_divmod_application ( const atermpp::aterm e)
inline

Recogniser for application of @gdivmod.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol generalised_divmod to a number of arguments.

Definition at line 2027 of file nat1.h.

◆ is_generalised_divmod_function_symbol()

bool mcrl2::data::sort_nat::is_generalised_divmod_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @gdivmod.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @gdivmod.

Definition at line 1989 of file nat1.h.

◆ is_gte_subtract_with_borrow_application()

bool mcrl2::data::sort_nat::is_gte_subtract_with_borrow_application ( const atermpp::aterm e)
inline

Recogniser for application of @gtesubtb.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol gte_subtract_with_borrow to a number of arguments.

Definition at line 969 of file nat1.h.

◆ is_gte_subtract_with_borrow_function_symbol()

bool mcrl2::data::sort_nat::is_gte_subtract_with_borrow_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @gtesubtb.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @gtesubtb.

Definition at line 931 of file nat1.h.

◆ is_is_odd_application()

bool mcrl2::data::sort_nat::is_is_odd_application ( const atermpp::aterm e)
inline

Recogniser for application of @is_odd.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol is_odd to a number of arguments.

Definition at line 1930 of file nat64.h.

◆ is_is_odd_function_symbol()

bool mcrl2::data::sort_nat::is_is_odd_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @is_odd.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @is_odd.

Definition at line 1896 of file nat64.h.

◆ is_last_application()

bool mcrl2::data::sort_nat::is_last_application ( const atermpp::aterm e)
inline

Recogniser for application of @last.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol last to a number of arguments.

Definition at line 1897 of file nat1.h.

◆ is_last_function_symbol()

bool mcrl2::data::sort_nat::is_last_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @last.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @last.

Definition at line 1863 of file nat1.h.

◆ is_maximum_application()

bool mcrl2::data::sort_nat::is_maximum_application ( const atermpp::aterm e)
inline

Recogniser for application of max.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol maximum to a number of arguments.

Definition at line 491 of file nat1.h.

◆ is_maximum_function_symbol()

bool mcrl2::data::sort_nat::is_maximum_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function max.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching max.

Definition at line 454 of file nat1.h.

◆ is_minimum_application()

bool mcrl2::data::sort_nat::is_minimum_application ( const atermpp::aterm e)
inline

Recogniser for application of min.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol minimum to a number of arguments.

Definition at line 568 of file nat1.h.

◆ is_minimum_function_symbol()

bool mcrl2::data::sort_nat::is_minimum_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function min.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching min.

Definition at line 531 of file nat1.h.

◆ is_mod_application()

bool mcrl2::data::sort_nat::is_mod_application ( const atermpp::aterm e)
inline

Recogniser for application of mod.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol mod to a number of arguments.

Definition at line 1174 of file nat1.h.

◆ is_mod_function_symbol()

bool mcrl2::data::sort_nat::is_mod_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function mod.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching mod.

Definition at line 1138 of file nat1.h.

◆ is_mod_whr1_application()

bool mcrl2::data::sort_nat::is_mod_whr1_application ( const atermpp::aterm e)
inline

Recogniser for application of @mod_whr1.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol mod_whr1 to a number of arguments.

Definition at line 3000 of file nat64.h.

◆ is_mod_whr1_function_symbol()

bool mcrl2::data::sort_nat::is_mod_whr1_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @mod_whr1.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @mod_whr1.

Definition at line 2960 of file nat64.h.

◆ is_monus_application()

bool mcrl2::data::sort_nat::is_monus_application ( const atermpp::aterm e)
inline

Recogniser for application of @monus.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol monus to a number of arguments.

Definition at line 1377 of file nat1.h.

◆ is_monus_function_symbol()

bool mcrl2::data::sort_nat::is_monus_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @monus.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @monus.

Definition at line 1341 of file nat1.h.

◆ is_monus_whr_application()

bool mcrl2::data::sort_nat::is_monus_whr_application ( const atermpp::aterm e)
inline

Recogniser for application of @monus_whr.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol monus_whr to a number of arguments.

Definition at line 2126 of file nat64.h.

◆ is_monus_whr_function_symbol()

bool mcrl2::data::sort_nat::is_monus_whr_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @monus_whr.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @monus_whr.

Definition at line 2084 of file nat64.h.

◆ is_most_significant_digit_nat_application()

bool mcrl2::data::sort_nat::is_most_significant_digit_nat_application ( const atermpp::aterm e)
inline

Recogniser for application of @most_significant_digitNat.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol most_significant_digit_nat to a number of arguments.

Definition at line 345 of file nat64.h.

◆ is_most_significant_digit_nat_function_symbol()

bool mcrl2::data::sort_nat::is_most_significant_digit_nat_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @most_significant_digitNat.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @most_significant_digitNat.

Definition at line 311 of file nat64.h.

◆ is_msd_application()

bool mcrl2::data::sort_nat::is_msd_application ( const atermpp::aterm e)
inline

Recogniser for application of @msd.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol msd to a number of arguments.

Definition at line 3540 of file nat64.h.

◆ is_msd_function_symbol()

bool mcrl2::data::sort_nat::is_msd_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @msd.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @msd.

Definition at line 3506 of file nat64.h.

◆ is_nat()

bool mcrl2::data::sort_nat::is_nat ( const sort_expression e)
inline

Recogniser for sort expression Nat.

Parameters
eA sort expression
Returns
true iff e == nat()

Definition at line 56 of file nat1.h.

◆ is_nat2pos_application()

bool mcrl2::data::sort_nat::is_nat2pos_application ( const atermpp::aterm e)
inline

Recogniser for application of Nat2Pos.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol nat2pos to a number of arguments.

Definition at line 406 of file nat1.h.

◆ is_nat2pos_function_symbol()

bool mcrl2::data::sort_nat::is_nat2pos_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function Nat2Pos.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching Nat2Pos.

Definition at line 372 of file nat1.h.

◆ is_natnatpair()

bool mcrl2::data::sort_nat::is_natnatpair ( const sort_expression e)
inline

Recogniser for sort expression @NatNatPair.

Parameters
eA sort expression
Returns
true iff e == natnatpair()

Definition at line 86 of file nat64.h.

◆ is_natpair()

bool mcrl2::data::sort_nat::is_natpair ( const sort_expression e)
inline

Recogniser for sort expression @NatPair.

Parameters
eA sort expression
Returns
true iff e == natpair()

Definition at line 85 of file nat1.h.

◆ is_natpred_application()

bool mcrl2::data::sort_nat::is_natpred_application ( const atermpp::aterm e)
inline

Recogniser for application of @natpred.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol natpred to a number of arguments.

Definition at line 1868 of file nat64.h.

◆ is_natpred_function_symbol()

bool mcrl2::data::sort_nat::is_natpred_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @natpred.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @natpred.

Definition at line 1834 of file nat64.h.

◆ is_natural_constant()

bool mcrl2::data::sort_nat::is_natural_constant ( const data_expression n)
inline

Determines whether n is a natural constant.

Parameters
nA data expression

Definition at line 531 of file standard_numbers_utility.h.

◆ is_nnpair_application()

bool mcrl2::data::sort_nat::is_nnpair_application ( const atermpp::aterm e)
inline

Recogniser for application of @nnPair.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol nnpair to a number of arguments.

Definition at line 249 of file nat64.h.

◆ is_nnpair_function_symbol()

bool mcrl2::data::sort_nat::is_nnpair_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @nnPair.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @nnPair.

Definition at line 213 of file nat64.h.

◆ is_not_equals_zero_application()

bool mcrl2::data::sort_nat::is_not_equals_zero_application ( const atermpp::aterm e)
inline

Recogniser for application of @not_equals_zero.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol not_equals_zero to a number of arguments.

Definition at line 546 of file nat64.h.

◆ is_not_equals_zero_function_symbol()

bool mcrl2::data::sort_nat::is_not_equals_zero_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @not_equals_zero.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @not_equals_zero.

Definition at line 512 of file nat64.h.

◆ is_odd() [1/2]

const function_symbol & mcrl2::data::sort_nat::is_odd ( )
inline

Constructor for function symbol @is_odd.

Returns
Function symbol is_odd.

Definition at line 1886 of file nat64.h.

◆ is_odd() [2/2]

application mcrl2::data::sort_nat::is_odd ( const data_expression arg0)
inline

Application of function symbol @is_odd.

Parameters
arg0A data expression.
Returns
Application of @is_odd to a number of arguments.

Definition at line 1910 of file nat64.h.

◆ is_odd_name()

const core::identifier_string & mcrl2::data::sort_nat::is_odd_name ( )
inline

Generate identifier @is_odd.

Returns
Identifier @is_odd.

Definition at line 1876 of file nat64.h.

◆ is_plus_application()

bool mcrl2::data::sort_nat::is_plus_application ( const atermpp::aterm e)
inline

Recogniser for application of +.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol plus to a number of arguments.

Definition at line 903 of file nat1.h.

◆ is_plus_function_symbol()

bool mcrl2::data::sort_nat::is_plus_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function +.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching +.

Definition at line 866 of file nat1.h.

◆ is_pos2nat_application()

bool mcrl2::data::sort_nat::is_pos2nat_application ( const atermpp::aterm e)
inline

Recogniser for application of Pos2Nat.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol pos2nat to a number of arguments.

Definition at line 344 of file nat1.h.

◆ is_pos2nat_function_symbol()

bool mcrl2::data::sort_nat::is_pos2nat_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function Pos2Nat.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching Pos2Nat.

Definition at line 310 of file nat1.h.

◆ is_pred_application()

bool mcrl2::data::sort_nat::is_pred_application ( const atermpp::aterm e)
inline

Recogniser for application of pred.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol pred to a number of arguments.

Definition at line 692 of file nat1.h.

◆ is_pred_function_symbol()

bool mcrl2::data::sort_nat::is_pred_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function pred.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching pred.

Definition at line 658 of file nat1.h.

◆ is_pred_whr_application()

bool mcrl2::data::sort_nat::is_pred_whr_application ( const atermpp::aterm e)
inline

Recogniser for application of @pred_whr.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol pred_whr to a number of arguments.

Definition at line 1080 of file nat64.h.

◆ is_pred_whr_function_symbol()

bool mcrl2::data::sort_nat::is_pred_whr_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @pred_whr.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @pred_whr.

Definition at line 1046 of file nat64.h.

◆ is_sqrt_application()

bool mcrl2::data::sort_nat::is_sqrt_application ( const atermpp::aterm e)
inline

Recogniser for application of sqrt.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt to a number of arguments.

Definition at line 1707 of file nat1.h.

◆ is_sqrt_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function sqrt.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching sqrt.

Definition at line 1673 of file nat1.h.

◆ is_sqrt_nat_aux_func_application()

bool mcrl2::data::sort_nat::is_sqrt_nat_aux_func_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_nat.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_nat_aux_func to a number of arguments.

Definition at line 1773 of file nat1.h.

◆ is_sqrt_nat_aux_func_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_nat_aux_func_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_nat.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_nat.

Definition at line 1735 of file nat1.h.

◆ is_sqrt_pair_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair to a number of arguments.

Definition at line 4008 of file nat64.h.

◆ is_sqrt_pair_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair.

Definition at line 3974 of file nat64.h.

◆ is_sqrt_pair_whr1_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr1_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair_whr1.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair_whr1 to a number of arguments.

Definition at line 4076 of file nat64.h.

◆ is_sqrt_pair_whr1_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr1_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair_whr1.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair_whr1.

Definition at line 4036 of file nat64.h.

◆ is_sqrt_pair_whr2_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr2_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair_whr2.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair_whr2 to a number of arguments.

Definition at line 4146 of file nat64.h.

◆ is_sqrt_pair_whr2_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr2_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair_whr2.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair_whr2.

Definition at line 4104 of file nat64.h.

◆ is_sqrt_pair_whr3_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr3_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair_whr3.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair_whr3 to a number of arguments.

Definition at line 4212 of file nat64.h.

◆ is_sqrt_pair_whr3_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr3_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair_whr3.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair_whr3.

Definition at line 4174 of file nat64.h.

◆ is_sqrt_pair_whr4_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr4_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair_whr4.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair_whr4 to a number of arguments.

Definition at line 4284 of file nat64.h.

◆ is_sqrt_pair_whr4_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr4_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair_whr4.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair_whr4.

Definition at line 4240 of file nat64.h.

◆ is_sqrt_pair_whr5_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr5_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair_whr5.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair_whr5 to a number of arguments.

Definition at line 4354 of file nat64.h.

◆ is_sqrt_pair_whr5_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr5_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair_whr5.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair_whr5.

Definition at line 4312 of file nat64.h.

◆ is_sqrt_pair_whr6_application()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr6_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_pair_whr6.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_pair_whr6 to a number of arguments.

Definition at line 4420 of file nat64.h.

◆ is_sqrt_pair_whr6_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_pair_whr6_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_pair_whr6.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_pair_whr6.

Definition at line 4382 of file nat64.h.

◆ is_sqrt_whr1_application()

bool mcrl2::data::sort_nat::is_sqrt_whr1_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_whr1.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_whr1 to a number of arguments.

Definition at line 3876 of file nat64.h.

◆ is_sqrt_whr1_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_whr1_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_whr1.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_whr1.

Definition at line 3836 of file nat64.h.

◆ is_sqrt_whr2_application()

bool mcrl2::data::sort_nat::is_sqrt_whr2_application ( const atermpp::aterm e)
inline

Recogniser for application of @sqrt_whr2.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol sqrt_whr2 to a number of arguments.

Definition at line 3946 of file nat64.h.

◆ is_sqrt_whr2_function_symbol()

bool mcrl2::data::sort_nat::is_sqrt_whr2_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @sqrt_whr2.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @sqrt_whr2.

Definition at line 3904 of file nat64.h.

◆ is_succ_application()

bool mcrl2::data::sort_nat::is_succ_application ( const atermpp::aterm e)
inline

Recogniser for application of succ.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol succ to a number of arguments.

Definition at line 630 of file nat1.h.

◆ is_succ_function_symbol()

bool mcrl2::data::sort_nat::is_succ_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function succ.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching succ.

Definition at line 595 of file nat1.h.

◆ is_succ_nat_application()

bool mcrl2::data::sort_nat::is_succ_nat_application ( const atermpp::aterm e)
inline

Recogniser for application of @succ_nat.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol succ_nat to a number of arguments.

Definition at line 185 of file nat64.h.

◆ is_succ_nat_function_symbol()

bool mcrl2::data::sort_nat::is_succ_nat_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @succ_nat.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @succ_nat.

Definition at line 151 of file nat64.h.

◆ is_swap_zero_add_application()

bool mcrl2::data::sort_nat::is_swap_zero_add_application ( const atermpp::aterm e)
inline

Recogniser for application of @swap_zero_add.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol swap_zero_add to a number of arguments.

Definition at line 1509 of file nat1.h.

◆ is_swap_zero_add_function_symbol()

bool mcrl2::data::sort_nat::is_swap_zero_add_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @swap_zero_add.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @swap_zero_add.

Definition at line 1469 of file nat1.h.

◆ is_swap_zero_application()

bool mcrl2::data::sort_nat::is_swap_zero_application ( const atermpp::aterm e)
inline

Recogniser for application of @swap_zero.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol swap_zero to a number of arguments.

Definition at line 1441 of file nat1.h.

◆ is_swap_zero_function_symbol()

bool mcrl2::data::sort_nat::is_swap_zero_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @swap_zero.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @swap_zero.

Definition at line 1405 of file nat1.h.

◆ is_swap_zero_min_application()

bool mcrl2::data::sort_nat::is_swap_zero_min_application ( const atermpp::aterm e)
inline

Recogniser for application of @swap_zero_min.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol swap_zero_min to a number of arguments.

Definition at line 1577 of file nat1.h.

◆ is_swap_zero_min_function_symbol()

bool mcrl2::data::sort_nat::is_swap_zero_min_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @swap_zero_min.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @swap_zero_min.

Definition at line 1537 of file nat1.h.

◆ is_swap_zero_monus_application()

bool mcrl2::data::sort_nat::is_swap_zero_monus_application ( const atermpp::aterm e)
inline

Recogniser for application of @swap_zero_monus.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol swap_zero_monus to a number of arguments.

Definition at line 1645 of file nat1.h.

◆ is_swap_zero_monus_function_symbol()

bool mcrl2::data::sort_nat::is_swap_zero_monus_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @swap_zero_monus.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @swap_zero_monus.

Definition at line 1605 of file nat1.h.

◆ is_times_application()

bool mcrl2::data::sort_nat::is_times_application ( const atermpp::aterm e)
inline

Recogniser for application of *.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol times to a number of arguments.

Definition at line 1046 of file nat1.h.

◆ is_times_function_symbol()

bool mcrl2::data::sort_nat::is_times_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function *.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching *.

Definition at line 1009 of file nat1.h.

◆ is_times_ordered_application()

bool mcrl2::data::sort_nat::is_times_ordered_application ( const atermpp::aterm e)
inline

Recogniser for application of @times_ordered.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol times_ordered to a number of arguments.

Definition at line 1460 of file nat64.h.

◆ is_times_ordered_function_symbol()

bool mcrl2::data::sort_nat::is_times_ordered_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @times_ordered.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @times_ordered.

Definition at line 1423 of file nat64.h.

◆ is_times_overflow_application()

bool mcrl2::data::sort_nat::is_times_overflow_application ( const atermpp::aterm e)
inline

Recogniser for application of @times_overflow.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol times_overflow to a number of arguments.

Definition at line 1539 of file nat64.h.

◆ is_times_overflow_function_symbol()

bool mcrl2::data::sort_nat::is_times_overflow_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @times_overflow.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @times_overflow.

Definition at line 1500 of file nat64.h.

◆ last() [1/2]

const function_symbol & mcrl2::data::sort_nat::last ( )
inline

Constructor for function symbol @last.

Returns
Function symbol last.

Definition at line 1853 of file nat1.h.

◆ last() [2/2]

application mcrl2::data::sort_nat::last ( const data_expression arg0)
inline

Application of function symbol @last.

Parameters
arg0A data expression.
Returns
Application of @last to a number of arguments.

Definition at line 1877 of file nat1.h.

◆ last_name()

const core::identifier_string & mcrl2::data::sort_nat::last_name ( )
inline

Generate identifier @last.

Returns
Identifier @last.

Definition at line 1843 of file nat1.h.

◆ left()

const data_expression & mcrl2::data::sort_nat::left ( const data_expression e)
inline

Function for projecting out argument. left from an application.

Parameters
eA data expression.
Precondition
left is defined for e.
Returns
The argument of e that corresponds to left.

Definition at line 2245 of file nat1.h.

◆ make_add_with_carry()

void mcrl2::data::sort_nat::make_add_with_carry ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @add_with_carry.

Parameters
resultThe data expression where the @add_with_carry expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1232 of file nat64.h.

◆ make_auxiliary_plus_nat()

void mcrl2::data::sort_nat::make_auxiliary_plus_nat ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @plus_nat.

Parameters
resultThe data expression where the @plus_nat expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1296 of file nat64.h.

◆ make_cnat()

void mcrl2::data::sort_nat::make_cnat ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @cNat.

Parameters
resultThe data expression where the @cNat expression is put.
arg0A data expression.

Definition at line 174 of file nat1.h.

◆ make_concat_digit()

void mcrl2::data::sort_nat::make_concat_digit ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @concat_digit.

Parameters
resultThe data expression where the @concat_digit expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 412 of file nat64.h.

◆ make_cpair()

void mcrl2::data::sort_nat::make_cpair ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @cPair.

Parameters
resultThe data expression where the @cPair expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 238 of file nat1.h.

◆ make_div()

void mcrl2::data::sort_nat::make_div ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol div.

Parameters
resultThe data expression where the div expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1100 of file nat1.h.

◆ make_div2()

void mcrl2::data::sort_nat::make_div2 ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @div2.

Parameters
resultThe data expression where the @div2 expression is put.
arg0A data expression.

Definition at line 1982 of file nat64.h.

◆ make_div_bold()

void mcrl2::data::sort_nat::make_div_bold ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @div_bold.

Parameters
resultThe data expression where the @div_bold expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 2712 of file nat64.h.

◆ make_div_bold_whr()

void mcrl2::data::sort_nat::make_div_bold_whr ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4,
const data_expression arg5 
)
inline

Make an application of function symbol @div_bold_whr.

Parameters
resultThe data expression where the @div_bold_whr expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
arg5A data expression.

Definition at line 2784 of file nat64.h.

◆ make_div_whr1()

void mcrl2::data::sort_nat::make_div_whr1 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @div_whr1.

Parameters
resultThe data expression where the @div_whr1 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 2852 of file nat64.h.

◆ make_div_whr2()

void mcrl2::data::sort_nat::make_div_whr2 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @div_whr2.

Parameters
resultThe data expression where the @div_whr2 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 2922 of file nat64.h.

◆ make_divmod()

void mcrl2::data::sort_nat::make_divmod ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @divmod.

Parameters
resultThe data expression where the @divmod expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1951 of file nat1.h.

◆ make_divmod_aux()

void mcrl2::data::sort_nat::make_divmod_aux ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @divmod_aux.

Parameters
resultThe data expression where the @divmod_aux expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 3054 of file nat64.h.

◆ make_divmod_aux_whr1()

void mcrl2::data::sort_nat::make_divmod_aux_whr1 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @divmod_aux_whr1.

Parameters
resultThe data expression where the @divmod_aux_whr1 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 3122 of file nat64.h.

◆ make_divmod_aux_whr2()

void mcrl2::data::sort_nat::make_divmod_aux_whr2 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @divmod_aux_whr2.

Parameters
resultThe data expression where the @divmod_aux_whr2 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 3192 of file nat64.h.

◆ make_divmod_aux_whr3()

void mcrl2::data::sort_nat::make_divmod_aux_whr3 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @divmod_aux_whr3.

Parameters
resultThe data expression where the @divmod_aux_whr3 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 3262 of file nat64.h.

◆ make_divmod_aux_whr4()

void mcrl2::data::sort_nat::make_divmod_aux_whr4 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @divmod_aux_whr4.

Parameters
resultThe data expression where the @divmod_aux_whr4 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 3330 of file nat64.h.

◆ make_divmod_aux_whr5()

void mcrl2::data::sort_nat::make_divmod_aux_whr5 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @divmod_aux_whr5.

Parameters
resultThe data expression where the @divmod_aux_whr5 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 3398 of file nat64.h.

◆ make_divmod_aux_whr6()

void mcrl2::data::sort_nat::make_divmod_aux_whr6 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @divmod_aux_whr6.

Parameters
resultThe data expression where the @divmod_aux_whr6 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 3468 of file nat64.h.

◆ make_doubly_generalised_divmod()

void mcrl2::data::sort_nat::make_doubly_generalised_divmod ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @ggdivmod.

Parameters
resultThe data expression where the @ggdivmod expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2083 of file nat1.h.

◆ make_dub()

void mcrl2::data::sort_nat::make_dub ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @dub.

Parameters
resultThe data expression where the @dub expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 746 of file nat1.h.

◆ make_dubsucc()

void mcrl2::data::sort_nat::make_dubsucc ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @dubsucc.

Parameters
resultThe data expression where the @dubsucc expression is put.
arg0A data expression.

Definition at line 808 of file nat1.h.

◆ make_equals_one()

void mcrl2::data::sort_nat::make_equals_one ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @equals_one.

Parameters
resultThe data expression where the @equals_one expression is put.
arg0A data expression.

Definition at line 598 of file nat64.h.

◆ make_equals_zero()

void mcrl2::data::sort_nat::make_equals_zero ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @equals_zero.

Parameters
resultThe data expression where the @equals_zero expression is put.
arg0A data expression.

Definition at line 474 of file nat64.h.

◆ make_even()

void mcrl2::data::sort_nat::make_even ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @even.

Parameters
resultThe data expression where the @even expression is put.
arg0A data expression.

Definition at line 1303 of file nat1.h.

◆ make_exp()

void mcrl2::data::sort_nat::make_exp ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol exp.

Parameters
resultThe data expression where the exp expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1241 of file nat1.h.

◆ make_exp_aux3n()

void mcrl2::data::sort_nat::make_exp_aux3n ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @exp_aux3n.

Parameters
resultThe data expression where the @exp_aux3n expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2316 of file nat64.h.

◆ make_exp_aux3p()

void mcrl2::data::sort_nat::make_exp_aux3p ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @exp_aux3p.

Parameters
resultThe data expression where the @exp_aux3p expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2182 of file nat64.h.

◆ make_exp_aux4n()

void mcrl2::data::sort_nat::make_exp_aux4n ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @exp_aux4n.

Parameters
resultThe data expression where the @exp_aux4n expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 2384 of file nat64.h.

◆ make_exp_aux4p()

void mcrl2::data::sort_nat::make_exp_aux4p ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @exp_aux4p.

Parameters
resultThe data expression where the @exp_aux4p expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 2250 of file nat64.h.

◆ make_exp_auxfalsen()

void mcrl2::data::sort_nat::make_exp_auxfalsen ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @exp_auxfalsen.

Parameters
resultThe data expression where the @exp_auxfalsen expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2648 of file nat64.h.

◆ make_exp_auxfalsep()

void mcrl2::data::sort_nat::make_exp_auxfalsep ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @exp_auxfalsep.

Parameters
resultThe data expression where the @exp_auxfalsep expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2582 of file nat64.h.

◆ make_exp_auxtruen()

void mcrl2::data::sort_nat::make_exp_auxtruen ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @exp_auxtruen.

Parameters
resultThe data expression where the @exp_auxtruen expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2516 of file nat64.h.

◆ make_exp_auxtruep()

void mcrl2::data::sort_nat::make_exp_auxtruep ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @exp_auxtruep.

Parameters
resultThe data expression where the @exp_auxtruep expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2450 of file nat64.h.

◆ make_first()

void mcrl2::data::sort_nat::make_first ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @first.

Parameters
resultThe data expression where the @first expression is put.
arg0A data expression.

Definition at line 1825 of file nat1.h.

◆ make_generalised_divmod()

void mcrl2::data::sort_nat::make_generalised_divmod ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @gdivmod.

Parameters
resultThe data expression where the @gdivmod expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 2017 of file nat1.h.

◆ make_gte_subtract_with_borrow()

void mcrl2::data::sort_nat::make_gte_subtract_with_borrow ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @gtesubtb.

Parameters
resultThe data expression where the @gtesubtb expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 959 of file nat1.h.

◆ make_is_odd()

void mcrl2::data::sort_nat::make_is_odd ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @is_odd.

Parameters
resultThe data expression where the @is_odd expression is put.
arg0A data expression.

Definition at line 1920 of file nat64.h.

◆ make_last()

void mcrl2::data::sort_nat::make_last ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @last.

Parameters
resultThe data expression where the @last expression is put.
arg0A data expression.

Definition at line 1887 of file nat1.h.

◆ make_maximum()

void mcrl2::data::sort_nat::make_maximum ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol max.

Parameters
resultThe data expression where the max expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 481 of file nat1.h.

◆ make_minimum()

void mcrl2::data::sort_nat::make_minimum ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol min.

Parameters
resultThe data expression where the min expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 558 of file nat1.h.

◆ make_mod()

void mcrl2::data::sort_nat::make_mod ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol mod.

Parameters
resultThe data expression where the mod expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1164 of file nat1.h.

◆ make_mod_whr1()

void mcrl2::data::sort_nat::make_mod_whr1 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @mod_whr1.

Parameters
resultThe data expression where the @mod_whr1 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 2990 of file nat64.h.

◆ make_monus()

void mcrl2::data::sort_nat::make_monus ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @monus.

Parameters
resultThe data expression where the @monus expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1367 of file nat1.h.

◆ make_monus_whr()

void mcrl2::data::sort_nat::make_monus_whr ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @monus_whr.

Parameters
resultThe data expression where the @monus_whr expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 2116 of file nat64.h.

◆ make_most_significant_digit_nat()

void mcrl2::data::sort_nat::make_most_significant_digit_nat ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @most_significant_digitNat.

Parameters
resultThe data expression where the @most_significant_digitNat expression is put.
arg0A data expression.

Definition at line 335 of file nat64.h.

◆ make_msd()

void mcrl2::data::sort_nat::make_msd ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @msd.

Parameters
resultThe data expression where the @msd expression is put.
arg0A data expression.

Definition at line 3530 of file nat64.h.

◆ make_nat2pos()

void mcrl2::data::sort_nat::make_nat2pos ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol Nat2Pos.

Parameters
resultThe data expression where the Nat2Pos expression is put.
arg0A data expression.

Definition at line 396 of file nat1.h.

◆ make_natpred()

void mcrl2::data::sort_nat::make_natpred ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @natpred.

Parameters
resultThe data expression where the @natpred expression is put.
arg0A data expression.

Definition at line 1858 of file nat64.h.

◆ make_nnpair()

void mcrl2::data::sort_nat::make_nnpair ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @nnPair.

Parameters
resultThe data expression where the @nnPair expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 239 of file nat64.h.

◆ make_not_equals_zero()

void mcrl2::data::sort_nat::make_not_equals_zero ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @not_equals_zero.

Parameters
resultThe data expression where the @not_equals_zero expression is put.
arg0A data expression.

Definition at line 536 of file nat64.h.

◆ make_plus()

void mcrl2::data::sort_nat::make_plus ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol +.

Parameters
resultThe data expression where the + expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 893 of file nat1.h.

◆ make_pos2nat()

void mcrl2::data::sort_nat::make_pos2nat ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol Pos2Nat.

Parameters
resultThe data expression where the Pos2Nat expression is put.
arg0A data expression.

Definition at line 334 of file nat1.h.

◆ make_pred()

void mcrl2::data::sort_nat::make_pred ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol pred.

Parameters
resultThe data expression where the pred expression is put.
arg0A data expression.

Definition at line 682 of file nat1.h.

◆ make_pred_whr()

void mcrl2::data::sort_nat::make_pred_whr ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @pred_whr.

Parameters
resultThe data expression where the @pred_whr expression is put.
arg0A data expression.

Definition at line 1070 of file nat64.h.

◆ make_sqrt()

void mcrl2::data::sort_nat::make_sqrt ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol sqrt.

Parameters
resultThe data expression where the sqrt expression is put.
arg0A data expression.

Definition at line 1697 of file nat1.h.

◆ make_sqrt_nat_aux_func()

void mcrl2::data::sort_nat::make_sqrt_nat_aux_func ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @sqrt_nat.

Parameters
resultThe data expression where the @sqrt_nat expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 1763 of file nat1.h.

◆ make_sqrt_pair()

void mcrl2::data::sort_nat::make_sqrt_pair ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @sqrt_pair.

Parameters
resultThe data expression where the @sqrt_pair expression is put.
arg0A data expression.

Definition at line 3998 of file nat64.h.

◆ make_sqrt_pair_whr1()

void mcrl2::data::sort_nat::make_sqrt_pair_whr1 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @sqrt_pair_whr1.

Parameters
resultThe data expression where the @sqrt_pair_whr1 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 4066 of file nat64.h.

◆ make_sqrt_pair_whr2()

void mcrl2::data::sort_nat::make_sqrt_pair_whr2 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @sqrt_pair_whr2.

Parameters
resultThe data expression where the @sqrt_pair_whr2 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 4136 of file nat64.h.

◆ make_sqrt_pair_whr3()

void mcrl2::data::sort_nat::make_sqrt_pair_whr3 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @sqrt_pair_whr3.

Parameters
resultThe data expression where the @sqrt_pair_whr3 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 4202 of file nat64.h.

◆ make_sqrt_pair_whr4()

void mcrl2::data::sort_nat::make_sqrt_pair_whr4 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4,
const data_expression arg5 
)
inline

Make an application of function symbol @sqrt_pair_whr4.

Parameters
resultThe data expression where the @sqrt_pair_whr4 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
arg5A data expression.

Definition at line 4274 of file nat64.h.

◆ make_sqrt_pair_whr5()

void mcrl2::data::sort_nat::make_sqrt_pair_whr5 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @sqrt_pair_whr5.

Parameters
resultThe data expression where the @sqrt_pair_whr5 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 4344 of file nat64.h.

◆ make_sqrt_pair_whr6()

void mcrl2::data::sort_nat::make_sqrt_pair_whr6 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @sqrt_pair_whr6.

Parameters
resultThe data expression where the @sqrt_pair_whr6 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 4410 of file nat64.h.

◆ make_sqrt_whr1()

void mcrl2::data::sort_nat::make_sqrt_whr1 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @sqrt_whr1.

Parameters
resultThe data expression where the @sqrt_whr1 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 3866 of file nat64.h.

◆ make_sqrt_whr2()

void mcrl2::data::sort_nat::make_sqrt_whr2 ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Make an application of function symbol @sqrt_whr2.

Parameters
resultThe data expression where the @sqrt_whr2 expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.

Definition at line 3936 of file nat64.h.

◆ make_succ()

void mcrl2::data::sort_nat::make_succ ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol succ.

Parameters
resultThe data expression where the succ expression is put.
arg0A data expression.

Definition at line 620 of file nat1.h.

◆ make_succ_nat()

void mcrl2::data::sort_nat::make_succ_nat ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol @succ_nat.

Parameters
resultThe data expression where the @succ_nat expression is put.
arg0A data expression.

Definition at line 175 of file nat64.h.

◆ make_swap_zero()

void mcrl2::data::sort_nat::make_swap_zero ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @swap_zero.

Parameters
resultThe data expression where the @swap_zero expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1431 of file nat1.h.

◆ make_swap_zero_add()

void mcrl2::data::sort_nat::make_swap_zero_add ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @swap_zero_add.

Parameters
resultThe data expression where the @swap_zero_add expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1499 of file nat1.h.

◆ make_swap_zero_min()

void mcrl2::data::sort_nat::make_swap_zero_min ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @swap_zero_min.

Parameters
resultThe data expression where the @swap_zero_min expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1567 of file nat1.h.

◆ make_swap_zero_monus()

void mcrl2::data::sort_nat::make_swap_zero_monus ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Make an application of function symbol @swap_zero_monus.

Parameters
resultThe data expression where the @swap_zero_monus expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1635 of file nat1.h.

◆ make_times()

void mcrl2::data::sort_nat::make_times ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol *.

Parameters
resultThe data expression where the * expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1036 of file nat1.h.

◆ make_times_ordered()

void mcrl2::data::sort_nat::make_times_ordered ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @times_ordered.

Parameters
resultThe data expression where the @times_ordered expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 1450 of file nat64.h.

◆ make_times_overflow()

void mcrl2::data::sort_nat::make_times_overflow ( data_expression result,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @times_overflow.

Parameters
resultThe data expression where the @times_overflow expression is put.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 1529 of file nat64.h.

◆ maximum() [1/2]

application mcrl2::data::sort_nat::maximum ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol max.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of max to a number of arguments.

Definition at line 470 of file nat1.h.

◆ maximum() [2/2]

function_symbol mcrl2::data::sort_nat::maximum ( const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 422 of file nat1.h.

◆ maximum_name()

const core::identifier_string & mcrl2::data::sort_nat::maximum_name ( )
inline

Generate identifier max.

Returns
Identifier max.

Definition at line 414 of file nat1.h.

◆ minimum() [1/2]

application mcrl2::data::sort_nat::minimum ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol min.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of min to a number of arguments.

Definition at line 547 of file nat1.h.

◆ minimum() [2/2]

function_symbol mcrl2::data::sort_nat::minimum ( const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 507 of file nat1.h.

◆ minimum_name()

const core::identifier_string & mcrl2::data::sort_nat::minimum_name ( )
inline

Generate identifier min.

Returns
Identifier min.

Definition at line 499 of file nat1.h.

◆ mod() [1/2]

const function_symbol & mcrl2::data::sort_nat::mod ( )
inline

Constructor for function symbol mod.

Returns
Function symbol mod.

Definition at line 1128 of file nat1.h.

◆ mod() [2/2]

application mcrl2::data::sort_nat::mod ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol mod.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of mod to a number of arguments.

Definition at line 1153 of file nat1.h.

◆ mod_name()

const core::identifier_string & mcrl2::data::sort_nat::mod_name ( )
inline

Generate identifier mod.

Returns
Identifier mod.

Definition at line 1118 of file nat1.h.

◆ mod_whr1() [1/2]

const function_symbol & mcrl2::data::sort_nat::mod_whr1 ( )
inline

Constructor for function symbol @mod_whr1.

Returns
Function symbol mod_whr1.

Definition at line 2950 of file nat64.h.

◆ mod_whr1() [2/2]

application mcrl2::data::sort_nat::mod_whr1 ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3 
)
inline

Application of function symbol @mod_whr1.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @mod_whr1 to a number of arguments.

Definition at line 2977 of file nat64.h.

◆ mod_whr1_name()

const core::identifier_string & mcrl2::data::sort_nat::mod_whr1_name ( )
inline

Generate identifier @mod_whr1.

Returns
Identifier @mod_whr1.

Definition at line 2940 of file nat64.h.

◆ monus() [1/2]

const function_symbol & mcrl2::data::sort_nat::monus ( )
inline

Constructor for function symbol @monus.

Returns
Function symbol monus.

Definition at line 1331 of file nat1.h.

◆ monus() [2/2]

application mcrl2::data::sort_nat::monus ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @monus.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @monus to a number of arguments.

Definition at line 1356 of file nat1.h.

◆ monus_name()

const core::identifier_string & mcrl2::data::sort_nat::monus_name ( )
inline

Generate identifier @monus.

Returns
Identifier @monus.

Definition at line 1321 of file nat1.h.

◆ monus_whr() [1/2]

const function_symbol & mcrl2::data::sort_nat::monus_whr ( )
inline

Constructor for function symbol @monus_whr.

Returns
Function symbol monus_whr.

Definition at line 2074 of file nat64.h.

◆ monus_whr() [2/2]

application mcrl2::data::sort_nat::monus_whr ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2,
const data_expression arg3,
const data_expression arg4 
)
inline

Application of function symbol @monus_whr.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
arg4A data expression.
Returns
Application of @monus_whr to a number of arguments.

Definition at line 2102 of file nat64.h.

◆ monus_whr_name()

const core::identifier_string & mcrl2::data::sort_nat::monus_whr_name ( )
inline

Generate identifier @monus_whr.

Returns
Identifier @monus_whr.

Definition at line 2064 of file nat64.h.

◆ most_significant_digit_nat() [1/2]

const function_symbol & mcrl2::data::sort_nat::most_significant_digit_nat ( )
inline

Constructor for function symbol @most_significant_digitNat.

Returns
Function symbol most_significant_digit_nat.

Definition at line 301 of file nat64.h.

◆ most_significant_digit_nat() [2/2]

application mcrl2::data::sort_nat::most_significant_digit_nat ( const data_expression arg0)
inline

Application of function symbol @most_significant_digitNat.

Parameters
arg0A data expression.
Returns
Application of @most_significant_digitNat to a number of arguments.

Definition at line 325 of file nat64.h.

◆ most_significant_digit_nat_name()

const core::identifier_string & mcrl2::data::sort_nat::most_significant_digit_nat_name ( )
inline

Generate identifier @most_significant_digitNat.

Returns
Identifier @most_significant_digitNat.

Definition at line 291 of file nat64.h.

◆ msd() [1/2]

const function_symbol & mcrl2::data::sort_nat::msd ( )
inline

Constructor for function symbol @msd.

Returns
Function symbol msd.

Definition at line 3496 of file nat64.h.

◆ msd() [2/2]

application mcrl2::data::sort_nat::msd ( const data_expression arg0)
inline

Application of function symbol @msd.

Parameters
arg0A data expression.
Returns
Application of @msd to a number of arguments.

Definition at line 3520 of file nat64.h.

◆ msd_name()

const core::identifier_string & mcrl2::data::sort_nat::msd_name ( )
inline

Generate identifier @msd.

Returns
Identifier @msd.

Definition at line 3486 of file nat64.h.

◆ nat() [1/3]

const basic_sort & mcrl2::data::sort_nat::nat ( )
inline

Constructor for sort expression Nat.

Returns
Sort expression Nat.

Definition at line 46 of file nat1.h.

◆ nat() [2/3]

data_expression mcrl2::data::sort_nat::nat ( const std::string &  n)
inline

Constructs expression of type Nat from a string.

Parameters
nA string

Definition at line 499 of file standard_numbers_utility.h.

◆ nat() [3/3]

template<typename T >
std::enable_if< std::is_integral< T >::value, data_expression >::type mcrl2::data::sort_nat::nat ( t)
inline

Constructs expression of type pos from an integral type.

Definition at line 483 of file standard_numbers_utility.h.

◆ nat2pos() [1/2]

const function_symbol & mcrl2::data::sort_nat::nat2pos ( )
inline

Constructor for function symbol Nat2Pos.

Returns
Function symbol nat2pos.

Definition at line 362 of file nat1.h.

◆ nat2pos() [2/2]

application mcrl2::data::sort_nat::nat2pos ( const data_expression arg0)
inline

Application of function symbol Nat2Pos.

Parameters
arg0A data expression.
Returns
Application of Nat2Pos to a number of arguments.

Definition at line 386 of file nat1.h.

◆ nat2pos_name()

const core::identifier_string & mcrl2::data::sort_nat::nat2pos_name ( )
inline

Generate identifier Nat2Pos.

Returns
Identifier Nat2Pos.

Definition at line 352 of file nat1.h.

◆ nat_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_nat::nat_cpp_implementable_constructors ( )
inline

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for nat.

Returns
All system defined constructors that are to be implemented in C++ for nat.

Definition at line 281 of file nat1.h.

◆ nat_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_nat::nat_cpp_implementable_mappings ( )
inline

Give all system defined mappings that are to be implemented in C++ code for nat.

Returns
A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for nat

Definition at line 2198 of file nat1.h.

◆ nat_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_nat::nat_generate_constructors_and_functions_code ( )
inline

Give all system defined mappings and constructors for nat.

Returns
All system defined mappings for nat

Definition at line 2141 of file nat1.h.

◆ nat_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_nat::nat_generate_constructors_code ( )
inline

Give all system defined constructors for nat.

Returns
All system defined constructors for nat.

Definition at line 255 of file nat1.h.

◆ nat_generate_equations_code()

data_equation_vector mcrl2::data::sort_nat::nat_generate_equations_code ( )
inline

Give all system defined equations for nat.

Returns
All system defined equations for sort nat

Definition at line 2290 of file nat1.h.

◆ nat_generate_functions_code()

function_symbol_vector mcrl2::data::sort_nat::nat_generate_functions_code ( )
inline

Give all system defined mappings for nat.

Returns
All system defined mappings for nat

Definition at line 2100 of file nat1.h.

◆ nat_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_nat::nat_mCRL2_usable_constructors ( )
inline

Give all defined constructors which can be used in mCRL2 specs for nat.

Returns
All system defined constructors that can be used in an mCRL2 specification for nat.

Definition at line 267 of file nat1.h.

◆ nat_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_nat::nat_mCRL2_usable_mappings ( )
inline

Give all system defined mappings that can be used in mCRL2 specs for nat.

Returns
All system defined mappings for that can be used in mCRL2 specificationis nat

Definition at line 2154 of file nat1.h.

◆ nat_name()

const core::identifier_string & mcrl2::data::sort_nat::nat_name ( )
inline

Definition at line 37 of file nat1.h.

◆ natnatpair()

const basic_sort & mcrl2::data::sort_nat::natnatpair ( )
inline

Constructor for sort expression @NatNatPair.

Returns
Sort expression @NatNatPair.

Definition at line 76 of file nat64.h.

◆ natnatpair_name()

const core::identifier_string & mcrl2::data::sort_nat::natnatpair_name ( )
inline

Definition at line 67 of file nat64.h.

◆ natpair()

const basic_sort & mcrl2::data::sort_nat::natpair ( )
inline

Constructor for sort expression @NatPair.

Returns
Sort expression @NatPair.

Definition at line 75 of file nat1.h.

◆ natpair_name()

const core::identifier_string & mcrl2::data::sort_nat::natpair_name ( )
inline

Definition at line 66 of file nat1.h.

◆ natpred() [1/2]

const function_symbol & mcrl2::data::sort_nat::natpred ( )
inline

Constructor for function symbol @natpred.

Returns
Function symbol natpred.

Definition at line 1824 of file nat64.h.

◆ natpred() [2/2]

application mcrl2::data::sort_nat::natpred ( const data_expression arg0)
inline

Application of function symbol @natpred.

Parameters
arg0A data expression.
Returns
Application of @natpred to a number of arguments.

Definition at line 1848 of file nat64.h.

◆ natpred_name()

const core::identifier_string & mcrl2::data::sort_nat::natpred_name ( )
inline

Generate identifier @natpred.

Returns
Identifier @natpred.

Definition at line 1814 of file nat64.h.

◆ natural_constant_as_string()

std::string mcrl2::data::sort_nat::natural_constant_as_string ( const data_expression n_in)
inline

Return the string representation of a natural number.

Parameters
nA data expression
Precondition
is_natural_constant(n)
Returns
String representation of n

Definition at line 552 of file standard_numbers_utility.h.

◆ natural_constant_to_value()

template<class NUMERIC_TYPE >
NUMERIC_TYPE mcrl2::data::sort_nat::natural_constant_to_value ( const data_expression n)
inline

Return the NUMERIC_VALUE representation of a natural number.

Parameters
nA data expression
Precondition
is_natural_constant(n)
Returns
NUMERIC_VALUE representation of n

Definition at line 591 of file standard_numbers_utility.h.

◆ nnpair() [1/2]

const function_symbol & mcrl2::data::sort_nat::nnpair ( )
inline

Constructor for function symbol @nnPair.

Returns
Function symbol nnpair.

Definition at line 203 of file nat64.h.

◆ nnpair() [2/2]

application mcrl2::data::sort_nat::nnpair ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @nnPair.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of @nnPair to a number of arguments.

Definition at line 228 of file nat64.h.

◆ nnpair_name()

const core::identifier_string & mcrl2::data::sort_nat::nnpair_name ( )
inline

Generate identifier @nnPair.

Returns
Identifier @nnPair.

Definition at line 193 of file nat64.h.

◆ not_equals_zero() [1/2]

const function_symbol & mcrl2::data::sort_nat::not_equals_zero ( )
inline

Constructor for function symbol @not_equals_zero.

Returns
Function symbol not_equals_zero.

Definition at line 502 of file nat64.h.

◆ not_equals_zero() [2/2]

application mcrl2::data::sort_nat::not_equals_zero ( const data_expression arg0)
inline

Application of function symbol @not_equals_zero.

Parameters
arg0A data expression.
Returns
Application of @not_equals_zero to a number of arguments.

Definition at line 526 of file nat64.h.

◆ not_equals_zero_name()

const core::identifier_string & mcrl2::data::sort_nat::not_equals_zero_name ( )
inline

Generate identifier @not_equals_zero.

Returns
Identifier @not_equals_zero.

Definition at line 492 of file nat64.h.

◆ plus() [1/2]

application mcrl2::data::sort_nat::plus ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol +.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of + to a number of arguments.

Definition at line 882 of file nat1.h.

◆ plus() [2/2]

function_symbol mcrl2::data::sort_nat::plus ( const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 834 of file nat1.h.