nat64.h

Go to the documentation of this file.

// Author(s): Jeroen Keiren
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_DATA_NAT64_H
#define MCRL2_DATA_NAT64_H
 
#include "functional"    // std::function
#include "mcrl2/utilities/exception.h"
#include "mcrl2/data/basic_sort.h"
#include "mcrl2/data/function_sort.h"
#include "mcrl2/data/function_symbol.h"
#include "mcrl2/data/application.h"
#include "mcrl2/data/data_equation.h"
#include "mcrl2/data/standard.h"
#include "mcrl2/data/machine_word.h"
#include "mcrl2/data/bool.h"
#include "mcrl2/data/pos64.h"
 
namespace mcrl2 {
 
  namespace data {
 
    namespace sort_nat {
 
      inline
      const core::identifier_string& nat_name()
      {
        static core::identifier_string nat_name = core::identifier_string("Nat");
        return nat_name;
      }
 
      inline
      const basic_sort& nat()
      {
        static basic_sort nat = basic_sort(nat_name());
        return nat;
      }
 
      inline
      bool is_nat(const sort_expression& e)
      {
        if (is_basic_sort(e))
        {
          return basic_sort(e) == nat();
        }
        return false;
      }
 
      inline
      const core::identifier_string& natnatpair_name()
      {
        static core::identifier_string natnatpair_name = core::identifier_string("@NatNatPair");
        return natnatpair_name;
      }
 
      inline
      const basic_sort& natnatpair()
      {
        static basic_sort natnatpair = basic_sort(natnatpair_name());
        return natnatpair;
      }
 
      inline
      bool is_natnatpair(const sort_expression& e)
      {
        if (is_basic_sort(e))
        {
          return basic_sort(e) == natnatpair();
        }
        return false;
      }
 
 
      inline
      const core::identifier_string& c0_name()
      {
        static core::identifier_string c0_name = core::identifier_string("@c0");
        return c0_name;
      }
 
      
      inline
      const function_symbol& c0()
      {
        static function_symbol c0(c0_name(), nat());
        return c0;
      }
 
      inline
      bool is_c0_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == c0();
        }
        return false;
      }
 
      inline
      const core::identifier_string& succ_nat_name()
      {
        static core::identifier_string succ_nat_name = core::identifier_string("@succ_nat");
        return succ_nat_name;
      }
 
      
      inline
      const function_symbol& succ_nat()
      {
        static function_symbol succ_nat(succ_nat_name(), make_function_sort_(nat(), nat()));
        return succ_nat;
      }
 
