Namespace for system defined sort nat. More...

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

Functions
template<typename T > requires std::is_integral_v<T>
data_expression	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.

const core::identifier_string &	nat_name ()

const basic_sort &	nat ()
	Constructor for sort expression Nat.

bool	is_nat (const sort_expression &e)
	Recogniser for sort expression Nat.

const core::identifier_string &	natpair_name ()

const basic_sort &	natpair ()
	Constructor for sort expression @NatPair.

bool	is_natpair (const sort_expression &e)
	Recogniser for sort expression @NatPair.

const core::identifier_string &	c0_name ()
	Generate identifier @c0.

const function_symbol &	c0 ()
	Constructor for function symbol @c0.

bool	is_c0_function_symbol (const atermpp::aterm &e)
	Recogniser for function @c0.

const core::identifier_string &	cnat_name ()
	Generate identifier @cNat.

const function_symbol &	cnat ()
	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_string &	cpair_name ()
	Generate identifier @cPair.

const function_symbol &	cpair ()
	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_string &	pos2nat_name ()
	Generate identifier Pos2Nat.

const function_symbol &	pos2nat ()
	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_string &	nat2pos_name ()
	Generate identifier Nat2Pos.

const function_symbol &	nat2pos ()
	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_string &	maximum_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_string &	minimum_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_string &	succ_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_string &	pred_name ()
	Generate identifier pred.

const function_symbol &	pred ()
	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_string &	dub_name ()
	Generate identifier @dub.

const function_symbol &	dub ()
	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_string &	dubsucc_name ()
	Generate identifier @dubsucc.

const function_symbol &	dubsucc ()
	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_string &	plus_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_string &	gte_subtract_with_borrow_name ()
	Generate identifier @gtesubtb.

const function_symbol &	gte_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_string &	times_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_string &	div_name ()
	Generate identifier div.

const function_symbol &	div ()
	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_string &	mod_name ()
	Generate identifier mod.

const function_symbol &	mod ()
	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_string &	exp_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_string &	even_name ()
	Generate identifier @even.

const function_symbol &	even ()
	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_string &	monus_name ()
	Generate identifier @monus.

const function_symbol &	monus ()
	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_string &	swap_zero_name ()
	Generate identifier @swap_zero.

const function_symbol &	swap_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_string &	swap_zero_add_name ()
	Generate identifier @swap_zero_add.

const function_symbol &	swap_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_string &	swap_zero_min_name ()
	Generate identifier @swap_zero_min.

const function_symbol &	swap_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_string &	swap_zero_monus_name ()
	Generate identifier @swap_zero_monus.

const function_symbol &	swap_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_string &	sqrt_name ()
	Generate identifier sqrt.

const function_symbol &	sqrt ()
	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_string &	sqrt_nat_aux_func_name ()
	Generate identifier @sqrt_nat.

const function_symbol &	sqrt_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_string &	first_name ()
	Generate identifier @first.

const function_symbol &	first ()
	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_string &	last_name ()
	Generate identifier @last.

const function_symbol &	last ()
	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_string &	divmod_name ()
	Generate identifier @divmod.

const function_symbol &	divmod ()
	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_string &	generalised_divmod_name ()
	Generate identifier @gdivmod.

const function_symbol &	generalised_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_string &	doubly_generalised_divmod_name ()
	Generate identifier @ggdivmod.

const function_symbol &	doubly_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_expression &	arg (const data_expression &e)
	Function for projecting out argument. arg from an application.

const data_expression &	arg1 (const data_expression &e)
	Function for projecting out argument. arg1 from an application.

const data_expression &	arg2 (const data_expression &e)
	Function for projecting out argument. arg2 from an application.

const data_expression &	left (const data_expression &e)
	Function for projecting out argument. left from an application.

const data_expression &	right (const data_expression &e)
	Function for projecting out argument. right from an application.

const data_expression &	arg3 (const data_expression &e)
	Function for projecting out argument. arg3 from an application.

