mcrl2/data/nat.h

Include file:

#include "mcrl2/data/nat.h"

The standard sort nat.

This file was generated from the data sort specification mcrl2/data/build/nat.spec.

Functions

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

Function for projecting out argument arg from an application.

Parameters:

  • e A data expression

Pre: arg is defined for e

Returns: The argument of e that corresponds to arg

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

Function for projecting out argument arg1 from an application.

Parameters:

  • e A data expression

Pre: arg1 is defined for e

Returns: The argument of e that corresponds to arg1

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

Function for projecting out argument arg2 from an application.

Parameters:

  • e A data expression

Pre: arg2 is defined for e

Returns: The argument of e that corresponds to arg2

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

Function for projecting out argument arg3 from an application.

Parameters:

  • e A data expression

Pre: arg3 is defined for e

Returns: The argument of e that corresponds to arg3

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

Function for projecting out argument arg4 from an application.

Parameters:

  • e A data expression

Pre: arg4 is defined for e

Returns: The argument of e that corresponds to arg4

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

Constructor for function symbol @c0.

Returns: Function symbol c0

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

Generate identifier @c0.

Returns: Identifier @c0

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

Constructor for function symbol @cNat.

Returns: Function symbol cnat

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

Application of function symbol @cNat.

Parameters:

  • arg0 A data expression

Returns: Application of @cNat to a number of arguments

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

Generate identifier @cNat.

Returns: Identifier @cNat

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

Constructor for function symbol @cPair.

Returns: Function symbol cpair

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

Application of function symbol @cPair.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @cPair to a number of arguments

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

Generate identifier @cPair.

Returns: Identifier @cPair

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

Constructor for function symbol div.

Returns: Function symbol div

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

Application of function symbol div.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of div to a number of arguments

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

Generate identifier div.

Returns: Identifier div

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

Constructor for function symbol @divmod.

Returns: Function symbol divmod

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

Application of function symbol @divmod.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @divmod to a number of arguments

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

Generate identifier @divmod.

Returns: Identifier @divmod

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

Constructor for function symbol @ggdivmod.

Returns: Function symbol doubly_generalised_divmod

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

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

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

Generate identifier @ggdivmod.

Returns: Identifier @ggdivmod

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

Constructor for function symbol @dub.

Returns: Function symbol dub

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

Application of function symbol @dub.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @dub to a number of arguments

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

Generate identifier @dub.

Returns: Identifier @dub

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

Constructor for function symbol @even.

Returns: Function symbol even

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

Application of function symbol @even.

Parameters:

  • arg0 A data expression

Returns: Application of @even to a number of arguments

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

Generate identifier @even.

Returns: Identifier @even