      inline
      bool is_succ_nat_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == succ_nat();
        }
        return false;
      }
 
      
      inline
      application succ_nat(const data_expression& arg0)
      {
        return sort_nat::succ_nat()(arg0);
      }
 
      
      inline
      void make_succ_nat(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::succ_nat(),arg0);
      }
 
      inline
      bool is_succ_nat_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_succ_nat_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& nnpair_name()
      {
        static core::identifier_string nnpair_name = core::identifier_string("@nnPair");
        return nnpair_name;
      }
 
      
      inline
      const function_symbol& nnpair()
      {
        static function_symbol nnpair(nnpair_name(), make_function_sort_(nat(), nat(), natnatpair()));
        return nnpair;
      }
 
      inline
      bool is_nnpair_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == nnpair();
        }
        return false;
      }
 
      
      inline
      application nnpair(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::nnpair()(arg0, arg1);
      }
 
      
      inline
      void make_nnpair(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::nnpair(),arg0, arg1);
      }
 
      inline
      bool is_nnpair_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_nnpair_function_symbol(atermpp::down_cast<application>(e).head());
      }
      inline
      function_symbol_vector nat_generate_constructors_code()
      {
        function_symbol_vector result;
        result.push_back(sort_nat::c0());
        result.push_back(sort_nat::succ_nat());
        result.push_back(sort_nat::nnpair());
 
        return result;
      }
      inline
      function_symbol_vector nat_mCRL2_usable_constructors()
      {
        function_symbol_vector result;
        result.push_back(sort_nat::c0());
        result.push_back(sort_nat::succ_nat());
        result.push_back(sort_nat::nnpair());
 
        return result;
      }
      // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
      typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
      inline
      implementation_map nat_cpp_implementable_constructors()
      {
        implementation_map result;
        return result;
      }
 
      inline
      const core::identifier_string& most_significant_digit_nat_name()
      {
        static core::identifier_string most_significant_digit_nat_name = core::identifier_string("@most_significant_digitNat");
        return most_significant_digit_nat_name;
      }
 
      
      inline
      const function_symbol& most_significant_digit_nat()
      {
        static function_symbol most_significant_digit_nat(most_significant_digit_nat_name(), make_function_sort_(sort_machine_word::machine_word(), nat()));
        return most_significant_digit_nat;
      }
 
      inline
      bool is_most_significant_digit_nat_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == most_significant_digit_nat();
        }
        return false;
      }
 
      
      inline
      application most_significant_digit_nat(const data_expression& arg0)
      {
        return sort_nat::most_significant_digit_nat()(arg0);
      }
 
      
      inline
      void make_most_significant_digit_nat(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::most_significant_digit_nat(),arg0);
      }
 
      inline
      bool is_most_significant_digit_nat_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_most_significant_digit_nat_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& concat_digit_name()
      {
        static core::identifier_string concat_digit_name = core::identifier_string("@concat_digit");
        return concat_digit_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol concat_digit(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == nat() && s1 == sort_machine_word::machine_word())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_machine_word::machine_word())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for concat_digit with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol concat_digit(concat_digit_name(), make_function_sort_(s0, s1, target_sort));
        return concat_digit;
      }
 
      inline
      bool is_concat_digit_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == concat_digit_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == concat_digit(nat(), sort_machine_word::machine_word()) || f == concat_digit(sort_pos::pos(), sort_machine_word::machine_word()));
        }
        return false;
      }
 
      
      inline
      application concat_digit(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::concat_digit(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_concat_digit(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::concat_digit(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_concat_digit_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_concat_digit_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& equals_zero_name()
      {
        static core::identifier_string equals_zero_name = core::identifier_string("@equals_zero");
        return equals_zero_name;
      }
 
      
      inline
      const function_symbol& equals_zero()
      {
        static function_symbol equals_zero(equals_zero_name(), make_function_sort_(nat(), sort_bool::bool_()));
        return equals_zero;
      }
 
      inline
      bool is_equals_zero_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == equals_zero();
        }
        return false;
      }
 
      
      inline
      application equals_zero(const data_expression& arg0)
      {
        return sort_nat::equals_zero()(arg0);
      }
 
      
      inline
      void make_equals_zero(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::equals_zero(),arg0);
      }
 
      inline
      bool is_equals_zero_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_equals_zero_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& not_equals_zero_name()
      {
        static core::identifier_string not_equals_zero_name = core::identifier_string("@not_equals_zero");
        return not_equals_zero_name;
      }
 
      
      inline
      const function_symbol& not_equals_zero()
      {
        static function_symbol not_equals_zero(not_equals_zero_name(), make_function_sort_(nat(), sort_bool::bool_()));
        return not_equals_zero;
      }
 
      inline
      bool is_not_equals_zero_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == not_equals_zero();
        }
        return false;
      }
 
      
      inline
      application not_equals_zero(const data_expression& arg0)
      {
        return sort_nat::not_equals_zero()(arg0);
      }
 
      
      inline
      void make_not_equals_zero(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::not_equals_zero(),arg0);
      }
 
      inline
      bool is_not_equals_zero_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_not_equals_zero_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& equals_one_name()
      {
        static core::identifier_string equals_one_name = core::identifier_string("@equals_one");
        return equals_one_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol equals_one(const sort_expression& s0)
      {
        sort_expression target_sort(sort_bool::bool_());
        function_symbol equals_one(equals_one_name(), make_function_sort_(s0, target_sort));
        return equals_one;
      }
 
      inline
      bool is_equals_one_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == equals_one_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == equals_one(nat()) || f == equals_one(sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application equals_one(const data_expression& arg0)
      {
        return sort_nat::equals_one(arg0.sort())(arg0);
      }
 
      
      inline
      void make_equals_one(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::equals_one(arg0.sort()),arg0);
      }
 
      inline
      bool is_equals_one_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_equals_one_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& pos2nat_name()
      {
        static core::identifier_string pos2nat_name = core::identifier_string("Pos2Nat");
        return pos2nat_name;
      }
 
      
      inline
      const function_symbol& pos2nat()
      {
        static function_symbol pos2nat(pos2nat_name(), make_function_sort_(sort_pos::pos(), nat()));
        return pos2nat;
      }
 
      inline
      bool is_pos2nat_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == pos2nat();
        }
        return false;
      }
 
      
      inline
      application pos2nat(const data_expression& arg0)
      {
        return sort_nat::pos2nat()(arg0);
      }
 
      
      inline
      void make_pos2nat(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::pos2nat(),arg0);
      }
 
      inline
      bool is_pos2nat_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_pos2nat_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& nat2pos_name()
      {
        static core::identifier_string nat2pos_name = core::identifier_string("Nat2Pos");
        return nat2pos_name;
      }
 
      
      inline
      const function_symbol& nat2pos()
      {
        static function_symbol nat2pos(nat2pos_name(), make_function_sort_(nat(), sort_pos::pos()));
        return nat2pos;
      }
 
      inline
      bool is_nat2pos_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == nat2pos();
        }
        return false;
      }
 
      
      inline
      application nat2pos(const data_expression& arg0)
      {
        return sort_nat::nat2pos()(arg0);
      }
 
      
      inline
      void make_nat2pos(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::nat2pos(),arg0);
      }
 
      inline
      bool is_nat2pos_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_nat2pos_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& succ_name()
      {
        static core::identifier_string succ_name = core::identifier_string("succ");
        return succ_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol succ(const sort_expression& s0)
      {
        sort_expression target_sort(sort_pos::pos());
        function_symbol succ(succ_name(), make_function_sort_(s0, target_sort));
        return succ;
      }
 
      inline
      bool is_succ_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == succ_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == succ(nat()) || f == succ(sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application succ(const data_expression& arg0)
      {
        return sort_nat::succ(arg0.sort())(arg0);
      }
 
      
      inline
      void make_succ(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::succ(arg0.sort()),arg0);
      }
 
      inline
      bool is_succ_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& maximum_name()
      {
        static core::identifier_string maximum_name = core::identifier_string("max");
        return maximum_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == sort_pos::pos() && s1 == nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == nat() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol maximum(maximum_name(), make_function_sort_(s0, s1, target_sort));
        return maximum;
      }
 
      inline
      bool is_maximum_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == maximum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == maximum(sort_pos::pos(), nat()) || f == maximum(nat(), sort_pos::pos()) || f == maximum(nat(), nat()) || f == maximum(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application maximum(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::maximum(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_maximum_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& minimum_name()
      {
        static core::identifier_string minimum_name = core::identifier_string("min");
        return minimum_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol minimum(minimum_name(), make_function_sort_(s0, s1, target_sort));
        return minimum;
      }
 
      inline
      bool is_minimum_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == minimum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minimum(nat(), nat()) || f == minimum(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application minimum(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::minimum(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_minimum_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& pred_name()
      {
        static core::identifier_string pred_name = core::identifier_string("pred");
        return pred_name;
      }
 
      
      inline
      const function_symbol& pred()
      {
        static function_symbol pred(pred_name(), make_function_sort_(sort_pos::pos(), nat()));
        return pred;
      }
 
      inline
      bool is_pred_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == pred();
        }
        return false;
      }
 
      
      inline
      application pred(const data_expression& arg0)
      {
        return sort_nat::pred()(arg0);
      }
 
      
      inline
      void make_pred(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::pred(),arg0);
      }
 
      inline
      bool is_pred_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& pred_whr_name()
      {
        static core::identifier_string pred_whr_name = core::identifier_string("@pred_whr");
        return pred_whr_name;
      }
 
      
      inline
      const function_symbol& pred_whr()
      {
        static function_symbol pred_whr(pred_whr_name(), make_function_sort_(nat(), nat()));
        return pred_whr;
      }
 
      inline
      bool is_pred_whr_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == pred_whr();
        }
        return false;
      }
 
      
      inline
      application pred_whr(const data_expression& arg0)
      {
        return sort_nat::pred_whr()(arg0);
      }
 
      
      inline
      void make_pred_whr(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::pred_whr(),arg0);
      }
 
      inline
      bool is_pred_whr_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_pred_whr_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& plus_name()
      {
        static core::identifier_string plus_name = core::identifier_string("+");
        return plus_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol plus(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == sort_pos::pos() && s1 == nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == nat() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
        return plus;
      }
 
      inline
      bool is_plus_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == plus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == plus(sort_pos::pos(), nat()) || f == plus(nat(), sort_pos::pos()) || f == plus(nat(), nat()) || f == plus(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application plus(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::plus(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::plus(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_plus_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& add_with_carry_name()
      {
        static core::identifier_string add_with_carry_name = core::identifier_string("@add_with_carry");
        return add_with_carry_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol add_with_carry(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for add_with_carry with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol add_with_carry(add_with_carry_name(), make_function_sort_(s0, s1, target_sort));
        return add_with_carry;
      }
 
      inline
      bool is_add_with_carry_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == add_with_carry_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == add_with_carry(nat(), nat()) || f == add_with_carry(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application add_with_carry(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::add_with_carry(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_add_with_carry(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::add_with_carry(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_add_with_carry_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_add_with_carry_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& auxiliary_plus_nat_name()
      {
        static core::identifier_string auxiliary_plus_nat_name = core::identifier_string("@plus_nat");
        return auxiliary_plus_nat_name;
      }
 
      
      inline
      const function_symbol& auxiliary_plus_nat()
      {
        static function_symbol auxiliary_plus_nat(auxiliary_plus_nat_name(), make_function_sort_(nat(), nat(), nat()));
        return auxiliary_plus_nat;
      }
 
      inline
      bool is_auxiliary_plus_nat_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == auxiliary_plus_nat();
        }
        return false;
      }
 
      
      inline
      application auxiliary_plus_nat(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::auxiliary_plus_nat()(arg0, arg1);
      }
 
      
      inline
      void make_auxiliary_plus_nat(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::auxiliary_plus_nat(),arg0, arg1);
      }
 
      inline
      bool is_auxiliary_plus_nat_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_auxiliary_plus_nat_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& times_name()
      {
        static core::identifier_string times_name = core::identifier_string("*");
        return times_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol times(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
        return times;
      }
 
      inline
      bool is_times_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == times_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times(nat(), nat()) || f == times(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application times(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::times(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::times(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_times_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& times_ordered_name()
      {
        static core::identifier_string times_ordered_name = core::identifier_string("@times_ordered");
        return times_ordered_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol times_ordered(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for times_ordered with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol times_ordered(times_ordered_name(), make_function_sort_(s0, s1, target_sort));
        return times_ordered;
      }
 
      inline
      bool is_times_ordered_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == times_ordered_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times_ordered(nat(), nat()) || f == times_ordered(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application times_ordered(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::times_ordered(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_times_ordered(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::times_ordered(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_times_ordered_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_ordered_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& times_overflow_name()
      {
        static core::identifier_string times_overflow_name = core::identifier_string("@times_overflow");
        return times_overflow_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol times_overflow(const sort_expression& s0, const sort_expression& s1, const sort_expression& s2)
      {
        sort_expression target_sort;
        if (s0 == nat() && s1 == sort_machine_word::machine_word() && s2 == sort_machine_word::machine_word())
        {
          target_sort = nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_machine_word::machine_word() && s2 == sort_machine_word::machine_word())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for times_overflow with domain sorts " + pp(s0) + ", " + pp(s1) + ", " + pp(s2) + ". ");
        }
 
        function_symbol times_overflow(times_overflow_name(), make_function_sort_(s0, s1, s2, target_sort));
        return times_overflow;
      }
 
      inline
      bool is_times_overflow_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == times_overflow_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 3 && (f == times_overflow(nat(), sort_machine_word::machine_word(), sort_machine_word::machine_word()) || f == times_overflow(sort_pos::pos(), sort_machine_word::machine_word(), sort_machine_word::machine_word()));
        }
        return false;
      }
 
      
      inline
      application times_overflow(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::times_overflow(arg0.sort(), arg1.sort(), arg2.sort())(arg0, arg1, arg2);
      }
 
      
      inline
      void make_times_overflow(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::times_overflow(arg0.sort(), arg1.sort(), arg2.sort()),arg0, arg1, arg2);
      }
 
      inline
      bool is_times_overflow_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_overflow_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& div_name()
      {
        static core::identifier_string div_name = core::identifier_string("div");
        return div_name;
      }
 
      
      inline
      const function_symbol& div()
      {
        static function_symbol div(div_name(), make_function_sort_(nat(), sort_pos::pos(), nat()));
        return div;
      }
 
      inline
      bool is_div_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div();
        }
        return false;
      }
 
      
      inline
      application div(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::div()(arg0, arg1);
      }
 
      
      inline
      void make_div(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::div(),arg0, arg1);
      }
 
      inline
      bool is_div_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& mod_name()
      {
        static core::identifier_string mod_name = core::identifier_string("mod");
        return mod_name;
      }
 
      
      inline
      const function_symbol& mod()
      {
        static function_symbol mod(mod_name(), make_function_sort_(nat(), sort_pos::pos(), nat()));
        return mod;
      }
 
      inline
      bool is_mod_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == mod();
        }
        return false;
      }
 
      
      inline
      application mod(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::mod()(arg0, arg1);
      }
 
      
      inline
      void make_mod(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::mod(),arg0, arg1);
      }
 
      inline
      bool is_mod_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_mod_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_name()
      {
        static core::identifier_string exp_name = core::identifier_string("exp");
        return exp_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol exp(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == sort_pos::pos() && s1 == nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == nat() && s1 == nat())
        {
          target_sort = nat();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
        return exp;
      }
 
      inline
      bool is_exp_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == exp_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == exp(sort_pos::pos(), nat()) || f == exp(nat(), nat()));
        }
        return false;
      }
 
      
      inline
      application exp(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::exp(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_exp(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::exp(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_exp_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_name()
      {
        static core::identifier_string sqrt_name = core::identifier_string("sqrt");
        return sqrt_name;
      }
 
      
      inline
      const function_symbol& sqrt()
      {
        static function_symbol sqrt(sqrt_name(), make_function_sort_(nat(), nat()));
        return sqrt;
      }
 
      inline
      bool is_sqrt_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt();
        }
        return false;
      }
 
      
      inline
      application sqrt(const data_expression& arg0)
      {
        return sort_nat::sqrt()(arg0);
      }
 
      
      inline
      void make_sqrt(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::sqrt(),arg0);
      }
 
      inline
      bool is_sqrt_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& natpred_name()
      {
        static core::identifier_string natpred_name = core::identifier_string("@natpred");
        return natpred_name;
      }
 
      
      inline
      const function_symbol& natpred()
      {
        static function_symbol natpred(natpred_name(), make_function_sort_(nat(), nat()));
        return natpred;
      }
 
      inline
      bool is_natpred_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == natpred();
        }
        return false;
      }
 
      
      inline
      application natpred(const data_expression& arg0)
      {
        return sort_nat::natpred()(arg0);
      }
 
      
      inline
      void make_natpred(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::natpred(),arg0);
      }
 
      inline
      bool is_natpred_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_natpred_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& is_odd_name()
      {
        static core::identifier_string is_odd_name = core::identifier_string("@is_odd");
        return is_odd_name;
      }
 
      
      inline
      const function_symbol& is_odd()
      {
        static function_symbol is_odd(is_odd_name(), make_function_sort_(nat(), sort_bool::bool_()));
        return is_odd;
      }
 
      inline
      bool is_is_odd_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == is_odd();
        }
        return false;
      }
 
      
      inline
      application is_odd(const data_expression& arg0)
      {
        return sort_nat::is_odd()(arg0);
      }
 
      
      inline
      void make_is_odd(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::is_odd(),arg0);
      }
 
      inline
      bool is_is_odd_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_is_odd_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& div2_name()
      {
        static core::identifier_string div2_name = core::identifier_string("@div2");
        return div2_name;
      }
 
      
      inline
      const function_symbol& div2()
      {
        static function_symbol div2(div2_name(), make_function_sort_(nat(), nat()));
        return div2;
      }
 
      inline
      bool is_div2_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div2();
        }
        return false;
      }
 
      
      inline
      application div2(const data_expression& arg0)
      {
        return sort_nat::div2()(arg0);
      }
 
      
      inline
      void make_div2(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::div2(),arg0);
      }
 
      inline
      bool is_div2_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div2_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& monus_name()
      {
        static core::identifier_string monus_name = core::identifier_string("@monus");
        return monus_name;
      }
 
      
      inline
      const function_symbol& monus()
      {
        static function_symbol monus(monus_name(), make_function_sort_(nat(), nat(), nat()));
        return monus;
      }
 
      inline
      bool is_monus_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == monus();
        }
        return false;
      }
 
      
      inline
      application monus(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::monus()(arg0, arg1);
      }
 
      
      inline
      void make_monus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::monus(),arg0, arg1);
      }
 
      inline
      bool is_monus_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_monus_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& monus_whr_name()
      {
        static core::identifier_string monus_whr_name = core::identifier_string("@monus_whr");
        return monus_whr_name;
      }
 
      
      inline
      const function_symbol& monus_whr()
      {
        static function_symbol monus_whr(monus_whr_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), nat(), sort_machine_word::machine_word(), nat(), nat()));
        return monus_whr;
      }
 
      inline
      bool is_monus_whr_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == monus_whr();
        }
        return false;
      }
 
      
      inline
      application monus_whr(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::monus_whr()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::monus_whr(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_monus_whr_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_monus_whr_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_aux3p_name()
      {
        static core::identifier_string exp_aux3p_name = core::identifier_string("@exp_aux3p");
        return exp_aux3p_name;
      }
 
      
      inline
      const function_symbol& exp_aux3p()
      {
        static function_symbol exp_aux3p(exp_aux3p_name(), make_function_sort_(sort_bool::bool_(), sort_pos::pos(), sort_machine_word::machine_word(), sort_pos::pos()));
        return exp_aux3p;
      }
 
      inline
      bool is_exp_aux3p_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_aux3p();
        }
        return false;
      }
 
      
      inline
      application exp_aux3p(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::exp_aux3p()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_exp_aux3p(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::exp_aux3p(),arg0, arg1, arg2);
      }
 
      inline
      bool is_exp_aux3p_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_aux3p_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_aux4p_name()
      {
        static core::identifier_string exp_aux4p_name = core::identifier_string("@exp_aux4p");
        return exp_aux4p_name;
      }
 
      
      inline
      const function_symbol& exp_aux4p()
      {
        static function_symbol exp_aux4p(exp_aux4p_name(), make_function_sort_(sort_bool::bool_(), sort_pos::pos(), nat(), sort_machine_word::machine_word(), sort_pos::pos()));
        return exp_aux4p;
      }
 
      inline
      bool is_exp_aux4p_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_aux4p();
        }
        return false;
      }
 
      
      inline
      application exp_aux4p(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::exp_aux4p()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_exp_aux4p(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_nat::exp_aux4p(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_exp_aux4p_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_aux4p_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_aux3n_name()
      {
        static core::identifier_string exp_aux3n_name = core::identifier_string("@exp_aux3n");
        return exp_aux3n_name;
      }
 
      
      inline
      const function_symbol& exp_aux3n()
      {
        static function_symbol exp_aux3n(exp_aux3n_name(), make_function_sort_(sort_bool::bool_(), nat(), sort_machine_word::machine_word(), nat()));
        return exp_aux3n;
      }
 
      inline
      bool is_exp_aux3n_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_aux3n();
        }
        return false;
      }
 
      
      inline
      application exp_aux3n(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::exp_aux3n()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_exp_aux3n(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::exp_aux3n(),arg0, arg1, arg2);
      }
 
      inline
      bool is_exp_aux3n_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_aux3n_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_aux4n_name()
      {
        static core::identifier_string exp_aux4n_name = core::identifier_string("@exp_aux4n");
        return exp_aux4n_name;
      }
 
      
      inline
      const function_symbol& exp_aux4n()
      {
        static function_symbol exp_aux4n(exp_aux4n_name(), make_function_sort_(sort_bool::bool_(), nat(), nat(), sort_machine_word::machine_word(), nat()));
        return exp_aux4n;
      }
 
      inline
      bool is_exp_aux4n_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_aux4n();
        }
        return false;
      }
 
      
      inline
      application exp_aux4n(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::exp_aux4n()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_exp_aux4n(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_nat::exp_aux4n(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_exp_aux4n_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_aux4n_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_auxtruep_name()
      {
        static core::identifier_string exp_auxtruep_name = core::identifier_string("@exp_auxtruep");
        return exp_auxtruep_name;
      }
 
      
      inline
      const function_symbol& exp_auxtruep()
      {
        static function_symbol exp_auxtruep(exp_auxtruep_name(), make_function_sort_(sort_pos::pos(), nat(), sort_machine_word::machine_word(), nat()));
        return exp_auxtruep;
      }
 
      inline
      bool is_exp_auxtruep_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_auxtruep();
        }
        return false;
      }
 
      
      inline
      application exp_auxtruep(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::exp_auxtruep()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_exp_auxtruep(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::exp_auxtruep(),arg0, arg1, arg2);
      }
 
      inline
      bool is_exp_auxtruep_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_auxtruep_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_auxtruen_name()
      {
        static core::identifier_string exp_auxtruen_name = core::identifier_string("@exp_auxtruen");
        return exp_auxtruen_name;
      }
 
      
      inline
      const function_symbol& exp_auxtruen()
      {
        static function_symbol exp_auxtruen(exp_auxtruen_name(), make_function_sort_(nat(), nat(), sort_machine_word::machine_word(), nat()));
        return exp_auxtruen;
      }
 
      inline
      bool is_exp_auxtruen_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_auxtruen();
        }
        return false;
      }
 
      
      inline
      application exp_auxtruen(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::exp_auxtruen()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_exp_auxtruen(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::exp_auxtruen(),arg0, arg1, arg2);
      }
 
      inline
      bool is_exp_auxtruen_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_auxtruen_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_auxfalsep_name()
      {
        static core::identifier_string exp_auxfalsep_name = core::identifier_string("@exp_auxfalsep");
        return exp_auxfalsep_name;
      }
 
      
      inline
      const function_symbol& exp_auxfalsep()
      {
        static function_symbol exp_auxfalsep(exp_auxfalsep_name(), make_function_sort_(sort_pos::pos(), nat(), sort_machine_word::machine_word(), nat()));
        return exp_auxfalsep;
      }
 
      inline
      bool is_exp_auxfalsep_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_auxfalsep();
        }
        return false;
      }
 
      
      inline
      application exp_auxfalsep(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::exp_auxfalsep()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_exp_auxfalsep(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::exp_auxfalsep(),arg0, arg1, arg2);
      }
 
      inline
      bool is_exp_auxfalsep_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_auxfalsep_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_auxfalsen_name()
      {
        static core::identifier_string exp_auxfalsen_name = core::identifier_string("@exp_auxfalsen");
        return exp_auxfalsen_name;
      }
 
      
      inline
      const function_symbol& exp_auxfalsen()
      {
        static function_symbol exp_auxfalsen(exp_auxfalsen_name(), make_function_sort_(nat(), nat(), sort_machine_word::machine_word(), nat()));
        return exp_auxfalsen;
      }
 
      inline
      bool is_exp_auxfalsen_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == exp_auxfalsen();
        }
        return false;
      }
 
      
      inline
      application exp_auxfalsen(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::exp_auxfalsen()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_exp_auxfalsen(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::exp_auxfalsen(),arg0, arg1, arg2);
      }
 
      inline
      bool is_exp_auxfalsen_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_auxfalsen_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& div_bold_name()
      {
        static core::identifier_string div_bold_name = core::identifier_string("@div_bold");
        return div_bold_name;
      }
 
      
      inline
      const function_symbol& div_bold()
      {
        static function_symbol div_bold(div_bold_name(), make_function_sort_(nat(), sort_pos::pos(), sort_machine_word::machine_word()));
        return div_bold;
      }
 
      inline
      bool is_div_bold_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_bold();
        }
        return false;
      }
 
      
      inline
      application div_bold(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::div_bold()(arg0, arg1);
      }
 
      
      inline
      void make_div_bold(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::div_bold(),arg0, arg1);
      }
 
      inline
      bool is_div_bold_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_bold_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& div_bold_whr_name()
      {
        static core::identifier_string div_bold_whr_name = core::identifier_string("@div_bold_whr");
        return div_bold_whr_name;
      }
 
      
      inline
      const function_symbol& div_bold_whr()
      {
        static function_symbol div_bold_whr(div_bold_whr_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), sort_pos::pos(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word()));
        return div_bold_whr;
      }
 
      inline
      bool is_div_bold_whr_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_bold_whr();
        }
        return false;
      }
 
      
      inline
      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)
      {
        return sort_nat::div_bold_whr()(arg0, arg1, arg2, arg3, arg4, arg5);
      }
 
      
      inline
      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_application(result, sort_nat::div_bold_whr(),arg0, arg1, arg2, arg3, arg4, arg5);
      }
 
      inline
      bool is_div_bold_whr_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_bold_whr_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& div_whr1_name()
      {
        static core::identifier_string div_whr1_name = core::identifier_string("@div_whr1");
        return div_whr1_name;
      }
 
      
      inline
      const function_symbol& div_whr1()
      {
        static function_symbol div_whr1(div_whr1_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), natnatpair(), nat()));
        return div_whr1;
      }
 
      inline
      bool is_div_whr1_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_whr1();
        }
        return false;
      }
 
      
      inline
      application div_whr1(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::div_whr1()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_div_whr1(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_nat::div_whr1(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_div_whr1_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_whr1_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& div_whr2_name()
      {
        static core::identifier_string div_whr2_name = core::identifier_string("@div_whr2");
        return div_whr2_name;
      }
 
      
      inline
      const function_symbol& div_whr2()
      {
        static function_symbol div_whr2(div_whr2_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), sort_pos::pos(), sort_machine_word::machine_word(), natnatpair(), nat()));
        return div_whr2;
      }
 
      inline
      bool is_div_whr2_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_whr2();
        }
        return false;
      }
 
      
      inline
      application div_whr2(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::div_whr2()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::div_whr2(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_div_whr2_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_whr2_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& mod_whr1_name()
      {
        static core::identifier_string mod_whr1_name = core::identifier_string("@mod_whr1");
        return mod_whr1_name;
      }
 
      
      inline
      const function_symbol& mod_whr1()
      {
        static function_symbol mod_whr1(mod_whr1_name(), make_function_sort_(sort_machine_word::machine_word(), sort_pos::pos(), sort_machine_word::machine_word(), nat(), nat()));
        return mod_whr1;
      }
 
      inline
      bool is_mod_whr1_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == mod_whr1();
        }
        return false;
      }
 
      
      inline
      application mod_whr1(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::mod_whr1()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_mod_whr1(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_nat::mod_whr1(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_mod_whr1_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_mod_whr1_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_name()
      {
        static core::identifier_string divmod_aux_name = core::identifier_string("@divmod_aux");
        return divmod_aux_name;
      }
 
      
      inline
      const function_symbol& divmod_aux()
      {
        static function_symbol divmod_aux(divmod_aux_name(), make_function_sort_(nat(), sort_pos::pos(), natnatpair()));
        return divmod_aux;
      }
 
      inline
      bool is_divmod_aux_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux();
        }
        return false;
      }
 
      
      inline
      application divmod_aux(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::divmod_aux()(arg0, arg1);
      }
 
      
      inline
      void make_divmod_aux(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::divmod_aux(),arg0, arg1);
      }
 
      inline
      bool is_divmod_aux_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_whr1_name()
      {
        static core::identifier_string divmod_aux_whr1_name = core::identifier_string("@divmod_aux_whr1");
        return divmod_aux_whr1_name;
      }
 
      
      inline
      const function_symbol& divmod_aux_whr1()
      {
        static function_symbol divmod_aux_whr1(divmod_aux_whr1_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), natnatpair(), natnatpair()));
        return divmod_aux_whr1;
      }
 
      inline
      bool is_divmod_aux_whr1_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux_whr1();
        }
        return false;
      }
 
      
      inline
      application divmod_aux_whr1(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::divmod_aux_whr1()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::divmod_aux_whr1(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_divmod_aux_whr1_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_whr1_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_whr2_name()
      {
        static core::identifier_string divmod_aux_whr2_name = core::identifier_string("@divmod_aux_whr2");
        return divmod_aux_whr2_name;
      }
 
      
      inline
      const function_symbol& divmod_aux_whr2()
      {
        static function_symbol divmod_aux_whr2(divmod_aux_whr2_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), sort_pos::pos(), sort_machine_word::machine_word(), nat(), natnatpair()));
        return divmod_aux_whr2;
      }
 
      inline
      bool is_divmod_aux_whr2_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux_whr2();
        }
        return false;
      }
 
      
      inline
      application divmod_aux_whr2(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::divmod_aux_whr2()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::divmod_aux_whr2(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_divmod_aux_whr2_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_whr2_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_whr3_name()
      {
        static core::identifier_string divmod_aux_whr3_name = core::identifier_string("@divmod_aux_whr3");
        return divmod_aux_whr3_name;
      }
 
      
      inline
      const function_symbol& divmod_aux_whr3()
      {
        static function_symbol divmod_aux_whr3(divmod_aux_whr3_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), sort_pos::pos(), sort_machine_word::machine_word(), nat(), natnatpair()));
        return divmod_aux_whr3;
      }
 
      inline
      bool is_divmod_aux_whr3_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux_whr3();
        }
        return false;
      }
 
      
      inline
      application divmod_aux_whr3(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::divmod_aux_whr3()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::divmod_aux_whr3(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_divmod_aux_whr3_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_whr3_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_whr4_name()
      {
        static core::identifier_string divmod_aux_whr4_name = core::identifier_string("@divmod_aux_whr4");
        return divmod_aux_whr4_name;
      }
 
      
      inline
      const function_symbol& divmod_aux_whr4()
      {
        static function_symbol divmod_aux_whr4(divmod_aux_whr4_name(), make_function_sort_(sort_machine_word::machine_word(), sort_pos::pos(), sort_machine_word::machine_word(), natnatpair(), natnatpair()));
        return divmod_aux_whr4;
      }
 
      inline
      bool is_divmod_aux_whr4_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux_whr4();
        }
        return false;
      }
 
      
      inline
      application divmod_aux_whr4(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::divmod_aux_whr4()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::divmod_aux_whr4(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_divmod_aux_whr4_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_whr4_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_whr5_name()
      {
        static core::identifier_string divmod_aux_whr5_name = core::identifier_string("@divmod_aux_whr5");
        return divmod_aux_whr5_name;
      }
 
      
      inline
      const function_symbol& divmod_aux_whr5()
      {
        static function_symbol divmod_aux_whr5(divmod_aux_whr5_name(), make_function_sort_(sort_pos::pos(), sort_machine_word::machine_word(), natnatpair(), nat(), natnatpair()));
        return divmod_aux_whr5;
      }
 
      inline
      bool is_divmod_aux_whr5_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux_whr5();
        }
        return false;
      }
 
      
      inline
      application divmod_aux_whr5(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::divmod_aux_whr5()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::divmod_aux_whr5(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_divmod_aux_whr5_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_whr5_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divmod_aux_whr6_name()
      {
        static core::identifier_string divmod_aux_whr6_name = core::identifier_string("@divmod_aux_whr6");
        return divmod_aux_whr6_name;
      }
 
      
      inline
      const function_symbol& divmod_aux_whr6()
      {
        static function_symbol divmod_aux_whr6(divmod_aux_whr6_name(), make_function_sort_(sort_pos::pos(), sort_machine_word::machine_word(), natnatpair(), nat(), nat(), natnatpair()));
        return divmod_aux_whr6;
      }
 
      inline
      bool is_divmod_aux_whr6_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == divmod_aux_whr6();
        }
        return false;
      }
 
      
      inline
      application divmod_aux_whr6(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::divmod_aux_whr6()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::divmod_aux_whr6(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_divmod_aux_whr6_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divmod_aux_whr6_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& msd_name()
      {
        static core::identifier_string msd_name = core::identifier_string("@msd");
        return msd_name;
      }
 
      
      inline
      const function_symbol& msd()
      {
        static function_symbol msd(msd_name(), make_function_sort_(nat(), sort_machine_word::machine_word()));
        return msd;
      }
 
      inline
      bool is_msd_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == msd();
        }
        return false;
      }
 
      
      inline
      application msd(const data_expression& arg0)
      {
        return sort_nat::msd()(arg0);
      }
 
      
      inline
      void make_msd(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::msd(),arg0);
      }
 
      inline
      bool is_msd_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_msd_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& swap_zero_name()
      {
        static core::identifier_string swap_zero_name = core::identifier_string("@swap_zero");
        return swap_zero_name;
      }
 
      
      inline
      const function_symbol& swap_zero()
      {
        static function_symbol swap_zero(swap_zero_name(), make_function_sort_(nat(), nat(), nat()));
        return swap_zero;
      }
 
      inline
      bool is_swap_zero_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == swap_zero();
        }
        return false;
      }
 
      
      inline
      application swap_zero(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_nat::swap_zero()(arg0, arg1);
      }
 
      
      inline
      void make_swap_zero(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_nat::swap_zero(),arg0, arg1);
      }
 
      inline
      bool is_swap_zero_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_swap_zero_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& swap_zero_add_name()
      {
        static core::identifier_string swap_zero_add_name = core::identifier_string("@swap_zero_add");
        return swap_zero_add_name;
      }
 
      
      inline
      const function_symbol& swap_zero_add()
      {
        static function_symbol swap_zero_add(swap_zero_add_name(), make_function_sort_(nat(), nat(), nat(), nat(), nat()));
        return swap_zero_add;
      }
 
      inline
      bool is_swap_zero_add_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == swap_zero_add();
        }
        return false;
      }
 
      
      inline
      application swap_zero_add(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::swap_zero_add()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::swap_zero_add(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_swap_zero_add_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_swap_zero_add_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& swap_zero_min_name()
      {
        static core::identifier_string swap_zero_min_name = core::identifier_string("@swap_zero_min");
        return swap_zero_min_name;
      }
 
      
      inline
      const function_symbol& swap_zero_min()
      {
        static function_symbol swap_zero_min(swap_zero_min_name(), make_function_sort_(nat(), nat(), nat(), nat(), nat()));
        return swap_zero_min;
      }
 
      inline
      bool is_swap_zero_min_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == swap_zero_min();
        }
        return false;
      }
 
      
      inline
      application swap_zero_min(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::swap_zero_min()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::swap_zero_min(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_swap_zero_min_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_swap_zero_min_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& swap_zero_monus_name()
      {
        static core::identifier_string swap_zero_monus_name = core::identifier_string("@swap_zero_monus");
        return swap_zero_monus_name;
      }
 
      
      inline
      const function_symbol& swap_zero_monus()
      {
        static function_symbol swap_zero_monus(swap_zero_monus_name(), make_function_sort_(nat(), nat(), nat(), nat(), nat()));
        return swap_zero_monus;
      }
 
      inline
      bool is_swap_zero_monus_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == swap_zero_monus();
        }
        return false;
      }
 
      
      inline
      application swap_zero_monus(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::swap_zero_monus()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::swap_zero_monus(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_swap_zero_monus_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_swap_zero_monus_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_whr1_name()
      {
        static core::identifier_string sqrt_whr1_name = core::identifier_string("@sqrt_whr1");
        return sqrt_whr1_name;
      }
 
      
      inline
      const function_symbol& sqrt_whr1()
      {
        static function_symbol sqrt_whr1(sqrt_whr1_name(), make_function_sort_(sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), nat()));
        return sqrt_whr1;
      }
 
      inline
      bool is_sqrt_whr1_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_whr1();
        }
        return false;
      }
 
      
      inline
      application sqrt_whr1(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::sqrt_whr1()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_sqrt_whr1(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_nat::sqrt_whr1(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_sqrt_whr1_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_whr1_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_whr2_name()
      {
        static core::identifier_string sqrt_whr2_name = core::identifier_string("@sqrt_whr2");
        return sqrt_whr2_name;
      }
 
      
      inline
      const function_symbol& sqrt_whr2()
      {
        static function_symbol sqrt_whr2(sqrt_whr2_name(), make_function_sort_(sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), nat()));
        return sqrt_whr2;
      }
 
      inline
      bool is_sqrt_whr2_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_whr2();
        }
        return false;
      }
 
      
      inline
      application sqrt_whr2(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::sqrt_whr2()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::sqrt_whr2(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_sqrt_whr2_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_whr2_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_name()
      {
        static core::identifier_string sqrt_pair_name = core::identifier_string("@sqrt_pair");
        return sqrt_pair_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair()
      {
        static function_symbol sqrt_pair(sqrt_pair_name(), make_function_sort_(nat(), natnatpair()));
        return sqrt_pair;
      }
 
      inline
      bool is_sqrt_pair_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair();
        }
        return false;
      }
 
      
      inline
      application sqrt_pair(const data_expression& arg0)
      {
        return sort_nat::sqrt_pair()(arg0);
      }
 
      
      inline
      void make_sqrt_pair(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::sqrt_pair(),arg0);
      }
 
      inline
      bool is_sqrt_pair_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_whr1_name()
      {
        static core::identifier_string sqrt_pair_whr1_name = core::identifier_string("@sqrt_pair_whr1");
        return sqrt_pair_whr1_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair_whr1()
      {
        static function_symbol sqrt_pair_whr1(sqrt_pair_whr1_name(), make_function_sort_(sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), nat(), natnatpair()));
        return sqrt_pair_whr1;
      }
 
      inline
      bool is_sqrt_pair_whr1_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair_whr1();
        }
        return false;
      }
 
      
      inline
      application sqrt_pair_whr1(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_nat::sqrt_pair_whr1()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      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_application(result, sort_nat::sqrt_pair_whr1(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_sqrt_pair_whr1_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_whr1_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_whr2_name()
      {
        static core::identifier_string sqrt_pair_whr2_name = core::identifier_string("@sqrt_pair_whr2");
        return sqrt_pair_whr2_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair_whr2()
      {
        static function_symbol sqrt_pair_whr2(sqrt_pair_whr2_name(), make_function_sort_(sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), sort_machine_word::machine_word(), nat(), natnatpair()));
        return sqrt_pair_whr2;
      }
 
      inline
      bool is_sqrt_pair_whr2_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair_whr2();
        }
        return false;
      }
 
      
      inline
      application sqrt_pair_whr2(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::sqrt_pair_whr2()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::sqrt_pair_whr2(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_sqrt_pair_whr2_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_whr2_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_whr3_name()
      {
        static core::identifier_string sqrt_pair_whr3_name = core::identifier_string("@sqrt_pair_whr3");
        return sqrt_pair_whr3_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair_whr3()
      {
        static function_symbol sqrt_pair_whr3(sqrt_pair_whr3_name(), make_function_sort_(sort_machine_word::machine_word(), sort_machine_word::machine_word(), natnatpair(), natnatpair()));
        return sqrt_pair_whr3;
      }
 
      inline
      bool is_sqrt_pair_whr3_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair_whr3();
        }
        return false;
      }
 
      
      inline
      application sqrt_pair_whr3(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::sqrt_pair_whr3()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_sqrt_pair_whr3(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::sqrt_pair_whr3(),arg0, arg1, arg2);
      }
 
      inline
      bool is_sqrt_pair_whr3_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_whr3_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_whr4_name()
      {
        static core::identifier_string sqrt_pair_whr4_name = core::identifier_string("@sqrt_pair_whr4");
        return sqrt_pair_whr4_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair_whr4()
      {
        static function_symbol sqrt_pair_whr4(sqrt_pair_whr4_name(), make_function_sort_(nat(), sort_machine_word::machine_word(), natnatpair(), nat(), nat(), nat(), natnatpair()));
        return sqrt_pair_whr4;
      }
 
      inline
      bool is_sqrt_pair_whr4_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair_whr4();
        }
        return false;
      }
 
      
      inline
      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)
      {
        return sort_nat::sqrt_pair_whr4()(arg0, arg1, arg2, arg3, arg4, arg5);
      }
 
      
      inline
      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_application(result, sort_nat::sqrt_pair_whr4(),arg0, arg1, arg2, arg3, arg4, arg5);
      }
 
      inline
      bool is_sqrt_pair_whr4_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_whr4_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_whr5_name()
      {
        static core::identifier_string sqrt_pair_whr5_name = core::identifier_string("@sqrt_pair_whr5");
        return sqrt_pair_whr5_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair_whr5()
      {
        static function_symbol sqrt_pair_whr5(sqrt_pair_whr5_name(), make_function_sort_(natnatpair(), nat(), nat(), nat(), nat(), natnatpair()));
        return sqrt_pair_whr5;
      }
 
      inline
      bool is_sqrt_pair_whr5_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair_whr5();
        }
        return false;
      }
 
      
      inline
      application sqrt_pair_whr5(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_nat::sqrt_pair_whr5()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      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_application(result, sort_nat::sqrt_pair_whr5(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_sqrt_pair_whr5_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_whr5_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& sqrt_pair_whr6_name()
      {
        static core::identifier_string sqrt_pair_whr6_name = core::identifier_string("@sqrt_pair_whr6");
        return sqrt_pair_whr6_name;
      }
 
      
      inline
      const function_symbol& sqrt_pair_whr6()
      {
        static function_symbol sqrt_pair_whr6(sqrt_pair_whr6_name(), make_function_sort_(nat(), nat(), nat(), natnatpair()));
        return sqrt_pair_whr6;
      }
 
      inline
      bool is_sqrt_pair_whr6_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_pair_whr6();
        }
        return false;
      }
 
      
      inline
      application sqrt_pair_whr6(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_nat::sqrt_pair_whr6()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_sqrt_pair_whr6(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_nat::sqrt_pair_whr6(),arg0, arg1, arg2);
      }
 
      inline
      bool is_sqrt_pair_whr6_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_pair_whr6_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& first_name()
      {
        static core::identifier_string first_name = core::identifier_string("@first");
        return first_name;
      }
 
      
      inline
      const function_symbol& first()
      {
        static function_symbol first(first_name(), make_function_sort_(natnatpair(), nat()));
        return first;
      }
 
      inline
      bool is_first_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == first();
        }
        return false;
      }
 
      
      inline
      application first(const data_expression& arg0)
      {
        return sort_nat::first()(arg0);
      }
 
      
      inline
      void make_first(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::first(),arg0);
      }
 
      inline
      bool is_first_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_first_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& last_name()
      {
        static core::identifier_string last_name = core::identifier_string("@last");
        return last_name;
      }
 
      
      inline
      const function_symbol& last()
      {
        static function_symbol last(last_name(), make_function_sort_(natnatpair(), nat()));
        return last;
      }
 
      inline
      bool is_last_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == last();
        }
        return false;
      }
 
      
      inline
      application last(const data_expression& arg0)
      {
        return sort_nat::last()(arg0);
      }
 
      
      inline
      void make_last(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_nat::last(),arg0);
      }
 
      inline
      bool is_last_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_last_function_symbol(atermpp::down_cast<application>(e).head());
      }
      inline
      function_symbol_vector nat_generate_functions_code()
      {
        function_symbol_vector result;
        result.push_back(sort_nat::most_significant_digit_nat());
        result.push_back(sort_nat::concat_digit(nat(), sort_machine_word::machine_word()));
        result.push_back(sort_nat::equals_zero());
        result.push_back(sort_nat::not_equals_zero());
        result.push_back(sort_nat::equals_one(nat()));
        result.push_back(sort_nat::pos2nat());
        result.push_back(sort_nat::nat2pos());
        result.push_back(sort_nat::succ(nat()));
        result.push_back(sort_nat::maximum(sort_pos::pos(), nat()));
        result.push_back(sort_nat::maximum(nat(), sort_pos::pos()));
        result.push_back(sort_nat::maximum(nat(), nat()));
        result.push_back(sort_nat::minimum(nat(), nat()));
        result.push_back(sort_nat::pred());
        result.push_back(sort_nat::pred_whr());
        result.push_back(sort_nat::plus(sort_pos::pos(), nat()));
        result.push_back(sort_nat::plus(nat(), sort_pos::pos()));
        result.push_back(sort_nat::plus(nat(), nat()));
        result.push_back(sort_nat::add_with_carry(nat(), nat()));
        result.push_back(sort_nat::auxiliary_plus_nat());
        result.push_back(sort_nat::times(nat(), nat()));
        result.push_back(sort_nat::times_ordered(nat(), nat()));
        result.push_back(sort_nat::times_overflow(nat(), sort_machine_word::machine_word(), sort_machine_word::machine_word()));
        result.push_back(sort_nat::div());
        result.push_back(sort_nat::mod());
        result.push_back(sort_nat::exp(sort_pos::pos(), nat()));
        result.push_back(sort_nat::exp(nat(), nat()));
        result.push_back(sort_nat::sqrt());
        result.push_back(sort_nat::natpred());
        result.push_back(sort_nat::is_odd());
        result.push_back(sort_nat::div2());
        result.push_back(sort_nat::monus());
        result.push_back(sort_nat::monus_whr());
        result.push_back(sort_nat::exp_aux3p());
        result.push_back(sort_nat::exp_aux4p());
        result.push_back(sort_nat::exp_aux3n());
        result.push_back(sort_nat::exp_aux4n());
        result.push_back(sort_nat::exp_auxtruep());
        result.push_back(sort_nat::exp_auxtruen());
        result.push_back(sort_nat::exp_auxfalsep());
        result.push_back(sort_nat::exp_auxfalsen());
        result.push_back(sort_nat::div_bold());
        result.push_back(sort_nat::div_bold_whr());
        result.push_back(sort_nat::div_whr1());
        result.push_back(sort_nat::div_whr2());
        result.push_back(sort_nat::mod_whr1());
        result.push_back(sort_nat::divmod_aux());
        result.push_back(sort_nat::divmod_aux_whr1());
        result.push_back(sort_nat::divmod_aux_whr2());
        result.push_back(sort_nat::divmod_aux_whr3());
        result.push_back(sort_nat::divmod_aux_whr4());
        result.push_back(sort_nat::divmod_aux_whr5());
        result.push_back(sort_nat::divmod_aux_whr6());
        result.push_back(sort_nat::msd());
        result.push_back(sort_nat::swap_zero());
        result.push_back(sort_nat::swap_zero_add());
        result.push_back(sort_nat::swap_zero_min());
        result.push_back(sort_nat::swap_zero_monus());
        result.push_back(sort_nat::sqrt_whr1());
        result.push_back(sort_nat::sqrt_whr2());
        result.push_back(sort_nat::sqrt_pair());
        result.push_back(sort_nat::sqrt_pair_whr1());
        result.push_back(sort_nat::sqrt_pair_whr2());
        result.push_back(sort_nat::sqrt_pair_whr3());
        result.push_back(sort_nat::sqrt_pair_whr4());
        result.push_back(sort_nat::sqrt_pair_whr5());
        result.push_back(sort_nat::sqrt_pair_whr6());
        result.push_back(sort_nat::first());
        result.push_back(sort_nat::last());
        return result;
      }
      
      inline
      function_symbol_vector nat_generate_constructors_and_functions_code()
      {
        function_symbol_vector result=nat_generate_functions_code();
        for(const function_symbol& f: nat_generate_constructors_code())
        {
          result.push_back(f);
        }
        return result;
      }
      
      inline
      function_symbol_vector nat_mCRL2_usable_mappings()
      {
        function_symbol_vector result;
        result.push_back(sort_nat::most_significant_digit_nat());
        result.push_back(sort_nat::concat_digit(nat(), sort_machine_word::machine_word()));
        result.push_back(sort_nat::equals_zero());
        result.push_back(sort_nat::not_equals_zero());
        result.push_back(sort_nat::equals_one(nat()));
        result.push_back(sort_nat::pos2nat());
        result.push_back(sort_nat::nat2pos());
        result.push_back(sort_nat::succ(nat()));
        result.push_back(sort_nat::maximum(sort_pos::pos(), nat()));
        result.push_back(sort_nat::maximum(nat(), sort_pos::pos()));
        result.push_back(sort_nat::maximum(nat(), nat()));
        result.push_back(sort_nat::minimum(nat(), nat()));
        result.push_back(sort_nat::pred());
        result.push_back(sort_nat::pred_whr());
        result.push_back(sort_nat::plus(sort_pos::pos(), nat()));
        result.push_back(sort_nat::plus(nat(), sort_pos::pos()));
        result.push_back(sort_nat::plus(nat(), nat()));
        result.push_back(sort_nat::add_with_carry(nat(), nat()));
        result.push_back(sort_nat::auxiliary_plus_nat());
        result.push_back(sort_nat::times(nat(), nat()));
        result.push_back(sort_nat::times_ordered(nat(), nat()));
        result.push_back(sort_nat::times_overflow(nat(), sort_machine_word::machine_word(), sort_machine_word::machine_word()));
        result.push_back(sort_nat::div());
        result.push_back(sort_nat::mod());
        result.push_back(sort_nat::exp(sort_pos::pos(), nat()));
        result.push_back(sort_nat::exp(nat(), nat()));
        result.push_back(sort_nat::sqrt());
        result.push_back(sort_nat::natpred());
        result.push_back(sort_nat::is_odd());
        result.push_back(sort_nat::div2());
        result.push_back(sort_nat::monus());
        result.push_back(sort_nat::monus_whr());
        result.push_back(sort_nat::exp_aux3p());
        result.push_back(sort_nat::exp_aux4p());
        result.push_back(sort_nat::exp_aux3n());
        result.push_back(sort_nat::exp_aux4n());
        result.push_back(sort_nat::exp_auxtruep());
        result.push_back(sort_nat::exp_auxtruen());
        result.push_back(sort_nat::exp_auxfalsep());
        result.push_back(sort_nat::exp_auxfalsen());
        result.push_back(sort_nat::div_bold());
        result.push_back(sort_nat::div_bold_whr());
        result.push_back(sort_nat::div_whr1());
        result.push_back(sort_nat::div_whr2());
        result.push_back(sort_nat::mod_whr1());
        result.push_back(sort_nat::divmod_aux());
        result.push_back(sort_nat::divmod_aux_whr1());
        result.push_back(sort_nat::divmod_aux_whr2());
        result.push_back(sort_nat::divmod_aux_whr3());
        result.push_back(sort_nat::divmod_aux_whr4());
        result.push_back(sort_nat::divmod_aux_whr5());
        result.push_back(sort_nat::divmod_aux_whr6());
        result.push_back(sort_nat::msd());
        result.push_back(sort_nat::swap_zero());
        result.push_back(sort_nat::swap_zero_add());
        result.push_back(sort_nat::swap_zero_min());
        result.push_back(sort_nat::swap_zero_monus());
        result.push_back(sort_nat::sqrt_whr1());
        result.push_back(sort_nat::sqrt_whr2());
        result.push_back(sort_nat::sqrt_pair());
        result.push_back(sort_nat::sqrt_pair_whr1());
        result.push_back(sort_nat::sqrt_pair_whr2());
        result.push_back(sort_nat::sqrt_pair_whr3());
        result.push_back(sort_nat::sqrt_pair_whr4());
        result.push_back(sort_nat::sqrt_pair_whr5());
        result.push_back(sort_nat::sqrt_pair_whr6());
        result.push_back(sort_nat::first());
        result.push_back(sort_nat::last());
        return result;
      }
 
 
      // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
      typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
      inline
      implementation_map nat_cpp_implementable_mappings()
      {
        implementation_map result;
        return result;
      }
      inline
      const data_expression& arg(const data_expression& e)
      {
        assert(is_succ_nat_application(e) || is_most_significant_digit_nat_application(e) || is_equals_zero_application(e) || is_not_equals_zero_application(e) || is_equals_one_application(e) || is_pos2nat_application(e) || is_nat2pos_application(e) || is_succ_application(e) || is_pred_application(e) || is_pred_whr_application(e) || is_sqrt_application(e) || is_natpred_application(e) || is_is_odd_application(e) || is_div2_application(e) || is_msd_application(e) || is_sqrt_pair_application(e) || is_first_application(e) || is_last_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg1(const data_expression& e)
      {
        assert(is_nnpair_application(e) || is_concat_digit_application(e) || is_times_overflow_application(e) || is_monus_whr_application(e) || is_exp_aux3p_application(e) || is_exp_aux4p_application(e) || is_exp_aux3n_application(e) || is_exp_aux4n_application(e) || is_exp_auxtruep_application(e) || is_exp_auxtruen_application(e) || is_exp_auxfalsep_application(e) || is_exp_auxfalsen_application(e) || is_div_bold_application(e) || is_div_bold_whr_application(e) || is_div_whr1_application(e) || is_div_whr2_application(e) || is_mod_whr1_application(e) || is_divmod_aux_application(e) || is_divmod_aux_whr1_application(e) || is_divmod_aux_whr2_application(e) || is_divmod_aux_whr3_application(e) || is_divmod_aux_whr4_application(e) || is_divmod_aux_whr5_application(e) || is_divmod_aux_whr6_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_whr1_application(e) || is_sqrt_whr2_application(e) || is_sqrt_pair_whr1_application(e) || is_sqrt_pair_whr2_application(e) || is_sqrt_pair_whr3_application(e) || is_sqrt_pair_whr4_application(e) || is_sqrt_pair_whr5_application(e) || is_sqrt_pair_whr6_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg2(const data_expression& e)
      {
        assert(is_nnpair_application(e) || is_concat_digit_application(e) || is_times_overflow_application(e) || is_monus_whr_application(e) || is_exp_aux3p_application(e) || is_exp_aux4p_application(e) || is_exp_aux3n_application(e) || is_exp_aux4n_application(e) || is_exp_auxtruep_application(e) || is_exp_auxtruen_application(e) || is_exp_auxfalsep_application(e) || is_exp_auxfalsen_application(e) || is_div_bold_application(e) || is_div_bold_whr_application(e) || is_div_whr1_application(e) || is_div_whr2_application(e) || is_mod_whr1_application(e) || is_divmod_aux_application(e) || is_divmod_aux_whr1_application(e) || is_divmod_aux_whr2_application(e) || is_divmod_aux_whr3_application(e) || is_divmod_aux_whr4_application(e) || is_divmod_aux_whr5_application(e) || is_divmod_aux_whr6_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_whr1_application(e) || is_sqrt_whr2_application(e) || is_sqrt_pair_whr1_application(e) || is_sqrt_pair_whr2_application(e) || is_sqrt_pair_whr3_application(e) || is_sqrt_pair_whr4_application(e) || is_sqrt_pair_whr5_application(e) || is_sqrt_pair_whr6_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& left(const data_expression& e)
      {
        assert(is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_add_with_carry_application(e) || is_auxiliary_plus_nat_application(e) || is_times_application(e) || is_times_ordered_application(e) || is_div_application(e) || is_mod_application(e) || is_exp_application(e) || is_monus_application(e) || is_swap_zero_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& right(const data_expression& e)
      {
        assert(is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_add_with_carry_application(e) || is_auxiliary_plus_nat_application(e) || is_times_application(e) || is_times_ordered_application(e) || is_div_application(e) || is_mod_application(e) || is_exp_application(e) || is_monus_application(e) || is_swap_zero_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg3(const data_expression& e)
      {
        assert(is_times_overflow_application(e) || is_monus_whr_application(e) || is_exp_aux3p_application(e) || is_exp_aux4p_application(e) || is_exp_aux3n_application(e) || is_exp_aux4n_application(e) || is_exp_auxtruep_application(e) || is_exp_auxtruen_application(e) || is_exp_auxfalsep_application(e) || is_exp_auxfalsen_application(e) || is_div_bold_whr_application(e) || is_div_whr1_application(e) || is_div_whr2_application(e) || is_mod_whr1_application(e) || is_divmod_aux_whr1_application(e) || is_divmod_aux_whr2_application(e) || is_divmod_aux_whr3_application(e) || is_divmod_aux_whr4_application(e) || is_divmod_aux_whr5_application(e) || is_divmod_aux_whr6_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_whr1_application(e) || is_sqrt_whr2_application(e) || is_sqrt_pair_whr1_application(e) || is_sqrt_pair_whr2_application(e) || is_sqrt_pair_whr3_application(e) || is_sqrt_pair_whr4_application(e) || is_sqrt_pair_whr5_application(e) || is_sqrt_pair_whr6_application(e));
        return atermpp::down_cast<application>(e)[2];
      }
 
      inline
      const data_expression& arg4(const data_expression& e)
      {
        assert(is_monus_whr_application(e) || is_exp_aux4p_application(e) || is_exp_aux4n_application(e) || is_div_bold_whr_application(e) || is_div_whr1_application(e) || is_div_whr2_application(e) || is_mod_whr1_application(e) || is_divmod_aux_whr1_application(e) || is_divmod_aux_whr2_application(e) || is_divmod_aux_whr3_application(e) || is_divmod_aux_whr4_application(e) || is_divmod_aux_whr5_application(e) || is_divmod_aux_whr6_application(e) || is_swap_zero_add_application(e) || is_swap_zero_min_application(e) || is_swap_zero_monus_application(e) || is_sqrt_whr1_application(e) || is_sqrt_whr2_application(e) || is_sqrt_pair_whr1_application(e) || is_sqrt_pair_whr2_application(e) || is_sqrt_pair_whr4_application(e) || is_sqrt_pair_whr5_application(e));
        return atermpp::down_cast<application>(e)[3];
      }
 
      inline
      const data_expression& arg5(const data_expression& e)
      {
        assert(is_monus_whr_application(e) || is_div_bold_whr_application(e) || is_div_whr2_application(e) || is_divmod_aux_whr2_application(e) || is_divmod_aux_whr3_application(e) || is_divmod_aux_whr6_application(e) || is_sqrt_whr2_application(e) || is_sqrt_pair_whr2_application(e) || is_sqrt_pair_whr4_application(e) || is_sqrt_pair_whr5_application(e));
        return atermpp::down_cast<application>(e)[4];
      }
 
      inline
      const data_expression& arg6(const data_expression& e)
      {
        assert(is_div_bold_whr_application(e) || is_sqrt_pair_whr4_application(e));
        return atermpp::down_cast<application>(e)[5];
      }
 
      inline
      data_equation_vector nat_generate_equations_code()
      {
        variable vb("b",sort_bool::bool_());
        variable vp("p",sort_pos::pos());
        variable vp1("p1",sort_pos::pos());
        variable vp2("p2",sort_pos::pos());
        variable vn("n",nat());
        variable vn1("n1",nat());
        variable vn2("n2",nat());
        variable vm("m",nat());
        variable vm1("m1",nat());
        variable vm2("m2",nat());
        variable vm3("m3",nat());
        variable vm4("m4",nat());
        variable vm5("m5",nat());
        variable vpredp("predp",nat());
        variable vdiff("diff",nat());
        variable vshift_n1("shift_n1",nat());
        variable vsolution("solution",nat());
        variable vpq("pq",nat());
        variable vy("y",nat());
        variable vy_guess("y_guess",nat());
        variable vpair_("pair_",natnatpair());
        variable vlp("lp",nat());
        variable vw("w",sort_machine_word::machine_word());
        variable vw1("w1",sort_machine_word::machine_word());
        variable vw2("w2",sort_machine_word::machine_word());
        variable vw3("w3",sort_machine_word::machine_word());
        variable vw4("w4",sort_machine_word::machine_word());
        variable vshift_w("shift_w",sort_machine_word::machine_word());
        variable voverflow("overflow",sort_machine_word::machine_word());
 
        data_equation_vector result;
        result.push_back(data_equation(variable_list(), c0(), most_significant_digit_nat(sort_machine_word::zero_word())));
        result.push_back(data_equation(variable_list({vw}), equals_zero(most_significant_digit_nat(vw)), sort_machine_word::equals_zero_word(vw)));
        result.push_back(data_equation(variable_list({vn, vw}), equals_zero(concat_digit(vn, vw)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vw}), not_equals_zero(most_significant_digit_nat(vw)), sort_machine_word::not_equals_zero_word(vw)));
        result.push_back(data_equation(variable_list({vn, vw}), not_equals_zero(concat_digit(vn, vw)), sort_bool::true_()));
        result.push_back(data_equation(variable_list({vw}), equals_one(most_significant_digit_nat(vw)), sort_machine_word::equals_one_word(vw)));
        result.push_back(data_equation(variable_list({vn, vw}), equals_one(concat_digit(vn, vw)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vw}), succ_nat(most_significant_digit_nat(vw)), if_(sort_machine_word::equals_max_word(vw), concat_digit(most_significant_digit_nat(sort_machine_word::one_word()), sort_machine_word::zero_word()), most_significant_digit_nat(sort_machine_word::succ_word(vw)))));
        result.push_back(data_equation(variable_list({vn, vw}), succ_nat(concat_digit(vn, vw)), if_(sort_machine_word::equals_max_word(vw), concat_digit(succ_nat(vn), sort_machine_word::zero_word()), concat_digit(vn, sort_machine_word::succ_word(vw)))));
        result.push_back(data_equation(variable_list({vw}), succ(most_significant_digit_nat(vw)), if_(sort_machine_word::equals_max_word(vw), concat_digit(sort_pos::most_significant_digit(sort_machine_word::one_word()), sort_machine_word::zero_word()), sort_pos::most_significant_digit(sort_machine_word::succ_word(vw)))));
        result.push_back(data_equation(variable_list({vn, vw}), succ(concat_digit(vn, vw)), if_(sort_machine_word::equals_max_word(vw), concat_digit(succ(vn), sort_machine_word::zero_word()), concat_digit(nat2pos(vn), sort_machine_word::succ_word(vw)))));
        result.push_back(data_equation(variable_list({vw1, vw2}), equal_to(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), sort_machine_word::equal_word(vw1, vw2)));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), equal_to(concat_digit(vn, vw1), most_significant_digit_nat(vw2)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), equal_to(most_significant_digit_nat(vw1), concat_digit(vn, vw2)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), equal_to(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), sort_bool::and_(sort_machine_word::equal_word(vw1, vw2), equal_to(vn1, vn2))));
        result.push_back(data_equation(variable_list({vn1, vn2}), equal_to(succ_nat(vn1), vn2), sort_bool::and_(not_equals_zero(vn2), equal_to(vn1, natpred(vn2)))));
        result.push_back(data_equation(variable_list({vn1, vn2}), equal_to(vn1, succ_nat(vn2)), sort_bool::and_(not_equals_zero(vn1), equal_to(natpred(vn1), vn2))));
        result.push_back(data_equation(variable_list({vw1, vw2}), less(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), sort_machine_word::less_word(vw1, vw2)));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), less(concat_digit(vn, vw1), most_significant_digit_nat(vw2)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), less(most_significant_digit_nat(vw1), concat_digit(vn, vw2)), sort_bool::true_()));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), less(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::less_word(vw1, vw2), less_equal(vn1, vn2), less(vn1, vn2))));
        result.push_back(data_equation(variable_list({vn1, vn2}), less(succ_nat(vn1), vn2), sort_bool::and_(less(most_significant_digit_nat(sort_machine_word::one_word()), vn2), less(vn1, natpred(vn2)))));
        result.push_back(data_equation(variable_list({vn1, vn2}), less(vn1, succ_nat(vn2)), less_equal(vn1, vn2)));
        result.push_back(data_equation(variable_list({vn, vw1}), sort_machine_word::equals_zero_word(vw1), less(vn, most_significant_digit_nat(vw1)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vw1, vw2}), less_equal(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), sort_machine_word::less_equal_word(vw1, vw2)));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), less_equal(concat_digit(vn, vw1), most_significant_digit_nat(vw2)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), less_equal(most_significant_digit_nat(vw1), concat_digit(vn, vw2)), sort_bool::true_()));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), less_equal(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::less_equal_word(vw1, vw2), less_equal(vn1, vn2), less(vn1, vn2))));
        result.push_back(data_equation(variable_list({vn1, vn2}), less_equal(succ_nat(vn1), vn2), less(vn1, vn2)));
        result.push_back(data_equation(variable_list({vn1, vn2}), less_equal(vn1, succ_nat(vn2)), less_equal(natpred(vn1), vn2)));
        result.push_back(data_equation(variable_list({vn, vw1}), sort_machine_word::equals_zero_word(vw1), less_equal(most_significant_digit_nat(vw1), vn), sort_bool::true_()));
        result.push_back(data_equation(variable_list({vw}), pos2nat(sort_pos::most_significant_digit(vw)), most_significant_digit_nat(vw)));
        result.push_back(data_equation(variable_list({vp, vw}), pos2nat(concat_digit(vp, vw)), concat_digit(pos2nat(vp), vw)));
        result.push_back(data_equation(variable_list({vp}), pos2nat(sort_pos::succpos(vp)), succ_nat(pos2nat(vp))));
        result.push_back(data_equation(variable_list({vw}), sort_machine_word::not_equals_zero_word(vw), nat2pos(most_significant_digit_nat(vw)), sort_pos::most_significant_digit(vw)));
        result.push_back(data_equation(variable_list({vn, vw}), nat2pos(concat_digit(vn, vw)), concat_digit(nat2pos(vn), vw)));
        result.push_back(data_equation(variable_list({vn, vp}), maximum(vp, vn), if_(less_equal(vn, pos2nat(vp)), vp, nat2pos(vn))));
        result.push_back(data_equation(variable_list({vn, vp}), maximum(vn, vp), if_(less_equal(vn, pos2nat(vp)), vp, nat2pos(vn))));
        result.push_back(data_equation(variable_list({vm, vn}), maximum(vm, vn), if_(less_equal(vm, vn), vn, vm)));
        result.push_back(data_equation(variable_list({vm, vn}), minimum(vm, vn), if_(less_equal(vm, vn), vm, vn)));
        result.push_back(data_equation(variable_list({vw}), pred(sort_pos::most_significant_digit(vw)), most_significant_digit_nat(sort_machine_word::pred_word(vw))));
        result.push_back(data_equation(variable_list({vp, vw}), pred(concat_digit(vp, vw)), if_(sort_machine_word::equals_zero_word(vw), pred_whr(pred(vp)), concat_digit(pos2nat(vp), sort_machine_word::pred_word(vw)))));
        result.push_back(data_equation(variable_list({vpredp}), pred_whr(vpredp), if_(equals_zero(vpredp), most_significant_digit_nat(sort_machine_word::max_word()), concat_digit(vpredp, sort_machine_word::max_word()))));
        result.push_back(data_equation(variable_list({vn, vp}), plus(vp, vn), plus(vn, vp)));
        result.push_back(data_equation(variable_list({vw1, vw2}), plus(most_significant_digit_nat(vw1), sort_pos::most_significant_digit(vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(sort_pos::most_significant_digit(sort_machine_word::one_word()), sort_machine_word::add_word(vw1, vw2)), sort_pos::most_significant_digit(sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vw1, vw2}), plus(concat_digit(vn1, vw1), sort_pos::most_significant_digit(vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(succ(vn1), sort_machine_word::add_word(vw1, vw2)), concat_digit(nat2pos(vn1), sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vp, vw1, vw2}), plus(most_significant_digit_nat(vw1), concat_digit(vp, vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(sort_pos::succpos(vp), sort_machine_word::add_word(vw1, vw2)), concat_digit(vp, sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vp, vw1, vw2}), plus(concat_digit(vn1, vw1), concat_digit(vp, vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(plus(succ(vn1), vp), sort_machine_word::add_word(vw1, vw2)), concat_digit(plus(vn1, vp), sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vw1, vw2}), plus(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(most_significant_digit_nat(sort_machine_word::one_word()), sort_machine_word::add_word(vw1, vw2)), most_significant_digit_nat(sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vw1, vw2}), add_with_carry(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::add_with_carry_overflow_word(vw1, vw2), concat_digit(most_significant_digit_nat(sort_machine_word::one_word()), sort_machine_word::add_with_carry_word(vw1, vw2)), most_significant_digit_nat(sort_machine_word::add_with_carry_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vw1, vw2}), plus(concat_digit(vn1, vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(succ_nat(vn1), sort_machine_word::add_word(vw1, vw2)), concat_digit(vn1, sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vw1, vw2}), add_with_carry(concat_digit(vn1, vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::add_with_carry_overflow_word(vw1, vw2), concat_digit(succ_nat(vn1), sort_machine_word::add_with_carry_word(vw1, vw2)), concat_digit(vn1, sort_machine_word::add_with_carry_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn2, vw1, vw2}), plus(most_significant_digit_nat(vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(succ_nat(vn2), sort_machine_word::add_word(vw1, vw2)), concat_digit(vn2, sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn2, vw1, vw2}), add_with_carry(most_significant_digit_nat(vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::add_with_carry_overflow_word(vw1, vw2), concat_digit(succ_nat(vn2), sort_machine_word::add_with_carry_word(vw1, vw2)), concat_digit(vn2, sort_machine_word::add_with_carry_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), plus(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::add_overflow_word(vw1, vw2), concat_digit(add_with_carry(vn1, vn2), sort_machine_word::add_word(vw1, vw2)), concat_digit(plus(vn1, vn2), sort_machine_word::add_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), add_with_carry(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::add_with_carry_overflow_word(vw1, vw2), concat_digit(add_with_carry(vn1, vn2), sort_machine_word::add_with_carry_word(vw1, vw2)), concat_digit(plus(vn1, vn2), sort_machine_word::add_with_carry_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vn2}), plus(succ_nat(vn1), vn2), succ_nat(plus(vn1, vn2))));
        result.push_back(data_equation(variable_list({vn1, vn2}), plus(vn1, succ_nat(vn2)), succ_nat(plus(vn1, vn2))));
        result.push_back(data_equation(variable_list({vn1, vp2}), plus(succ_nat(vn1), vp2), sort_pos::succpos(plus(vn1, vp2))));
        result.push_back(data_equation(variable_list({vn1, vp2}), plus(vn1, sort_pos::succpos(vp2)), sort_pos::succpos(plus(vn1, vp2))));
        result.push_back(data_equation(variable_list({vn2, vp1}), plus(sort_pos::succpos(vp1), vn2), sort_pos::succpos(plus(vp1, vn2))));
        result.push_back(data_equation(variable_list({vn2, vp1}), plus(vp1, succ_nat(vn2)), sort_pos::succpos(plus(vp1, vn2))));
        result.push_back(data_equation(variable_list({vn1, vn2}), auxiliary_plus_nat(vn1, vn2), plus(vn1, vn2)));
        result.push_back(data_equation(variable_list({vw}), natpred(most_significant_digit_nat(vw)), if_(sort_machine_word::equals_zero_word(vw), most_significant_digit_nat(sort_machine_word::zero_word()), most_significant_digit_nat(sort_machine_word::pred_word(vw)))));
        result.push_back(data_equation(variable_list({vn, vw}), natpred(concat_digit(vn, vw)), if_(sort_machine_word::equals_zero_word(vw), if_(equals_one(vn), most_significant_digit_nat(sort_machine_word::max_word()), concat_digit(natpred(vn), sort_machine_word::max_word())), concat_digit(vn, sort_machine_word::pred_word(vw)))));
        result.push_back(data_equation(variable_list({vn}), natpred(succ_nat(vn)), vn));
        result.push_back(data_equation(variable_list({vw1, vw2}), monus(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), most_significant_digit_nat(sort_machine_word::monus_word(vw1, vw2))));
        result.push_back(data_equation(variable_list({vn1, vw1, vw2}), monus(concat_digit(vn1, vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::less_word(vw1, vw2), if_(equals_one(vn1), most_significant_digit_nat(sort_machine_word::minus_word(vw1, vw2)), concat_digit(natpred(vn1), sort_machine_word::minus_word(vw1, vw2))), concat_digit(vn1, sort_machine_word::minus_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn2, vw1, vw2}), monus(most_significant_digit_nat(vw1), concat_digit(vn2, vw2)), most_significant_digit_nat(sort_machine_word::zero_word())));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), monus(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), monus_whr(vn1, vw1, vn2, vw2, monus(vn1, vn2))));
        result.push_back(data_equation(variable_list({vdiff, vn1, vn2, vw1, vw2}), monus_whr(vn1, vw1, vn2, vw2, vdiff), if_(sort_machine_word::less_word(vw1, vw2), if_(equals_zero(vdiff), most_significant_digit_nat(sort_machine_word::zero_word()), if_(equals_one(vdiff), most_significant_digit_nat(sort_machine_word::minus_word(vw1, vw2)), concat_digit(natpred(vdiff), sort_machine_word::minus_word(vw1, vw2)))), if_(equals_zero(vdiff), most_significant_digit_nat(sort_machine_word::minus_word(vw1, vw2)), concat_digit(vdiff, sort_machine_word::minus_word(vw1, vw2))))));
        result.push_back(data_equation(variable_list({vw1, vw2}), times(most_significant_digit_nat(vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::equals_zero_word(sort_machine_word::times_overflow_word(vw1, vw2)), most_significant_digit_nat(sort_machine_word::times_word(vw1, vw2)), concat_digit(most_significant_digit_nat(sort_machine_word::times_overflow_word(vw1, vw2)), sort_machine_word::times_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn2, vw1, vw2}), times(most_significant_digit_nat(vw1), concat_digit(vn2, vw2)), if_(sort_machine_word::equals_zero_word(vw1), most_significant_digit_nat(sort_machine_word::zero_word()), concat_digit(times_overflow(vn2, vw1, sort_machine_word::times_overflow_word(vw1, vw2)), sort_machine_word::times_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vw1, vw2}), times(concat_digit(vn1, vw1), most_significant_digit_nat(vw2)), if_(sort_machine_word::equals_zero_word(vw2), most_significant_digit_nat(sort_machine_word::zero_word()), concat_digit(times_overflow(vn1, vw2, sort_machine_word::times_overflow_word(vw1, vw2)), sort_machine_word::times_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1, vw2}), times(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), if_(less(vn1, vn2), times_ordered(concat_digit(vn1, vw1), concat_digit(vn2, vw2)), times_ordered(concat_digit(vn2, vw2), concat_digit(vn1, vw1)))));
        result.push_back(data_equation(variable_list({vn2, vw1, vw2}), times_ordered(most_significant_digit_nat(vw1), concat_digit(vn2, vw2)), concat_digit(times_overflow(vn2, vw1, sort_machine_word::times_overflow_word(vw1, vw2)), sort_machine_word::times_word(vw1, vw2))));
        result.push_back(data_equation(variable_list({vn1, vn2, vw1}), times_ordered(concat_digit(vn1, vw1), vn2), plus(concat_digit(times_ordered(vn1, vn2), sort_machine_word::zero_word()), times_overflow(vn2, vw1, sort_machine_word::zero_word()))));
        result.push_back(data_equation(variable_list({voverflow, vw1, vw2}), times_overflow(most_significant_digit_nat(vw1), vw2, voverflow), if_(sort_machine_word::equals_zero_word(sort_machine_word::times_with_carry_overflow_word(vw1, vw2, voverflow)), most_significant_digit_nat(sort_machine_word::times_with_carry_word(vw1, vw2, voverflow)), concat_digit(most_significant_digit_nat(sort_machine_word::times_with_carry_overflow_word(vw1, vw2, voverflow)), sort_machine_word::times_with_carry_word(vw1, vw2, voverflow)))));
        result.push_back(data_equation(variable_list({vn1, voverflow, vw1, vw2}), times_overflow(concat_digit(vn1, vw1), vw2, voverflow), if_(sort_machine_word::equals_zero_word(vw2), most_significant_digit_nat(voverflow), concat_digit(times_overflow(vn1, vw2, sort_machine_word::times_with_carry_overflow_word(vw1, vw2, voverflow)), sort_machine_word::times_with_carry_word(vw1, vw2, voverflow)))));
        result.push_back(data_equation(variable_list({vw}), is_odd(most_significant_digit_nat(vw)), sort_machine_word::rightmost_bit(vw)));
        result.push_back(data_equation(variable_list({vn, vw}), is_odd(concat_digit(vn, vw)), sort_machine_word::rightmost_bit(vw)));
        result.push_back(data_equation(variable_list({vw}), div2(most_significant_digit_nat(vw)), most_significant_digit_nat(sort_machine_word::shift_right(sort_bool::false_(), vw))));
        result.push_back(data_equation(variable_list({vn, vw}), div2(concat_digit(vn, vw)), if_(equals_zero(vn), most_significant_digit_nat(sort_machine_word::shift_right(is_odd(vn), vw)), concat_digit(div2(vn), sort_machine_word::shift_right(is_odd(vn), vw)))));
        result.push_back(data_equation(variable_list({vw}), msd(most_significant_digit_nat(vw)), vw));
        result.push_back(data_equation(variable_list({vn, vw}), msd(concat_digit(vn, vw)), msd(vn)));
        result.push_back(data_equation(variable_list({vn, vw}), exp(vn, most_significant_digit_nat(vw)), exp_aux3n(sort_machine_word::rightmost_bit(vw), vn, vw)));
        result.push_back(data_equation(variable_list({vn, vn1, vw1}), exp(vn, concat_digit(vn1, vw1)), exp_aux4n(sort_machine_word::rightmost_bit(vw1), vn, vn1, vw1)));
        result.push_back(data_equation(variable_list({vn, vw}), exp_aux3n(sort_bool::true_(), vn, vw), if_(sort_machine_word::equals_one_word(vw), vn, times(vn, exp_aux3n(sort_machine_word::rightmost_bit(sort_machine_word::shift_right(sort_bool::false_(), vw)), times(vn, vn), sort_machine_word::shift_right(sort_bool::false_(), vw))))));
        result.push_back(data_equation(variable_list({vn, vw}), exp_aux3n(sort_bool::false_(), vn, vw), if_(sort_machine_word::equals_zero_word(vw), most_significant_digit_nat(sort_machine_word::one_word()), exp_aux3n(sort_machine_word::rightmost_bit(sort_machine_word::shift_right(sort_bool::false_(), vw)), times(vn, vn), sort_machine_word::shift_right(sort_bool::false_(), vw)))));
        result.push_back(data_equation(variable_list({vn, vn1, vw}), exp_aux4n(sort_bool::true_(), vn, vn1, vw), exp_auxtruen(vn, div2(vn1), sort_machine_word::shift_right(is_odd(vn1), vw))));
        result.push_back(data_equation(variable_list({vn, vshift_n1, vshift_w}), exp_auxtruen(vn, vshift_n1, vshift_w), if_(equals_zero(vshift_n1), times(vn, exp_aux3n(sort_machine_word::rightmost_bit(vshift_w), times(vn, vn), vshift_w)), times(vn, exp_aux4n(sort_machine_word::rightmost_bit(vshift_w), times(vn, vn), vshift_n1, vshift_w)))));
        result.push_back(data_equation(variable_list({vn, vn1, vw}), exp_aux4n(sort_bool::false_(), vn, vn1, vw), exp_auxfalsen(vn, div2(vn1), sort_machine_word::shift_right(is_odd(vn1), vw))));
        result.push_back(data_equation(variable_list({vn, vshift_n1, vshift_w}), exp_auxfalsen(vn, vshift_n1, vshift_w), if_(equals_zero(vshift_n1), exp_aux3n(sort_machine_word::rightmost_bit(vshift_w), times(vn, vn), vshift_w), exp_aux4n(sort_machine_word::rightmost_bit(vshift_w), times(vn, vn), vshift_n1, vshift_w))));
        result.push_back(data_equation(variable_list({vp, vw}), exp(vp, most_significant_digit_nat(vw)), exp_aux3p(sort_machine_word::rightmost_bit(vw), vp, vw)));
        result.push_back(data_equation(variable_list({vn1, vp, vw1}), exp(vp, concat_digit(vn1, vw1)), exp_aux4p(sort_machine_word::rightmost_bit(vw1), vp, vn1, vw1)));
        result.push_back(data_equation(variable_list({vp, vw}), exp_aux3p(sort_bool::true_(), vp, vw), if_(sort_machine_word::equals_one_word(vw), vp, times(vp, exp_aux3p(sort_machine_word::rightmost_bit(sort_machine_word::shift_right(sort_bool::false_(), vw)), times(vp, vp), sort_machine_word::shift_right(sort_bool::false_(), vw))))));
        result.push_back(data_equation(variable_list({vp, vw}), exp_aux3p(sort_bool::false_(), vp, vw), if_(sort_machine_word::equals_zero_word(vw), sort_pos::most_significant_digit(sort_machine_word::one_word()), exp_aux3p(sort_machine_word::rightmost_bit(sort_machine_word::shift_right(sort_bool::false_(), vw)), times(vp, vp), sort_machine_word::shift_right(sort_bool::false_(), vw)))));
        result.push_back(data_equation(variable_list({vn1, vp, vw}), exp_aux4p(sort_bool::true_(), vp, vn1, vw), exp_auxtruep(vp, div2(vn1), sort_machine_word::shift_right(is_odd(vn1), vw))));
        result.push_back(data_equation(variable_list({vp, vshift_n1, vshift_w}), exp_auxtruep(vp, vshift_n1, vshift_w), if_(equals_zero(vshift_n1), times(vp, exp_aux3p(sort_machine_word::rightmost_bit(vshift_w), times(vp, vp), vshift_w)), times(vp, exp_aux4p(sort_machine_word::rightmost_bit(vshift_w), times(vp, vp), vshift_n1, vshift_w)))));
        result.push_back(data_equation(variable_list({vn1, vp, vw}), exp_aux4p(sort_bool::false_(), vp, vn1, vw), exp_auxfalsep(vp, div2(vn1), sort_machine_word::shift_right(is_odd(vn1), vw))));
        result.push_back(data_equation(variable_list({vp, vshift_n1, vshift_w}), exp_auxfalsep(vp, vshift_n1, vshift_w), if_(equals_zero(vshift_n1), exp_aux3p(sort_machine_word::rightmost_bit(vshift_w), times(vp, vp), vshift_w), exp_aux4p(sort_machine_word::rightmost_bit(vshift_w), times(vp, vp), vshift_n1, vshift_w))));
        result.push_back(data_equation(variable_list({vw1, vw2}), div(most_significant_digit_nat(vw1), sort_pos::most_significant_digit(vw2)), most_significant_digit_nat(sort_machine_word::div_word(vw1, vw2))));
        result.push_back(data_equation(variable_list({vw1, vw2}), mod(most_significant_digit_nat(vw1), sort_pos::most_significant_digit(vw2)), most_significant_digit_nat(sort_machine_word::mod_word(vw1, vw2))));
        result.push_back(data_equation(variable_list({vp, vw1, vw2}), div(most_significant_digit_nat(vw1), concat_digit(vp, vw2)), most_significant_digit_nat(sort_machine_word::zero_word())));
        result.push_back(data_equation(variable_list({vp, vw1, vw2}), mod(most_significant_digit_nat(vw1), concat_digit(vp, vw2)), most_significant_digit_nat(vw1)));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), div(concat_digit(vn, vw1), sort_pos::most_significant_digit(vw2)), div_whr1(vn, vw1, vw2, divmod_aux(vn, sort_pos::most_significant_digit(vw2)))));
        result.push_back(data_equation(variable_list({vn, vpair_, vw1, vw2}), div_whr1(vn, vw1, vw2, vpair_), if_(less(vn, most_significant_digit_nat(vw2)), most_significant_digit_nat(div_bold(concat_digit(vn, vw1), sort_pos::most_significant_digit(vw2))), if_(equals_zero(first(vpair_)), most_significant_digit_nat(div_bold(if_(equals_zero(last(vpair_)), most_significant_digit_nat(vw1), concat_digit(last(vpair_), vw1)), sort_pos::most_significant_digit(vw2))), concat_digit(first(vpair_), div_bold(if_(equals_zero(last(vpair_)), most_significant_digit_nat(vw1), concat_digit(last(vpair_), vw1)), sort_pos::most_significant_digit(vw2)))))));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), mod(concat_digit(vn, vw1), sort_pos::most_significant_digit(vw2)), most_significant_digit_nat(sort_machine_word::mod_doubleword(msd(mod(vn, sort_pos::most_significant_digit(vw2))), vw1, vw2))));
        result.push_back(data_equation(variable_list({vn, vp, vw1, vw2}), div(concat_digit(vn, vw1), concat_digit(vp, vw2)), if_(less(vn, pos2nat(concat_digit(vp, vw2))), most_significant_digit_nat(div_bold(concat_digit(vn, vw1), concat_digit(vp, vw2))), div_whr2(vn, vw1, vp, vw2, divmod_aux(vn, concat_digit(vp, vw2))))));
        result.push_back(data_equation(variable_list({vn, vp, vpair_, vw1, vw2}), div_whr2(vn, vw1, vp, vw2, vpair_), plus(if_(equals_zero(first(vpair_)), most_significant_digit_nat(sort_machine_word::zero_word()), concat_digit(first(vpair_), sort_machine_word::zero_word())), most_significant_digit_nat(div_bold(if_(equals_zero(last(vpair_)), most_significant_digit_nat(vw1), concat_digit(last(vpair_), vw1)), concat_digit(vp, vw2))))));
        result.push_back(data_equation(variable_list({vn, vp, vw1, vw2}), mod(concat_digit(vn, vw1), concat_digit(vp, vw2)), mod_whr1(vw1, vp, vw2, mod(vn, concat_digit(vp, vw2)))));
        result.push_back(data_equation(variable_list({vm1, vp, vw1, vw2}), mod_whr1(vw1, vp, vw2, vm1), monus(if_(less(most_significant_digit_nat(sort_machine_word::zero_word()), vm1), concat_digit(vm1, vw1), most_significant_digit_nat(vw1)), times(concat_digit(pos2nat(vp), vw2), most_significant_digit_nat(div_bold(if_(less(most_significant_digit_nat(sort_machine_word::zero_word()), vm1), concat_digit(vm1, vw1), most_significant_digit_nat(vw1)), concat_digit(vp, vw2)))))));
        result.push_back(data_equation(variable_list({vw1, vw2}), divmod_aux(most_significant_digit_nat(vw1), sort_pos::most_significant_digit(vw2)), nnpair(most_significant_digit_nat(sort_machine_word::div_word(vw1, vw2)), most_significant_digit_nat(sort_machine_word::mod_word(vw1, vw2)))));
        result.push_back(data_equation(variable_list({vp, vw1, vw2}), divmod_aux(most_significant_digit_nat(vw1), concat_digit(vp, vw2)), nnpair(most_significant_digit_nat(sort_machine_word::zero_word()), most_significant_digit_nat(vw1))));
        result.push_back(data_equation(variable_list({vn, vw1, vw2}), divmod_aux(concat_digit(vn, vw1), sort_pos::most_significant_digit(vw2)), divmod_aux_whr1(vn, vw1, vw2, divmod_aux(vn,