const data_expression &	arg4 (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_string &	natnatpair_name ()

const basic_sort &	natnatpair ()
	Constructor for sort expression @NatNatPair.

bool	is_natnatpair (const sort_expression &e)
	Recogniser for sort expression @NatNatPair.

const core::identifier_string &	succ_nat_name ()
	Generate identifier @succ_nat.

const function_symbol &	succ_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_string &	nnpair_name ()
	Generate identifier @nnPair.

const function_symbol &	nnpair ()
	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_string &	most_significant_digit_nat_name ()
	Generate identifier @most_significant_digitNat.

const function_symbol &	most_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_string &	concat_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_string &	equals_zero_name ()
	Generate identifier @equals_zero.

const function_symbol &	equals_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_string &	not_equals_zero_name ()
	Generate identifier @not_equals_zero.

const function_symbol &	not_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_string &	equals_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_string &	pred_whr_name ()
	Generate identifier @pred_whr.

const function_symbol &	pred_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_string &	add_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_string &	auxiliary_plus_nat_name ()
	Generate identifier @plus_nat.

const function_symbol &	auxiliary_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_string &	times_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_string &	times_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_string &	natpred_name ()
	Generate identifier @natpred.

const function_symbol &	natpred ()
	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_string &	is_odd_name ()
	Generate identifier @is_odd.

const function_symbol &	is_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_string &	div2_name ()
	Generate identifier @div2.

const function_symbol &	div2 ()
	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_string &	monus_whr_name ()
	Generate identifier @monus_whr.

const function_symbol &	monus_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_string &	exp_aux3p_name ()
	Generate identifier @exp_aux3p.

const function_symbol &	exp_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_string &	exp_aux4p_name ()
	Generate identifier @exp_aux4p.

const function_symbol &	exp_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_string &	exp_aux3n_name ()
	Generate identifier @exp_aux3n.

const function_symbol &	exp_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_string &	exp_aux4n_name ()
	Generate identifier @exp_aux4n.

const function_symbol &	exp_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_string &	exp_auxtruep_name ()
	Generate identifier @exp_auxtruep.

const function_symbol &	exp_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_string &	exp_auxtruen_name ()
	Generate identifier @exp_auxtruen.

const function_symbol &	exp_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_string &	exp_auxfalsep_name ()
	Generate identifier @exp_auxfalsep.

const function_symbol &	exp_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_string &	exp_auxfalsen_name ()
	Generate identifier @exp_auxfalsen.

const function_symbol &	exp_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_string &	div_bold_name ()
	Generate identifier @div_bold.

const function_symbol &	div_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_string &	div_bold_whr_name ()
	Generate identifier @div_bold_whr.

const function_symbol &	div_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_string &	div_whr1_name ()
	Generate identifier @div_whr1.

const function_symbol &	div_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_string &	div_whr2_name ()
	Generate identifier @div_whr2.

const function_symbol &	div_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_string &	mod_whr1_name ()
	Generate identifier @mod_whr1.

const function_symbol &	mod_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_string &	divmod_aux_name ()
	Generate identifier @divmod_aux.

const function_symbol &	divmod_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_string &	divmod_aux_whr1_name ()
	Generate identifier @divmod_aux_whr1.

const function_symbol &	divmod_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_string &	divmod_aux_whr2_name ()
	Generate identifier @divmod_aux_whr2.

const function_symbol &	divmod_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_string &	divmod_aux_whr3_name ()
	Generate identifier @divmod_aux_whr3.

const function_symbol &	divmod_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_string &	divmod_aux_whr4_name ()
	Generate identifier @divmod_aux_whr4.

const function_symbol &	divmod_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_string &	divmod_aux_whr5_name ()
	Generate identifier @divmod_aux_whr5.

const function_symbol &	divmod_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_string &	divmod_aux_whr6_name ()
	Generate identifier @divmod_aux_whr6.

const function_symbol &	divmod_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_string &	msd_name ()
	Generate identifier @msd.

const function_symbol &	msd ()
	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_string &	sqrt_whr1_name ()
	Generate identifier @sqrt_whr1.

const function_symbol &	sqrt_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_string &	sqrt_whr2_name ()
	Generate identifier @sqrt_whr2.

const function_symbol &	sqrt_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_string &	sqrt_pair_name ()
	Generate identifier @sqrt_pair.

const function_symbol &	sqrt_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_string &	sqrt_pair_whr1_name ()
	Generate identifier @sqrt_pair_whr1.

const function_symbol &	sqrt_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_string &	sqrt_pair_whr2_name ()
	Generate identifier @sqrt_pair_whr2.

const function_symbol &	sqrt_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_string &	sqrt_pair_whr3_name ()
	Generate identifier @sqrt_pair_whr3.

const function_symbol &	sqrt_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_string &	sqrt_pair_whr4_name ()
	Generate identifier @sqrt_pair_whr4.

const function_symbol &	sqrt_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_string &	sqrt_pair_whr5_name ()
	Generate identifier @sqrt_pair_whr5.

const function_symbol &	sqrt_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_string &	sqrt_pair_whr6_name ()
	Generate identifier @sqrt_pair_whr6.

const function_symbol &	sqrt_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_expression &	arg5 (const data_expression &e)
	Function for projecting out argument. arg5 from an application.

const data_expression &	arg6 (const data_expression &e)
	Function for projecting out argument. arg6 from an application.

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 274 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @add_with_carry to a number of arguments.

Definition at line 1218 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 1178 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 1170 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

e	A data expression.

Precondition: arg is defined for e.

Returns: The argument of e that corresponds to arg.

Definition at line 2206 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

e	A data expression.

Precondition: arg1 is defined for e.

Returns: The argument of e that corresponds to arg1.

Definition at line 2218 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

e	A data expression.

Precondition: arg2 is defined for e.

Returns: The argument of e that corresponds to arg2.

Definition at line 2230 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

e	A data expression.

Precondition: arg3 is defined for e.

Returns: The argument of e that corresponds to arg3.

Definition at line 2266 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

e	A data expression.

Precondition: arg4 is defined for e.

Returns: The argument of e that corresponds to arg4.

Definition at line 2278 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

e	A data expression.

Precondition: arg5 is defined for e.

Returns: The argument of e that corresponds to arg5.

Definition at line 4813 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

e	A data expression.

Precondition: arg6 is defined for e.

Returns: The argument of e that corresponds to arg6.

Definition at line 4825 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 1257 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @plus_nat to a number of arguments.

Definition at line 1282 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 1247 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 105 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 95 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 137 of file nat1.h.

◆ cnat() [2/2]

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

inline

Application of function symbol @cNat.

Parameters

arg0	A data expression.

Returns: Application of @cNat to a number of arguments.

Definition at line 161 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 127 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @concat_digit to a number of arguments.

Definition at line 398 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 358 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 350 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 199 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @cPair to a number of arguments.

Definition at line 224 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 189 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 1061 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of div to a number of arguments.

Definition at line 1086 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 1945 of file nat64.h.

◆ div2() [2/2]

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

inline

Application of function symbol @div2.

Parameters

arg0	A data expression.

Returns: Application of @div2 to a number of arguments.

Definition at line 1969 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 1935 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 2673 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @div_bold to a number of arguments.

Definition at line 2698 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 2663 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 2737 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.
arg5	A data expression.

Returns: Application of @div_bold_whr to a number of arguments.

Definition at line 2766 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 2727 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 1051 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 2809 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @div_whr1 to a number of arguments.

Definition at line 2836 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 2799 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 2877 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @div_whr2 to a number of arguments.

Definition at line 2905 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 2867 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 1912 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @divmod to a number of arguments.

Definition at line 1937 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 3015 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @divmod_aux to a number of arguments.

Definition at line 3040 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 3005 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 3079 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @divmod_aux_whr1 to a number of arguments.

Definition at line 3106 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 3069 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 3147 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @divmod_aux_whr2 to a number of arguments.

Definition at line 3175 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 3137 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 3217 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @divmod_aux_whr3 to a number of arguments.

Definition at line 3245 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 3207 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 3287 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @divmod_aux_whr4 to a number of arguments.

Definition at line 3314 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 3277 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 3355 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @divmod_aux_whr5 to a number of arguments.

Definition at line 3382 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 3345 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 3423 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @divmod_aux_whr6 to a number of arguments.

Definition at line 3451 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 3413 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 1902 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 2042 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @ggdivmod to a number of arguments.

Definition at line 2068 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 2032 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 707 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @dub to a number of arguments.

Definition at line 732 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 697 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 771 of file nat1.h.

◆ dubsucc() [2/2]

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

inline

Application of function symbol @dubsucc.

Parameters

arg0	A data expression.

Returns: Application of @dubsucc to a number of arguments.

Definition at line 795 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 761 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

arg0	A data expression.

Returns: Application of @equals_one to a number of arguments.

Definition at line 585 of file nat64.h.

◆ equals_one() [2/2]

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

inline

Definition at line 559 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 551 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 437 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

arg0	A data expression.

Returns: Application of @equals_zero to a number of arguments.

Definition at line 461 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 427 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 1266 of file nat1.h.

◆ even() [2/2]

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

inline

Application of function symbol @even.

Parameters

arg0	A data expression.

Returns: Application of @even to a number of arguments.

Definition at line 1290 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 1256 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of exp to a number of arguments.

Definition at line 1227 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 1187 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 2275 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @exp_aux3n to a number of arguments.

Definition at line 2301 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 2265 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 2141 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @exp_aux3p to a number of arguments.

Definition at line 2167 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 2131 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 2341 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @exp_aux4n to a number of arguments.

Definition at line 2368 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 2331 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 2207 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @exp_aux4p to a number of arguments.

Definition at line 2234 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 2197 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 2607 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @exp_auxfalsen to a number of arguments.

Definition at line 2633 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 2597 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 2541 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @exp_auxfalsep to a number of arguments.

Definition at line 2567 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 2531 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 2475 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @exp_auxtruen to a number of arguments.

Definition at line 2501 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 2465 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 2409 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @exp_auxtruep to a number of arguments.

Definition at line 2435 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 2399 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 1179 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 1788 of file nat1.h.

◆ first() [2/2]

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

inline

Application of function symbol @first.

Parameters

arg0	A data expression.

Returns: Application of @first to a number of arguments.

Definition at line 1812 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 1778 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 1976 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @gdivmod to a number of arguments.

Definition at line 2002 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 1966 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 918 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @gtesubtb to a number of arguments.

Definition at line 944 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 908 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

e	A data expression.

Returns: true iff e is an application of function symbol add_with_carry to a number of arguments.

Definition at line 1239 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

e	A data expression.

Returns: true iff e is the function symbol matching @add_with_carry.

Definition at line 1202 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

e	A data expression.

Returns: true iff e is an application of function symbol auxiliary_plus_nat to a number of arguments.

Definition at line 1303 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

e	A data expression.

Returns: true iff e is the function symbol matching @plus_nat.

Definition at line 1267 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

e	A data expression.

Returns: true iff e is the function symbol matching @c0.

Definition at line 115 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

e	A data expression.

Returns: true iff e is an application of function symbol cnat to a number of arguments.

Definition at line 181 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

e	A data expression.

Returns: true iff e is the function symbol matching @cNat.

Definition at line 147 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

e	A data expression.

Returns: true iff e is an application of function symbol concat_digit to a number of arguments.

Definition at line 419 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

e	A data expression.

Returns: true iff e is the function symbol matching @concat_digit.

Definition at line 382 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

e	A data expression.

Returns: true iff e is an application of function symbol cpair to a number of arguments.

Definition at line 245 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

e	A data expression.

Returns: true iff e is the function symbol matching @cPair.

Definition at line 209 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

e	A data expression.

Returns: true iff e is an application of function symbol div2 to a number of arguments.

Definition at line 1989 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

e	A data expression.

Returns: true iff e is the function symbol matching @div2.

Definition at line 1955 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

e	A data expression.

Returns: true iff e is an application of function symbol div to a number of arguments.

Definition at line 1107 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

e	A data expression.

Returns: true iff e is an application of function symbol div_bold to a number of arguments.

Definition at line 2719 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

e	A data expression.

Returns: true iff e is the function symbol matching @div_bold.

Definition at line 2683 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

e	A data expression.

Returns: true iff e is an application of function symbol div_bold_whr to a number of arguments.

Definition at line 2791 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

e	A data expression.

Returns: true iff e is the function symbol matching @div_bold_whr.

Definition at line 2747 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

e	A data expression.

Returns: true iff e is the function symbol matching div.

Definition at line 1071 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

e	A data expression.

Returns: true iff e is an application of function symbol div_whr1 to a number of arguments.

Definition at line 2859 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

e	A data expression.

Returns: true iff e is the function symbol matching @div_whr1.

Definition at line 2819 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

e	A data expression.

Returns: true iff e is an application of function symbol div_whr2 to a number of arguments.

Definition at line 2929 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

e	A data expression.

Returns: true iff e is the function symbol matching @div_whr2.

Definition at line 2887 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod to a number of arguments.

Definition at line 1958 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux to a number of arguments.

Definition at line 3061 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux.

Definition at line 3025 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux_whr1 to a number of arguments.

Definition at line 3129 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux_whr1.

Definition at line 3089 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux_whr2 to a number of arguments.

Definition at line 3199 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux_whr2.

Definition at line 3157 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux_whr3 to a number of arguments.

Definition at line 3269 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux_whr3.

Definition at line 3227 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux_whr4 to a number of arguments.

Definition at line 3337 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux_whr4.

Definition at line 3297 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux_whr5 to a number of arguments.

Definition at line 3405 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux_whr5.

Definition at line 3365 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

e	A data expression.

Returns: true iff e is an application of function symbol divmod_aux_whr6 to a number of arguments.

Definition at line 3475 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod_aux_whr6.

Definition at line 3433 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

e	A data expression.

Returns: true iff e is the function symbol matching @divmod.

Definition at line 1922 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

e	A data expression.

Returns: true iff e is an application of function symbol doubly_generalised_divmod to a number of arguments.

Definition at line 2090 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

e	A data expression.

Returns: true iff e is the function symbol matching @ggdivmod.

Definition at line 2052 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

e	A data expression.

Returns: true iff e is an application of function symbol dub to a number of arguments.

Definition at line 753 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

e	A data expression.

Returns: true iff e is the function symbol matching @dub.

Definition at line 717 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

e	A data expression.

Returns: true iff e is an application of function symbol dubsucc to a number of arguments.

Definition at line 815 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

e	A data expression.

Returns: true iff e is the function symbol matching @dubsucc.

Definition at line 781 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

e	A data expression.

Returns: true iff e is an application of function symbol equals_one to a number of arguments.

Definition at line 605 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

e	A data expression.

Returns: true iff e is the function symbol matching @equals_one.

Definition at line 570 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

e	A data expression.

Returns: true iff e is an application of function symbol equals_zero to a number of arguments.

Definition at line 481 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

e	A data expression.

Returns: true iff e is the function symbol matching @equals_zero.

Definition at line 447 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

e	A data expression.

Returns: true iff e is an application of function symbol even to a number of arguments.

Definition at line 1310 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

e	A data expression.

Returns: true iff e is the function symbol matching @even.

Definition at line 1276 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

e	A data expression.

Returns: true iff e is an application of function symbol exp to a number of arguments.

Definition at line 1248 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_aux3n to a number of arguments.

Definition at line 2323 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_aux3n.

Definition at line 2285 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_aux3p to a number of arguments.

Definition at line 2189 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_aux3p.

Definition at line 2151 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_aux4n to a number of arguments.

Definition at line 2391 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_aux4n.

Definition at line 2351 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_aux4p to a number of arguments.

Definition at line 2257 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_aux4p.

Definition at line 2217 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_auxfalsen to a number of arguments.

Definition at line 2655 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_auxfalsen.

Definition at line 2617 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_auxfalsep to a number of arguments.

Definition at line 2589 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_auxfalsep.

Definition at line 2551 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_auxtruen to a number of arguments.

Definition at line 2523 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_auxtruen.

Definition at line 2485 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

e	A data expression.

Returns: true iff e is an application of function symbol exp_auxtruep to a number of arguments.

Definition at line 2457 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

e	A data expression.

Returns: true iff e is the function symbol matching @exp_auxtruep.

Definition at line 2419 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

e	A data expression.

Returns: true iff e is the function symbol matching exp.

Definition at line 1211 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

e	A data expression.

Returns: true iff e is an application of function symbol first to a number of arguments.

Definition at line 1832 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

e	A data expression.

Returns: true iff e is the function symbol matching @first.

Definition at line 1798 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

e	A data expression.

Returns: true iff e is an application of function symbol generalised_divmod to a number of arguments.

Definition at line 2024 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

e	A data expression.

Returns: true iff e is the function symbol matching @gdivmod.

Definition at line 1986 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

e	A data expression.

Returns: true iff e is an application of function symbol gte_subtract_with_borrow to a number of arguments.

Definition at line 966 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

e	A data expression.

Returns: true iff e is the function symbol matching @gtesubtb.

Definition at line 928 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

e	A data expression.

Returns: true iff e is an application of function symbol is_odd to a number of arguments.

Definition at line 1927 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

e	A data expression.

Returns: true iff e is the function symbol matching @is_odd.

Definition at line 1893 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

e	A data expression.

Returns: true iff e is an application of function symbol last to a number of arguments.

Definition at line 1894 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

e	A data expression.

Returns: true iff e is the function symbol matching @last.

Definition at line 1860 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

e	A data expression.

Returns: true iff e is an application of function symbol maximum to a number of arguments.

Definition at line 488 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

e	A data expression.

Returns: true iff e is the function symbol matching max.

Definition at line 451 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

e	A data expression.

Returns: true iff e is an application of function symbol minimum to a number of arguments.

Definition at line 565 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

e	A data expression.

Returns: true iff e is the function symbol matching min.

Definition at line 528 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

e	A data expression.

Returns: true iff e is an application of function symbol mod to a number of arguments.

Definition at line 1171 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

e	A data expression.

Returns: true iff e is the function symbol matching mod.

Definition at line 1135 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

e	A data expression.

Returns: true iff e is an application of function symbol mod_whr1 to a number of arguments.

Definition at line 2997 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

e	A data expression.

Returns: true iff e is the function symbol matching @mod_whr1.

Definition at line 2957 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

e	A data expression.

Returns: true iff e is an application of function symbol monus to a number of arguments.

Definition at line 1374 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

e	A data expression.

Returns: true iff e is the function symbol matching @monus.

Definition at line 1338 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

e	A data expression.

Returns: true iff e is an application of function symbol monus_whr to a number of arguments.

Definition at line 2123 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

e	A data expression.

Returns: true iff e is the function symbol matching @monus_whr.

Definition at line 2081 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

e	A data expression.

Returns: true iff e is an application of function symbol most_significant_digit_nat to a number of arguments.

Definition at line 342 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

e	A data expression.

Returns: true iff e is the function symbol matching @most_significant_digitNat.

Definition at line 308 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

e	A data expression.

Returns: true iff e is an application of function symbol msd to a number of arguments.

Definition at line 3537 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

e	A data expression.

Returns: true iff e is the function symbol matching @msd.

Definition at line 3503 of file nat64.h.

◆ is_nat()

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

inline

Recogniser for sort expression Nat.

Parameters

e	A sort expression

Returns: true iff e == nat()

Definition at line 53 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

e	A data expression.

Returns: true iff e is an application of function symbol nat2pos to a number of arguments.

Definition at line 403 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

e	A data expression.

Returns: true iff e is the function symbol matching Nat2Pos.

Definition at line 369 of file nat1.h.

◆ is_natnatpair()

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

inline

Recogniser for sort expression @NatNatPair.

Parameters

e	A sort expression

Returns: true iff e == natnatpair()

Definition at line 83 of file nat64.h.

◆ is_natpair()

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

inline

Recogniser for sort expression @NatPair.

Parameters

e	A sort expression

Returns: true iff e == natpair()

Definition at line 82 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

e	A data expression.

Returns: true iff e is an application of function symbol natpred to a number of arguments.

Definition at line 1865 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

e	A data expression.

Returns: true iff e is the function symbol matching @natpred.

Definition at line 1831 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

n	A data expression

Definition at line 530 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

e	A data expression.

Returns: true iff e is an application of function symbol nnpair to a number of arguments.

Definition at line 246 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

e	A data expression.

Returns: true iff e is the function symbol matching @nnPair.

Definition at line 210 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

e	A data expression.

Returns: true iff e is an application of function symbol not_equals_zero to a number of arguments.

Definition at line 543 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

e	A data expression.

Returns: true iff e is the function symbol matching @not_equals_zero.

Definition at line 509 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 1883 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

arg0	A data expression.

Returns: Application of @is_odd to a number of arguments.

Definition at line 1907 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 1873 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

e	A data expression.

Returns: true iff e is an application of function symbol plus to a number of arguments.

Definition at line 900 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

e	A data expression.

Returns: true iff e is the function symbol matching +.

Definition at line 863 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

e	A data expression.

Returns: true iff e is an application of function symbol pos2nat to a number of arguments.

Definition at line 341 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

e	A data expression.

Returns: true iff e is the function symbol matching Pos2Nat.

Definition at line 307 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

e	A data expression.

Returns: true iff e is an application of function symbol pred to a number of arguments.

Definition at line 689 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

e	A data expression.

Returns: true iff e is the function symbol matching pred.

Definition at line 655 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

e	A data expression.

Returns: true iff e is an application of function symbol pred_whr to a number of arguments.

Definition at line 1077 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

e	A data expression.

Returns: true iff e is the function symbol matching @pred_whr.

Definition at line 1043 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt to a number of arguments.

Definition at line 1704 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

e	A data expression.

Returns: true iff e is the function symbol matching sqrt.

Definition at line 1670 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_nat_aux_func to a number of arguments.

Definition at line 1770 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_nat.

Definition at line 1732 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair to a number of arguments.

Definition at line 4005 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair.

Definition at line 3971 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair_whr1 to a number of arguments.

Definition at line 4073 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair_whr1.

Definition at line 4033 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair_whr2 to a number of arguments.

Definition at line 4143 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair_whr2.

Definition at line 4101 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair_whr3 to a number of arguments.

Definition at line 4209 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair_whr3.

Definition at line 4171 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair_whr4 to a number of arguments.

Definition at line 4281 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair_whr4.

Definition at line 4237 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair_whr5 to a number of arguments.

Definition at line 4351 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair_whr5.

Definition at line 4309 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_pair_whr6 to a number of arguments.

Definition at line 4417 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_pair_whr6.

Definition at line 4379 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_whr1 to a number of arguments.

Definition at line 3873 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_whr1.

Definition at line 3833 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

e	A data expression.

Returns: true iff e is an application of function symbol sqrt_whr2 to a number of arguments.

Definition at line 3943 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

e	A data expression.

Returns: true iff e is the function symbol matching @sqrt_whr2.

Definition at line 3901 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

e	A data expression.

Returns: true iff e is an application of function symbol succ to a number of arguments.

Definition at line 627 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

e	A data expression.

Returns: true iff e is the function symbol matching succ.

Definition at line 592 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

e	A data expression.

Returns: true iff e is an application of function symbol succ_nat to a number of arguments.

Definition at line 182 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

e	A data expression.

Returns: true iff e is the function symbol matching @succ_nat.

Definition at line 148 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

e	A data expression.

Returns: true iff e is an application of function symbol swap_zero_add to a number of arguments.

Definition at line 1506 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

e	A data expression.

Returns: true iff e is the function symbol matching @swap_zero_add.

Definition at line 1466 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

e	A data expression.

Returns: true iff e is an application of function symbol swap_zero to a number of arguments.

Definition at line 1438 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

e	A data expression.

Returns: true iff e is the function symbol matching @swap_zero.

Definition at line 1402 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

e	A data expression.

Returns: true iff e is an application of function symbol swap_zero_min to a number of arguments.

Definition at line 1574 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

e	A data expression.

Returns: true iff e is the function symbol matching @swap_zero_min.

Definition at line 1534 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

e	A data expression.

Returns: true iff e is an application of function symbol swap_zero_monus to a number of arguments.

Definition at line 1642 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

e	A data expression.

Returns: true iff e is the function symbol matching @swap_zero_monus.

Definition at line 1602 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

e	A data expression.

Returns: true iff e is an application of function symbol times to a number of arguments.

Definition at line 1043 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

e	A data expression.

Returns: true iff e is the function symbol matching *.

Definition at line 1006 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

e	A data expression.

Returns: true iff e is an application of function symbol times_ordered to a number of arguments.

Definition at line 1457 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

e	A data expression.

Returns: true iff e is the function symbol matching @times_ordered.

Definition at line 1420 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

e	A data expression.

Returns: true iff e is an application of function symbol times_overflow to a number of arguments.

Definition at line 1536 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

e	A data expression.

Returns: true iff e is the function symbol matching @times_overflow.

Definition at line 1497 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 1850 of file nat1.h.

◆ last() [2/2]

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

inline

Application of function symbol @last.

Parameters

arg0	A data expression.

Returns: Application of @last to a number of arguments.

Definition at line 1874 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 1840 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

e	A data expression.

Precondition: left is defined for e.

Returns: The argument of e that corresponds to left.

Definition at line 2242 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

result	The data expression where the @add_with_carry expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1229 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

result	The data expression where the @plus_nat expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1293 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

result	The data expression where the @cNat expression is put.
arg0	A data expression.

Definition at line 171 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

result	The data expression where the @concat_digit expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 409 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

result	The data expression where the @cPair expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 235 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

result	The data expression where the div expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1097 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

result	The data expression where the @div2 expression is put.
arg0	A data expression.

Definition at line 1979 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

result	The data expression where the @div_bold expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 2709 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

result	The data expression where the @div_bold_whr expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.
arg5	A data expression.

Definition at line 2781 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

result	The data expression where the @div_whr1 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 2849 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

result	The data expression where the @div_whr2 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 2919 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

result	The data expression where the @divmod expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1948 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

result	The data expression where the @divmod_aux expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 3051 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

result	The data expression where the @divmod_aux_whr1 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 3119 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

result	The data expression where the @divmod_aux_whr2 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 3189 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

result	The data expression where the @divmod_aux_whr3 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 3259 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

result	The data expression where the @divmod_aux_whr4 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 3327 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

result	The data expression where the @divmod_aux_whr5 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 3395 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

result	The data expression where the @divmod_aux_whr6 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 3465 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

result	The data expression where the @ggdivmod expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2080 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

result	The data expression where the @dub expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 743 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

result	The data expression where the @dubsucc expression is put.
arg0	A data expression.

Definition at line 805 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

result	The data expression where the @equals_one expression is put.
arg0	A data expression.

Definition at line 595 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

result	The data expression where the @equals_zero expression is put.
arg0	A data expression.

Definition at line 471 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

result	The data expression where the @even expression is put.
arg0	A data expression.

Definition at line 1300 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

result	The data expression where the exp expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1238 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

result	The data expression where the @exp_aux3n expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2313 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

result	The data expression where the @exp_aux3p expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2179 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

result	The data expression where the @exp_aux4n expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 2381 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

result	The data expression where the @exp_aux4p expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 2247 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

result	The data expression where the @exp_auxfalsen expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2645 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

result	The data expression where the @exp_auxfalsep expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2579 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

result	The data expression where the @exp_auxtruen expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2513 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

result	The data expression where the @exp_auxtruep expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2447 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

result	The data expression where the @first expression is put.
arg0	A data expression.

Definition at line 1822 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

result	The data expression where the @gdivmod expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 2014 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

result	The data expression where the @gtesubtb expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 956 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

result	The data expression where the @is_odd expression is put.
arg0	A data expression.

Definition at line 1917 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

result	The data expression where the @last expression is put.
arg0	A data expression.

Definition at line 1884 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

result	The data expression where the max expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 478 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

result	The data expression where the min expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 555 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

result	The data expression where the mod expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1161 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

result	The data expression where the @mod_whr1 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 2987 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

result	The data expression where the @monus expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1364 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

result	The data expression where the @monus_whr expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 2113 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

result	The data expression where the @most_significant_digitNat expression is put.
arg0	A data expression.

Definition at line 332 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

result	The data expression where the @msd expression is put.
arg0	A data expression.

Definition at line 3527 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

result	The data expression where the Nat2Pos expression is put.
arg0	A data expression.

Definition at line 393 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

result	The data expression where the @natpred expression is put.
arg0	A data expression.

Definition at line 1855 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

result	The data expression where the @nnPair expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 236 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

result	The data expression where the @not_equals_zero expression is put.
arg0	A data expression.

Definition at line 533 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

result	The data expression where the + expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 890 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

result	The data expression where the Pos2Nat expression is put.
arg0	A data expression.

Definition at line 331 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

result	The data expression where the pred expression is put.
arg0	A data expression.

Definition at line 679 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

result	The data expression where the @pred_whr expression is put.
arg0	A data expression.

Definition at line 1067 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

result	The data expression where the sqrt expression is put.
arg0	A data expression.

Definition at line 1694 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

result	The data expression where the @sqrt_nat expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 1760 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

result	The data expression where the @sqrt_pair expression is put.
arg0	A data expression.

Definition at line 3995 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

result	The data expression where the @sqrt_pair_whr1 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 4063 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

result	The data expression where the @sqrt_pair_whr2 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 4133 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

result	The data expression where the @sqrt_pair_whr3 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 4199 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

result	The data expression where the @sqrt_pair_whr4 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.
arg5	A data expression.

Definition at line 4271 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

result	The data expression where the @sqrt_pair_whr5 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 4341 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

result	The data expression where the @sqrt_pair_whr6 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 4407 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

result	The data expression where the @sqrt_whr1 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 3863 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

result	The data expression where the @sqrt_whr2 expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 3933 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

result	The data expression where the succ expression is put.
arg0	A data expression.

Definition at line 617 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

result	The data expression where the @succ_nat expression is put.
arg0	A data expression.

Definition at line 172 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

result	The data expression where the @swap_zero expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1428 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

result	The data expression where the @swap_zero_add expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 1496 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

result	The data expression where the @swap_zero_min expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 1564 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

result	The data expression where the @swap_zero_monus expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Definition at line 1632 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

result	The data expression where the * expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1033 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

result	The data expression where the @times_ordered expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1447 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

result	The data expression where the @times_overflow expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 1526 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of max to a number of arguments.

Definition at line 467 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 419 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 411 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of min to a number of arguments.

Definition at line 544 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 504 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 496 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 1125 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of mod to a number of arguments.

Definition at line 1150 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 1115 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 2947 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @mod_whr1 to a number of arguments.

Definition at line 2974 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 2937 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 1328 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @monus to a number of arguments.

Definition at line 1353 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 1318 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 2071 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

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @monus_whr to a number of arguments.

Definition at line 2099 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 2061 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 298 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

arg0	A data expression.

Returns: Application of @most_significant_digitNat to a number of arguments.

Definition at line 322 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 288 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 3493 of file nat64.h.

◆ msd() [2/2]

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

inline

Application of function symbol @msd.

Parameters

arg0	A data expression.

Returns: Application of @msd to a number of arguments.

Definition at line 3517 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 3483 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 43 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

n A string

Definition at line 498 of file standard_numbers_utility.h.

◆ nat() [3/3]

template<typename T >
requires std::is_integral_v<T>

data_expression mcrl2::data::sort_nat::nat ( T t )

inline

Constructs expression of type pos from an integral type.

Definition at line 481 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 359 of file nat1.h.

◆ nat2pos() [2/2]

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

inline

Application of function symbol Nat2Pos.

Parameters

arg0	A data expression.

Returns: Application of Nat2Pos to a number of arguments.

Definition at line 383 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 349 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 278 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 2195 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 2138 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 252 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 2287 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 2097 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 264 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 2151 of file nat1.h.

◆ nat_name()

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

inline

Definition at line 34 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 73 of file nat64.h.

◆ natnatpair_name()

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

inline

Definition at line 64 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 72 of file nat1.h.

◆ natpair_name()

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

inline

Definition at line 63 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 1821 of file nat64.h.

◆ natpred() [2/2]

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

inline

Application of function symbol @natpred.

Parameters

arg0	A data expression.

Returns: Application of @natpred to a number of arguments.

Definition at line 1845 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 1811 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

n	A data expression

Precondition: is_natural_constant(n)

Returns: String representation of n

Definition at line 551 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

n	A data expression

Precondition: is_natural_constant(n)

Returns: NUMERIC_VALUE representation of n

Definition at line 590 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 200 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of @nnPair to a number of arguments.

Definition at line 225 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 190 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 499 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

arg0	A data expression.

Returns: Application of @not_equals_zero to a number of arguments.

Definition at line 523 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 489 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

arg0	A data expression.
arg1	A data expression.

Returns: Application of + to a number of arguments.

Definition at line 879 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 831 of file nat1.h.

◆ plus_name()

const core::identifier_string & mcrl2::data::sort_nat::plus_name ( )

inline

Generate identifier +.

Returns: Identifier +.

Definition at line 823 of file nat1.h.

◆ pos2nat() [1/2]

const function_symbol & mcrl2::data::sort_nat::pos2nat ( )

inline

Constructor for function symbol Pos2Nat.

Returns: Function symbol pos2nat.

Definition at line 297 of file nat1.h.

◆ pos2nat() [2/2]

application mcrl2::data::sort_nat::pos2nat ( const data_expression & arg0 )

inline

Application of function symbol Pos2Nat.

Parameters

arg0	A data expression.

Returns: Application of Pos2Nat to a number of arguments.

Definition at line 321 of file nat1.h.

◆ pos2nat_name()

const core::identifier_string & mcrl2::data::sort_nat::pos2nat_name ( )

inline

Generate identifier Pos2Nat.

Returns: Identifier Pos2Nat.

Definition at line 287 of file nat1.h.

◆ pred() [1/2]

const function_symbol & mcrl2::data::sort_nat::pred ( )

inline

Constructor for function symbol pred.

Returns: Function symbol pred.

Definition at line 645 of file nat1.h.

◆ pred() [2/2]

application mcrl2::data::sort_nat::pred ( const data_expression & arg0 )

inline

Application of function symbol pred.

Parameters

arg0	A data expression.

Returns: Application of pred to a number of arguments.

Definition at line 669 of file nat1.h.

◆ pred_name()

const core::identifier_string & mcrl2::data::sort_nat::pred_name ( )

inline

Generate identifier pred.

Returns: Identifier pred.

Definition at line 635 of file nat1.h.

◆ pred_whr() [1/2]

const function_symbol & mcrl2::data::sort_nat::pred_whr ( )

inline

Constructor for function symbol @pred_whr.

Returns: Function symbol pred_whr.

Definition at line 1033 of file nat64.h.

◆ pred_whr() [2/2]

application mcrl2::data::sort_nat::pred_whr ( const data_expression & arg0 )

inline

Application of function symbol @pred_whr.

Parameters

arg0	A data expression.

Returns: Application of @pred_whr to a number of arguments.

Definition at line 1057 of file nat64.h.

◆ pred_whr_name()

const core::identifier_string & mcrl2::data::sort_nat::pred_whr_name ( )

inline

Generate identifier @pred_whr.

Returns: Identifier @pred_whr.

Definition at line 1023 of file nat64.h.

◆ right()

const data_expression & mcrl2::data::sort_nat::right ( const data_expression & e )

inline

Function for projecting out argument. right from an application.

Parameters

e	A data expression.

Precondition: right is defined for e.

Returns: The argument of e that corresponds to right.

Definition at line 2254 of file nat1.h.

◆ sqrt() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt ( )

inline

Constructor for function symbol sqrt.

Returns: Function symbol sqrt.

Definition at line 1660 of file nat1.h.

◆ sqrt() [2/2]

application mcrl2::data::sort_nat::sqrt ( const data_expression & arg0 )

inline

Application of function symbol sqrt.

Parameters

arg0	A data expression.

Returns: Application of sqrt to a number of arguments.

Definition at line 1684 of file nat1.h.

◆ sqrt_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_name ( )

inline

Generate identifier sqrt.

Returns: Identifier sqrt.

Definition at line 1650 of file nat1.h.

◆ sqrt_nat_aux_func() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_nat_aux_func ( )

inline

Constructor for function symbol @sqrt_nat.

Returns: Function symbol sqrt_nat_aux_func.

Definition at line 1722 of file nat1.h.

◆ sqrt_nat_aux_func() [2/2]

application mcrl2::data::sort_nat::sqrt_nat_aux_func	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @sqrt_nat.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @sqrt_nat to a number of arguments.

Definition at line 1748 of file nat1.h.

◆ sqrt_nat_aux_func_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_nat_aux_func_name ( )

inline

Generate identifier @sqrt_nat.

Returns: Identifier @sqrt_nat.

Definition at line 1712 of file nat1.h.

◆ sqrt_pair() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair ( )

inline

Constructor for function symbol @sqrt_pair.

Returns: Function symbol sqrt_pair.

Definition at line 3961 of file nat64.h.

◆ sqrt_pair() [2/2]

application mcrl2::data::sort_nat::sqrt_pair ( const data_expression & arg0 )

inline

Application of function symbol @sqrt_pair.

Parameters

arg0	A data expression.

Returns: Application of @sqrt_pair to a number of arguments.

Definition at line 3985 of file nat64.h.

◆ sqrt_pair_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_name ( )

inline

Generate identifier @sqrt_pair.

Returns: Identifier @sqrt_pair.

Definition at line 3951 of file nat64.h.

◆ sqrt_pair_whr1() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair_whr1 ( )

inline

Constructor for function symbol @sqrt_pair_whr1.

Returns: Function symbol sqrt_pair_whr1.

Definition at line 4023 of file nat64.h.

◆ sqrt_pair_whr1() [2/2]

application mcrl2::data::sort_nat::sqrt_pair_whr1	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2,
		const data_expression &	arg3
	)