function_symbol const &mcrl2::data::sort_nat::exp(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_nat::exp(const data_expression &arg0, const data_expression &arg1)

Application of function symbol exp.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of exp to a number of arguments

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

Generate identifier exp.

Returns: Identifier exp

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

Constructor for function symbol @first.

Returns: Function symbol first

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

Application of function symbol @first.

Parameters:

  • arg0 A data expression

Returns: Application of @first to a number of arguments

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

Generate identifier @first.

Returns: Identifier @first

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

Constructor for function symbol @gdivmod.

Returns: Function symbol generalised_divmod

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

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

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

Generate identifier @gdivmod.

Returns: Identifier @gdivmod

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

Constructor for function symbol @gtesubtb.

Returns: Function symbol gte_subtract_with_borrow

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

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

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

Generate identifier @gtesubtb.

Returns: Identifier @gtesubtb

bool mcrl2::data::sort_nat::is_c0_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @c0.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_cnat_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_cnat_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cNat.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_cpair_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_cpair_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cPair.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_div_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_div_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function div.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching div

bool mcrl2::data::sort_nat::is_divmod_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_divmod_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @divmod.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_doubly_generalised_divmod_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_doubly_generalised_divmod_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @ggdivmod.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_dub_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_dub_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @dub.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_even_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_even_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @even.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_exp_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_exp_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function exp.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching exp

bool mcrl2::data::sort_nat::is_first_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_first_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @first.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_generalised_divmod_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_generalised_divmod_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @gdivmod.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_gte_subtract_with_borrow_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_gte_subtract_with_borrow_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @gtesubtb.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_last_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_last_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @last.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_maximum_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_maximum_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function max.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching max

bool mcrl2::data::sort_nat::is_minimum_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_minimum_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function min.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching min

bool mcrl2::data::sort_nat::is_mod_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_mod_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function mod.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching mod

bool mcrl2::data::sort_nat::is_monus_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_monus_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @monus.

Parameters:

  • e A data expression

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

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

Recogniser for sort expression Nat.

Parameters:

  • e A sort expression

Returns: true iff e == nat()

bool mcrl2::data::sort_nat::is_nat2pos_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_nat2pos_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Nat2Pos.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Nat2Pos

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

Recogniser for sort expression @NatPair.

Parameters:

  • e A sort expression

Returns: true iff e == natpair()

bool mcrl2::data::sort_nat::is_plus_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_plus_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function +.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching +

bool mcrl2::data::sort_nat::is_pos2nat_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_pos2nat_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Pos2Nat.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Pos2Nat

bool mcrl2::data::sort_nat::is_pred_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_pred_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function pred.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching pred

bool mcrl2::data::sort_nat::is_sqrt_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_sqrt_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function sqrt.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching sqrt

bool mcrl2::data::sort_nat::is_sqrt_nat_aux_func_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_sqrt_nat_aux_func_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @sqrt_nat.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_succ_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_succ_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function succ.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching succ

bool mcrl2::data::sort_nat::is_swap_zero_add_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_swap_zero_add_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @swap_zero_add.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_swap_zero_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_swap_zero_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @swap_zero.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_swap_zero_min_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_swap_zero_min_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @swap_zero_min.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_swap_zero_monus_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_swap_zero_monus_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @swap_zero_monus.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_nat::is_times_application(const atermpp::aterm_appl &e)

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

bool mcrl2::data::sort_nat::is_times_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function *.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching *

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

Constructor for function symbol @last.

Returns: Function symbol last

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

Application of function symbol @last.

Parameters:

  • arg0 A data expression

Returns: Application of @last to a number of arguments

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

Generate identifier @last.

Returns: Identifier @last

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

Function for projecting out argument left from an application.

Parameters:

  • e A data expression

Pre: left is defined for e

Returns: The argument of e that corresponds to left

function_symbol const &mcrl2::data::sort_nat::maximum(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_nat::maximum(const data_expression &arg0, const data_expression &arg1)

Application of function symbol max.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of max to a number of arguments

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

Generate identifier max.

Returns: Identifier max

function_symbol const &mcrl2::data::sort_nat::minimum(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_nat::minimum(const data_expression &arg0, const data_expression &arg1)

Application of function symbol min.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of min to a number of arguments

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

Generate identifier min.

Returns: Identifier min

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

Constructor for function symbol mod.

Returns: Function symbol mod

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

Application of function symbol mod.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of mod to a number of arguments

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

Generate identifier mod.

Returns: Identifier mod

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

Constructor for function symbol @monus.

Returns: Function symbol monus

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

Application of function symbol @monus.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @monus to a number of arguments

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

Generate identifier @monus.

Returns: Identifier @monus

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

Constructor for sort expression Nat.

Returns: Sort expression Nat

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

Constructor for function symbol Nat2Pos.

Returns: Function symbol nat2pos

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

Application of function symbol Nat2Pos.

Parameters:

  • arg0 A data expression

Returns: Application of Nat2Pos to a number of arguments

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

Generate identifier Nat2Pos.

Returns: Identifier Nat2Pos

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

Give all system defined constructors for nat.

Returns: All system defined constructors for nat

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

Give all system defined equations for nat.

Returns: All system defined equations for sort nat

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

Give all system defined mappings for nat.

Returns: All system defined mappings for nat

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

Constructor for sort expression @NatPair.

Returns: Sort expression @NatPair

core::identifier_string const &mcrl2::data::sort_nat::natpair_name()
function_symbol const &mcrl2::data::sort_nat::plus(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_nat::plus(const data_expression &arg0, const data_expression &arg1)

Application of function symbol +.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of + to a number of arguments

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

Generate identifier +.

Returns: Identifier +

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

Constructor for function symbol Pos2Nat.

Returns: Function symbol pos2nat

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

Application of function symbol Pos2Nat.

Parameters:

  • arg0 A data expression

Returns: Application of Pos2Nat to a number of arguments

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

Generate identifier Pos2Nat.

Returns: Identifier Pos2Nat

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

Constructor for function symbol pred.

Returns: Function symbol pred

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

Application of function symbol pred.

Parameters:

  • arg0 A data expression

Returns: Application of pred to a number of arguments

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

Generate identifier pred.

Returns: Identifier pred

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

Function for projecting out argument right from an application.

Parameters:

  • e A data expression

Pre: right is defined for e

Returns: The argument of e that corresponds to right

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

Constructor for function symbol sqrt.

Returns: Function symbol sqrt

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

Application of function symbol sqrt.

Parameters:

  • arg0 A data expression

Returns: Application of sqrt to a number of arguments

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

Generate identifier sqrt.

Returns: Identifier sqrt

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

Constructor for function symbol @sqrt_nat.

Returns: Function symbol sqrt_nat_aux_func

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

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

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

Generate identifier @sqrt_nat.

Returns: Identifier @sqrt_nat

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

Application of function symbol succ.

Parameters:

  • arg0 A data expression

Returns: Application of succ to a number of arguments

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

Generate identifier succ.

Returns: Identifier succ

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

Constructor for function symbol @swap_zero.

Returns: Function symbol swap_zero

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

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

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

Constructor for function symbol @swap_zero_add.

Returns: Function symbol swap_zero_add

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

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

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

Generate identifier @swap_zero_add.

Returns: Identifier @swap_zero_add

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

Constructor for function symbol @swap_zero_min.

Returns: Function symbol swap_zero_min

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

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

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

Generate identifier @swap_zero_min.

Returns: Identifier @swap_zero_min

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

Constructor for function symbol @swap_zero_monus.

Returns: Function symbol swap_zero_monus

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

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

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

Generate identifier @swap_zero_monus.

Returns: Identifier @swap_zero_monus

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

Generate identifier @swap_zero.

Returns: Identifier @swap_zero

function_symbol const &mcrl2::data::sort_nat::times(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_nat::times(const data_expression &arg0, const data_expression &arg1)

Application of function symbol *.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of * to a number of arguments

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

Generate identifier *.

Returns: Identifier *