inline

Application of function symbol @sqrt_pair_whr1.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @sqrt_pair_whr1 to a number of arguments.

Definition at line 4050 of file nat64.h.

◆ sqrt_pair_whr1_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_whr1_name ( )

inline

Generate identifier @sqrt_pair_whr1.

Returns: Identifier @sqrt_pair_whr1.

Definition at line 4013 of file nat64.h.

◆ sqrt_pair_whr2() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair_whr2 ( )

inline

Constructor for function symbol @sqrt_pair_whr2.

Returns: Function symbol sqrt_pair_whr2.

Definition at line 4091 of file nat64.h.

◆ sqrt_pair_whr2() [2/2]

application mcrl2::data::sort_nat::sqrt_pair_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 @sqrt_pair_whr2.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @sqrt_pair_whr2 to a number of arguments.

Definition at line 4119 of file nat64.h.

◆ sqrt_pair_whr2_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_whr2_name ( )

inline

Generate identifier @sqrt_pair_whr2.

Returns: Identifier @sqrt_pair_whr2.

Definition at line 4081 of file nat64.h.

◆ sqrt_pair_whr3() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair_whr3 ( )

inline

Constructor for function symbol @sqrt_pair_whr3.

Returns: Function symbol sqrt_pair_whr3.

Definition at line 4161 of file nat64.h.

◆ sqrt_pair_whr3() [2/2]

application mcrl2::data::sort_nat::sqrt_pair_whr3	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @sqrt_pair_whr3.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @sqrt_pair_whr3 to a number of arguments.

Definition at line 4187 of file nat64.h.

◆ sqrt_pair_whr3_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_whr3_name ( )

inline

Generate identifier @sqrt_pair_whr3.

Returns: Identifier @sqrt_pair_whr3.

Definition at line 4151 of file nat64.h.

◆ sqrt_pair_whr4() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair_whr4 ( )

inline

Constructor for function symbol @sqrt_pair_whr4.

Returns: Function symbol sqrt_pair_whr4.

Definition at line 4227 of file nat64.h.

◆ sqrt_pair_whr4() [2/2]

application mcrl2::data::sort_nat::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
	)

inline

Application of function symbol @sqrt_pair_whr4.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.
arg5	A data expression.

Returns: Application of @sqrt_pair_whr4 to a number of arguments.

Definition at line 4256 of file nat64.h.

◆ sqrt_pair_whr4_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_whr4_name ( )

inline

Generate identifier @sqrt_pair_whr4.

Returns: Identifier @sqrt_pair_whr4.

Definition at line 4217 of file nat64.h.

◆ sqrt_pair_whr5() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair_whr5 ( )

inline

Constructor for function symbol @sqrt_pair_whr5.

Returns: Function symbol sqrt_pair_whr5.

Definition at line 4299 of file nat64.h.

◆ sqrt_pair_whr5() [2/2]

application mcrl2::data::sort_nat::sqrt_pair_whr5	(	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 @sqrt_pair_whr5.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @sqrt_pair_whr5 to a number of arguments.

Definition at line 4327 of file nat64.h.

◆ sqrt_pair_whr5_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_whr5_name ( )

inline

Generate identifier @sqrt_pair_whr5.

Returns: Identifier @sqrt_pair_whr5.

Definition at line 4289 of file nat64.h.

◆ sqrt_pair_whr6() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_pair_whr6 ( )

inline

Constructor for function symbol @sqrt_pair_whr6.

Returns: Function symbol sqrt_pair_whr6.

Definition at line 4369 of file nat64.h.

◆ sqrt_pair_whr6() [2/2]

application mcrl2::data::sort_nat::sqrt_pair_whr6	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @sqrt_pair_whr6.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @sqrt_pair_whr6 to a number of arguments.

Definition at line 4395 of file nat64.h.

◆ sqrt_pair_whr6_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_pair_whr6_name ( )

inline

Generate identifier @sqrt_pair_whr6.

Returns: Identifier @sqrt_pair_whr6.

Definition at line 4359 of file nat64.h.

◆ sqrt_whr1() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_whr1 ( )

inline

Constructor for function symbol @sqrt_whr1.

Returns: Function symbol sqrt_whr1.

Definition at line 3823 of file nat64.h.

◆ sqrt_whr1() [2/2]

application mcrl2::data::sort_nat::sqrt_whr1	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2,
		const data_expression &	arg3
	)

inline

Application of function symbol @sqrt_whr1.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @sqrt_whr1 to a number of arguments.

Definition at line 3850 of file nat64.h.

◆ sqrt_whr1_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_whr1_name ( )

inline

Generate identifier @sqrt_whr1.

Returns: Identifier @sqrt_whr1.

Definition at line 3813 of file nat64.h.

◆ sqrt_whr2() [1/2]

const function_symbol & mcrl2::data::sort_nat::sqrt_whr2 ( )

inline

Constructor for function symbol @sqrt_whr2.

Returns: Function symbol sqrt_whr2.

Definition at line 3891 of file nat64.h.

◆ sqrt_whr2() [2/2]

application mcrl2::data::sort_nat::sqrt_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 @sqrt_whr2.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns: Application of @sqrt_whr2 to a number of arguments.

Definition at line 3919 of file nat64.h.

◆ sqrt_whr2_name()

const core::identifier_string & mcrl2::data::sort_nat::sqrt_whr2_name ( )

inline

Generate identifier @sqrt_whr2.

Returns: Identifier @sqrt_whr2.

Definition at line 3881 of file nat64.h.

◆ succ() [1/2]

application mcrl2::data::sort_nat::succ ( const data_expression & arg0 )

inline

Application of function symbol succ.

Parameters

arg0	A data expression.

Returns: Application of succ to a number of arguments.

Definition at line 607 of file nat1.h.

◆ succ() [2/2]

function_symbol mcrl2::data::sort_nat::succ ( const sort_expression & s0 )

inline

Definition at line 581 of file nat1.h.

◆ succ_name()

const core::identifier_string & mcrl2::data::sort_nat::succ_name ( )

inline

Generate identifier succ.

Returns: Identifier succ.

Definition at line 573 of file nat1.h.

◆ succ_nat() [1/2]

const function_symbol & mcrl2::data::sort_nat::succ_nat ( )

inline

Constructor for function symbol @succ_nat.

Returns: Function symbol succ_nat.

Definition at line 138 of file nat64.h.

◆ succ_nat() [2/2]

application mcrl2::data::sort_nat::succ_nat ( const data_expression & arg0 )

inline

Application of function symbol @succ_nat.

Parameters

arg0	A data expression.

Returns: Application of @succ_nat to a number of arguments.

Definition at line 162 of file nat64.h.

◆ succ_nat_name()

const core::identifier_string & mcrl2::data::sort_nat::succ_nat_name ( )

inline

Generate identifier @succ_nat.

Returns: Identifier @succ_nat.

Definition at line 128 of file nat64.h.

◆ swap_zero() [1/2]

const function_symbol & mcrl2::data::sort_nat::swap_zero ( )

inline

Constructor for function symbol @swap_zero.

Returns: Function symbol swap_zero.

Definition at line 1392 of file nat1.h.

◆ swap_zero() [2/2]

application mcrl2::data::sort_nat::swap_zero	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @swap_zero.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of @swap_zero to a number of arguments.

Definition at line 1417 of file nat1.h.

◆ swap_zero_add() [1/2]

const function_symbol & mcrl2::data::sort_nat::swap_zero_add ( )

inline

Constructor for function symbol @swap_zero_add.

Returns: Function symbol swap_zero_add.

Definition at line 1456 of file nat1.h.

◆ swap_zero_add() [2/2]

application mcrl2::data::sort_nat::swap_zero_add	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2,
		const data_expression &	arg3
	)

inline

Application of function symbol @swap_zero_add.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @swap_zero_add to a number of arguments.

Definition at line 1483 of file nat1.h.

◆ swap_zero_add_name()

const core::identifier_string & mcrl2::data::sort_nat::swap_zero_add_name ( )

inline

Generate identifier @swap_zero_add.

Returns: Identifier @swap_zero_add.

Definition at line 1446 of file nat1.h.

◆ swap_zero_min() [1/2]

const function_symbol & mcrl2::data::sort_nat::swap_zero_min ( )

inline

Constructor for function symbol @swap_zero_min.

Returns: Function symbol swap_zero_min.

Definition at line 1524 of file nat1.h.

◆ swap_zero_min() [2/2]

application mcrl2::data::sort_nat::swap_zero_min	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2,
		const data_expression &	arg3
	)

inline

Application of function symbol @swap_zero_min.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @swap_zero_min to a number of arguments.

Definition at line 1551 of file nat1.h.

◆ swap_zero_min_name()

const core::identifier_string & mcrl2::data::sort_nat::swap_zero_min_name ( )

inline

Generate identifier @swap_zero_min.

Returns: Identifier @swap_zero_min.

Definition at line 1514 of file nat1.h.

◆ swap_zero_monus() [1/2]

const function_symbol & mcrl2::data::sort_nat::swap_zero_monus ( )

inline

Constructor for function symbol @swap_zero_monus.

Returns: Function symbol swap_zero_monus.

Definition at line 1592 of file nat1.h.

◆ swap_zero_monus() [2/2]

application mcrl2::data::sort_nat::swap_zero_monus	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2,
		const data_expression &	arg3
	)

inline

Application of function symbol @swap_zero_monus.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.

Returns: Application of @swap_zero_monus to a number of arguments.

Definition at line 1619 of file nat1.h.

◆ swap_zero_monus_name()

const core::identifier_string & mcrl2::data::sort_nat::swap_zero_monus_name ( )

inline

Generate identifier @swap_zero_monus.

Returns: Identifier @swap_zero_monus.

Definition at line 1582 of file nat1.h.

◆ swap_zero_name()

const core::identifier_string & mcrl2::data::sort_nat::swap_zero_name ( )

inline

Generate identifier @swap_zero.

Returns: Identifier @swap_zero.

Definition at line 1382 of file nat1.h.

◆ times() [1/2]

application mcrl2::data::sort_nat::times	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol *.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of * to a number of arguments.

Definition at line 1022 of file nat1.h.

◆ times() [2/2]

function_symbol mcrl2::data::sort_nat::times	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 982 of file nat1.h.

◆ times_name()

const core::identifier_string & mcrl2::data::sort_nat::times_name ( )

inline

Generate identifier *.

Returns: Identifier *.

Definition at line 974 of file nat1.h.

◆ times_ordered() [1/2]

application mcrl2::data::sort_nat::times_ordered	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @times_ordered.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of @times_ordered to a number of arguments.

Definition at line 1436 of file nat64.h.

◆ times_ordered() [2/2]

function_symbol mcrl2::data::sort_nat::times_ordered	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1396 of file nat64.h.

◆ times_ordered_name()

const core::identifier_string & mcrl2::data::sort_nat::times_ordered_name ( )

inline

Generate identifier @times_ordered.

Returns: Identifier @times_ordered.

Definition at line 1388 of file nat64.h.

◆ times_overflow() [1/2]

application mcrl2::data::sort_nat::times_overflow	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @times_overflow.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @times_overflow to a number of arguments.

Definition at line 1514 of file nat64.h.

◆ times_overflow() [2/2]

function_symbol mcrl2::data::sort_nat::times_overflow	(	const sort_expression &	s0,
		const sort_expression &	s1,
		const sort_expression &	s2
	)

inline

Definition at line 1473 of file nat64.h.

◆ times_overflow_name()

const core::identifier_string & mcrl2::data::sort_nat::times_overflow_name ( )

inline

Generate identifier @times_overflow.

Returns: Identifier @times_overflow.

Definition at line 1465 of file nat64.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ add_with_carry() [1/2]

◆ add_with_carry() [2/2]

◆ add_with_carry_name()

◆ arg()

◆ arg1()

◆ arg2()

◆ arg3()

◆ arg4()

◆ arg5()

◆ arg6()

◆ auxiliary_plus_nat() [1/2]

◆ auxiliary_plus_nat() [2/2]

◆ auxiliary_plus_nat_name()

◆ c0()

◆ c0_name()

◆ cnat() [1/2]

◆ cnat() [2/2]

◆ cnat_name()

◆ concat_digit() [1/2]

◆ concat_digit() [2/2]

◆ concat_digit_name()

◆ cpair() [1/2]

◆ cpair() [2/2]

◆ cpair_name()

◆ div() [1/2]

◆ div() [2/2]

◆ div2() [1/2]

◆ div2() [2/2]

◆ div2_name()

◆ div_bold() [1/2]

◆ div_bold() [2/2]

◆ div_bold_name()

◆ div_bold_whr() [1/2]

◆ div_bold_whr() [2/2]

◆ div_bold_whr_name()

◆ div_name()

◆ div_whr1() [1/2]

◆ div_whr1() [2/2]

◆ div_whr1_name()

◆ div_whr2() [1/2]

◆ div_whr2() [2/2]

◆ div_whr2_name()

◆ divmod() [1/2]

◆ divmod() [2/2]

◆ divmod_aux() [1/2]

◆ divmod_aux() [2/2]

◆ divmod_aux_name()

◆ divmod_aux_whr1() [1/2]

◆ divmod_aux_whr1() [2/2]

◆ divmod_aux_whr1_name()

◆ divmod_aux_whr2() [1/2]

◆ divmod_aux_whr2() [2/2]

◆ divmod_aux_whr2_name()

◆ divmod_aux_whr3() [1/2]

◆ divmod_aux_whr3() [2/2]

◆ divmod_aux_whr3_name()

◆ divmod_aux_whr4() [1/2]

◆ divmod_aux_whr4() [2/2]

◆ divmod_aux_whr4_name()

◆ divmod_aux_whr5() [1/2]

◆ divmod_aux_whr5() [2/2]

◆ divmod_aux_whr5_name()

◆ divmod_aux_whr6() [1/2]

◆ divmod_aux_whr6() [2/2]

◆ divmod_aux_whr6_name()

◆ divmod_name()

◆ doubly_generalised_divmod() [1/2]

◆ doubly_generalised_divmod() [2/2]

◆ doubly_generalised_divmod_name()

◆ dub() [1/2]

◆ dub() [2/2]

◆ dub_name()

◆ dubsucc() [1/2]

◆ dubsucc() [2/2]