machine_word.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_MACHINE_WORD_H
#define MCRL2_DATA_MACHINE_WORD_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/bool.h"
 
namespace mcrl2 {
 
  namespace data {
 
    namespace sort_machine_word {
 
      inline
      const core::identifier_string& machine_word_name()
      {
        static core::identifier_string machine_word_name = core::identifier_string("@word");
        return machine_word_name;
      }
 
      inline
      const basic_sort& machine_word()
      {
        static basic_sort machine_word = basic_sort(machine_word_name());
        return machine_word;
      }
 
      inline
      bool is_machine_word(const sort_expression& e)
      {
        if (is_basic_sort(e))
        {
          return basic_sort(e) == machine_word();
        }
        return false;
      }
 
 
      inline
      const core::identifier_string& zero_word_name()
      {
        static core::identifier_string zero_word_name = core::identifier_string("@zero_word");
        return zero_word_name;
      }
 
      
      inline
      const function_symbol& zero_word()
      {
        static function_symbol zero_word(zero_word_name(), machine_word());
        return zero_word;
      }
 
      inline
      bool is_zero_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == zero_word();
        }
        return false;
      }
 
      inline
      void zero_word_manual_implementation(data_expression& result);
 
      inline
      void zero_word_application(data_expression& result, const data_expression& a)
      {
        static_cast< void >(a); // suppress unused variable warning.
        assert(is_function_symbol(a));
        // assert(a==zero_word());
        zero_word_manual_implementation(result);
      }
 
 
      inline
      const core::identifier_string& succ_word_name()
      {
        static core::identifier_string succ_word_name = core::identifier_string("@succ_word");
        return succ_word_name;
      }
 
      
      inline
      const function_symbol& succ_word()
      {
        static function_symbol succ_word(succ_word_name(), make_function_sort_(machine_word(), machine_word()));
        return succ_word;
      }
 
      inline
      bool is_succ_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == succ_word();
        }
        return false;
      }
 
      
      inline
      application succ_word(const data_expression& arg0)
      {
        return sort_machine_word::succ_word()(arg0);
      }
 
      
      inline
      void make_succ_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::succ_word(),arg0);
      }
 
      inline
      bool is_succ_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_succ_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void succ_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void succ_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==succ_word());
        succ_word_manual_implementation(result, a[0]);
      }
 
      inline
      function_symbol_vector machine_word_generate_constructors_code()
      {
        function_symbol_vector result;
        result.push_back(sort_machine_word::zero_word());
        result.push_back(sort_machine_word::succ_word());
 
        return result;
      }
      inline
      function_symbol_vector machine_word_mCRL2_usable_constructors()
      {
        function_symbol_vector result;
        result.push_back(sort_machine_word::zero_word());
        result.push_back(sort_machine_word::succ_word());
 
        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 machine_word_cpp_implementable_constructors()
      {
        implementation_map result;
        result[sort_machine_word::zero_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::zero_word_application,"sort_machine_word::zero_word_manual_implementation");
        result[sort_machine_word::succ_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::succ_word_application,"sort_machine_word::succ_word_manual_implementation");
 
        return result;
      }
 
      inline
      const core::identifier_string& one_word_name()
      {
        static core::identifier_string one_word_name = core::identifier_string("@one_word");
        return one_word_name;
      }
 
      
      inline
      const function_symbol& one_word()
      {
        static function_symbol one_word(one_word_name(), machine_word());
        return one_word;
      }
 
      inline
      bool is_one_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == one_word();
        }
        return false;
      }
 
      inline
      void one_word_manual_implementation(data_expression& result);
 
      inline
      void one_word_application(data_expression& result, const data_expression& a)
      {
        static_cast< void >(a); // suppress unused variable warning.
        assert(is_function_symbol(a));
        // assert(a==one_word());
        one_word_manual_implementation(result);
      }
 
 
      inline
      const core::identifier_string& two_word_name()
      {
        static core::identifier_string two_word_name = core::identifier_string("@two_word");
        return two_word_name;
      }
 
      
      inline
      const function_symbol& two_word()
      {
        static function_symbol two_word(two_word_name(), machine_word());
        return two_word;
      }
 
      inline
      bool is_two_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == two_word();
        }
        return false;
      }
 
      inline
      void two_word_manual_implementation(data_expression& result);
 
      inline
      void two_word_application(data_expression& result, const data_expression& a)
      {
        static_cast< void >(a); // suppress unused variable warning.
        assert(is_function_symbol(a));
        // assert(a==two_word());
        two_word_manual_implementation(result);
      }
 
 
      inline
      const core::identifier_string& three_word_name()
      {
        static core::identifier_string three_word_name = core::identifier_string("@three_word");
        return three_word_name;
      }
 
      
      inline
      const function_symbol& three_word()
      {
        static function_symbol three_word(three_word_name(), machine_word());
        return three_word;
      }
 
      inline
      bool is_three_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == three_word();
        }
        return false;
      }
 
      inline
      void three_word_manual_implementation(data_expression& result);
 
      inline
      void three_word_application(data_expression& result, const data_expression& a)
      {
        static_cast< void >(a); // suppress unused variable warning.
        assert(is_function_symbol(a));
        // assert(a==three_word());
        three_word_manual_implementation(result);
      }
 
 
      inline
      const core::identifier_string& four_word_name()
      {
        static core::identifier_string four_word_name = core::identifier_string("@four_word");
        return four_word_name;
      }
 
      
      inline
      const function_symbol& four_word()
      {
        static function_symbol four_word(four_word_name(), machine_word());
        return four_word;
      }
 
      inline
      bool is_four_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == four_word();
        }
        return false;
      }
 
      inline
      void four_word_manual_implementation(data_expression& result);
 
      inline
      void four_word_application(data_expression& result, const data_expression& a)
      {
        static_cast< void >(a); // suppress unused variable warning.
        assert(is_function_symbol(a));
        // assert(a==four_word());
        four_word_manual_implementation(result);
      }
 
 
      inline
      const core::identifier_string& max_word_name()
      {
        static core::identifier_string max_word_name = core::identifier_string("@max_word");
        return max_word_name;
      }
 
      
      inline
      const function_symbol& max_word()
      {
        static function_symbol max_word(max_word_name(), machine_word());
        return max_word;
      }
 
      inline
      bool is_max_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == max_word();
        }
        return false;
      }
 
      inline
      void max_word_manual_implementation(data_expression& result);
 
      inline
      void max_word_application(data_expression& result, const data_expression& a)
      {
        static_cast< void >(a); // suppress unused variable warning.
        assert(is_function_symbol(a));
        // assert(a==max_word());
        max_word_manual_implementation(result);
      }
 
 
      inline
      const core::identifier_string& equals_zero_word_name()
      {
        static core::identifier_string equals_zero_word_name = core::identifier_string("@equals_zero_word");
        return equals_zero_word_name;
      }
 
      
      inline
      const function_symbol& equals_zero_word()
      {
        static function_symbol equals_zero_word(equals_zero_word_name(), make_function_sort_(machine_word(), sort_bool::bool_()));
        return equals_zero_word;
      }
 
      inline
      bool is_equals_zero_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == equals_zero_word();
        }
        return false;
      }
 
      
      inline
      application equals_zero_word(const data_expression& arg0)
      {
        return sort_machine_word::equals_zero_word()(arg0);
      }
 
      
      inline
      void make_equals_zero_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::equals_zero_word(),arg0);
      }
 
      inline
      bool is_equals_zero_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_equals_zero_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void equals_zero_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void equals_zero_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==equals_zero_word());
        equals_zero_word_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& not_equals_zero_word_name()
      {
        static core::identifier_string not_equals_zero_word_name = core::identifier_string("@not_equals_zero_word");
        return not_equals_zero_word_name;
      }
 
      
      inline
      const function_symbol& not_equals_zero_word()
      {
        static function_symbol not_equals_zero_word(not_equals_zero_word_name(), make_function_sort_(machine_word(), sort_bool::bool_()));
        return not_equals_zero_word;
      }
 
      inline
      bool is_not_equals_zero_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == not_equals_zero_word();
        }
        return false;
      }
 
      
      inline
      application not_equals_zero_word(const data_expression& arg0)
      {
        return sort_machine_word::not_equals_zero_word()(arg0);
      }
 
      
      inline
      void make_not_equals_zero_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::not_equals_zero_word(),arg0);
      }
 
      inline
      bool is_not_equals_zero_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_not_equals_zero_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void not_equals_zero_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void not_equals_zero_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==not_equals_zero_word());
        not_equals_zero_word_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& equals_one_word_name()
      {
        static core::identifier_string equals_one_word_name = core::identifier_string("@equals_one_word");
        return equals_one_word_name;
      }
 
      
      inline
      const function_symbol& equals_one_word()
      {
        static function_symbol equals_one_word(equals_one_word_name(), make_function_sort_(machine_word(), sort_bool::bool_()));
        return equals_one_word;
      }
 
      inline
      bool is_equals_one_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == equals_one_word();
        }
        return false;
      }
 
      
      inline
      application equals_one_word(const data_expression& arg0)
      {
        return sort_machine_word::equals_one_word()(arg0);
      }
 
      
      inline
      void make_equals_one_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::equals_one_word(),arg0);
      }
 
      inline
      bool is_equals_one_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_equals_one_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void equals_one_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void equals_one_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==equals_one_word());
        equals_one_word_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& equals_max_word_name()
      {
        static core::identifier_string equals_max_word_name = core::identifier_string("@equals_max_word");
        return equals_max_word_name;
      }
 
      
      inline
      const function_symbol& equals_max_word()
      {
        static function_symbol equals_max_word(equals_max_word_name(), make_function_sort_(machine_word(), sort_bool::bool_()));
        return equals_max_word;
      }
 
      inline
      bool is_equals_max_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == equals_max_word();
        }
        return false;
      }
 
      
      inline
      application equals_max_word(const data_expression& arg0)
      {
        return sort_machine_word::equals_max_word()(arg0);
      }
 
      
      inline
      void make_equals_max_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::equals_max_word(),arg0);
      }
 
      inline
      bool is_equals_max_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_equals_max_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void equals_max_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void equals_max_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==equals_max_word());
        equals_max_word_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& add_word_name()
      {
        static core::identifier_string add_word_name = core::identifier_string("@add_word");
        return add_word_name;
      }
 
      
      inline
      const function_symbol& add_word()
      {
        static function_symbol add_word(add_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return add_word;
      }
 
      inline
      bool is_add_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == add_word();
        }
        return false;
      }
 
      
      inline
      application add_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::add_word()(arg0, arg1);
      }
 
      
      inline
      void make_add_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::add_word(),arg0, arg1);
      }
 
      inline
      bool is_add_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_add_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void add_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void add_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==add_word());
        add_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& add_with_carry_word_name()
      {
        static core::identifier_string add_with_carry_word_name = core::identifier_string("@add_with_carry_word");
        return add_with_carry_word_name;
      }
 
      
      inline
      const function_symbol& add_with_carry_word()
      {
        static function_symbol add_with_carry_word(add_with_carry_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return add_with_carry_word;
      }
 
      inline
      bool is_add_with_carry_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == add_with_carry_word();
        }
        return false;
      }
 
      
      inline
      application add_with_carry_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::add_with_carry_word()(arg0, arg1);
      }
 
      
      inline
      void make_add_with_carry_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::add_with_carry_word(),arg0, arg1);
      }
 
      inline
      bool is_add_with_carry_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_add_with_carry_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void add_with_carry_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void add_with_carry_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==add_with_carry_word());
        add_with_carry_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& add_overflow_word_name()
      {
        static core::identifier_string add_overflow_word_name = core::identifier_string("@add_overflow_word");
        return add_overflow_word_name;
      }
 
      
      inline
      const function_symbol& add_overflow_word()
      {
        static function_symbol add_overflow_word(add_overflow_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return add_overflow_word;
      }
 
      inline
      bool is_add_overflow_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == add_overflow_word();
        }
        return false;
      }
 
      
      inline
      application add_overflow_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::add_overflow_word()(arg0, arg1);
      }
 
      
      inline
      void make_add_overflow_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::add_overflow_word(),arg0, arg1);
      }
 
      inline
      bool is_add_overflow_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_add_overflow_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void add_overflow_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void add_overflow_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==add_overflow_word());
        add_overflow_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& add_with_carry_overflow_word_name()
      {
        static core::identifier_string add_with_carry_overflow_word_name = core::identifier_string("@add_with_carry_overflow_word");
        return add_with_carry_overflow_word_name;
      }
 
      
      inline
      const function_symbol& add_with_carry_overflow_word()
      {
        static function_symbol add_with_carry_overflow_word(add_with_carry_overflow_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return add_with_carry_overflow_word;
      }
 
      inline
      bool is_add_with_carry_overflow_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == add_with_carry_overflow_word();
        }
        return false;
      }
 
      
      inline
      application add_with_carry_overflow_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::add_with_carry_overflow_word()(arg0, arg1);
      }
 
      
      inline
      void make_add_with_carry_overflow_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::add_with_carry_overflow_word(),arg0, arg1);
      }
 
      inline
      bool is_add_with_carry_overflow_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_add_with_carry_overflow_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void add_with_carry_overflow_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void add_with_carry_overflow_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==add_with_carry_overflow_word());
        add_with_carry_overflow_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& times_word_name()
      {
        static core::identifier_string times_word_name = core::identifier_string("@times_word");
        return times_word_name;
      }
 
      
      inline
      const function_symbol& times_word()
      {
        static function_symbol times_word(times_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return times_word;
      }
 
      inline
      bool is_times_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == times_word();
        }
        return false;
      }
 
      
      inline
      application times_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::times_word()(arg0, arg1);
      }
 
      
      inline
      void make_times_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::times_word(),arg0, arg1);
      }
 
      inline
      bool is_times_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void times_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void times_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==times_word());
        times_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& times_with_carry_word_name()
      {
        static core::identifier_string times_with_carry_word_name = core::identifier_string("@times_with_carry_word");
        return times_with_carry_word_name;
      }
 
      
      inline
      const function_symbol& times_with_carry_word()
      {
        static function_symbol times_with_carry_word(times_with_carry_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word()));
        return times_with_carry_word;
      }
 
      inline
      bool is_times_with_carry_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == times_with_carry_word();
        }
        return false;
      }
 
      
      inline
      application times_with_carry_word(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_machine_word::times_with_carry_word()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_times_with_carry_word(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_machine_word::times_with_carry_word(),arg0, arg1, arg2);
      }
 
      inline
      bool is_times_with_carry_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_with_carry_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void times_with_carry_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void times_with_carry_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==times_with_carry_word());
        times_with_carry_word_manual_implementation(result, a[0], a[1], a[2]);
      }
 
 
      inline
      const core::identifier_string& times_overflow_word_name()
      {
        static core::identifier_string times_overflow_word_name = core::identifier_string("@times_overflow_word");
        return times_overflow_word_name;
      }
 
      
      inline
      const function_symbol& times_overflow_word()
      {
        static function_symbol times_overflow_word(times_overflow_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return times_overflow_word;
      }
 
      inline
      bool is_times_overflow_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == times_overflow_word();
        }
        return false;
      }
 
      
      inline
      application times_overflow_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::times_overflow_word()(arg0, arg1);
      }
 
      
      inline
      void make_times_overflow_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::times_overflow_word(),arg0, arg1);
      }
 
      inline
      bool is_times_overflow_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_overflow_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void times_overflow_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void times_overflow_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==times_overflow_word());
        times_overflow_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& times_with_carry_overflow_word_name()
      {
        static core::identifier_string times_with_carry_overflow_word_name = core::identifier_string("@times_with_carry_overflow_word");
        return times_with_carry_overflow_word_name;
      }
 
      
      inline
      const function_symbol& times_with_carry_overflow_word()
      {
        static function_symbol times_with_carry_overflow_word(times_with_carry_overflow_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word()));
        return times_with_carry_overflow_word;
      }
 
      inline
      bool is_times_with_carry_overflow_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == times_with_carry_overflow_word();
        }
        return false;
      }
 
      
      inline
      application times_with_carry_overflow_word(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_machine_word::times_with_carry_overflow_word()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_times_with_carry_overflow_word(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_machine_word::times_with_carry_overflow_word(),arg0, arg1, arg2);
      }
 
      inline
      bool is_times_with_carry_overflow_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_with_carry_overflow_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void times_with_carry_overflow_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void times_with_carry_overflow_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==times_with_carry_overflow_word());
        times_with_carry_overflow_word_manual_implementation(result, a[0], a[1], a[2]);
      }
 
 
      inline
      const core::identifier_string& minus_word_name()
      {
        static core::identifier_string minus_word_name = core::identifier_string("@minus_word");
        return minus_word_name;
      }
 
      
      inline
      const function_symbol& minus_word()
      {
        static function_symbol minus_word(minus_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return minus_word;
      }
 
      inline
      bool is_minus_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == minus_word();
        }
        return false;
      }
 
      
      inline
      application minus_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::minus_word()(arg0, arg1);
      }
 
      
      inline
      void make_minus_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::minus_word(),arg0, arg1);
      }
 
      inline
      bool is_minus_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_minus_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void minus_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void minus_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==minus_word());
        minus_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& monus_word_name()
      {
        static core::identifier_string monus_word_name = core::identifier_string("@monus_word");
        return monus_word_name;
      }
 
      
      inline
      const function_symbol& monus_word()
      {
        static function_symbol monus_word(monus_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return monus_word;
      }
 
      inline
      bool is_monus_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == monus_word();
        }
        return false;
      }
 
      
      inline
      application monus_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::monus_word()(arg0, arg1);
      }
 
      
      inline
      void make_monus_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::monus_word(),arg0, arg1);
      }
 
      inline
      bool is_monus_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_monus_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void monus_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void monus_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==monus_word());
        monus_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& div_word_name()
      {
        static core::identifier_string div_word_name = core::identifier_string("@div_word");
        return div_word_name;
      }
 
      
      inline
      const function_symbol& div_word()
      {
        static function_symbol div_word(div_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return div_word;
      }
 
      inline
      bool is_div_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_word();
        }
        return false;
      }
 
      
      inline
      application div_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::div_word()(arg0, arg1);
      }
 
      
      inline
      void make_div_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::div_word(),arg0, arg1);
      }
 
      inline
      bool is_div_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void div_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void div_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==div_word());
        div_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& mod_word_name()
      {
        static core::identifier_string mod_word_name = core::identifier_string("@mod_word");
        return mod_word_name;
      }
 
      
      inline
      const function_symbol& mod_word()
      {
        static function_symbol mod_word(mod_word_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return mod_word;
      }
 
      inline
      bool is_mod_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == mod_word();
        }
        return false;
      }
 
      
      inline
      application mod_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::mod_word()(arg0, arg1);
      }
 
      
      inline
      void make_mod_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::mod_word(),arg0, arg1);
      }
 
      inline
      bool is_mod_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_mod_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void mod_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void mod_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==mod_word());
        mod_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& sqrt_word_name()
      {
        static core::identifier_string sqrt_word_name = core::identifier_string("@sqrt_word");
        return sqrt_word_name;
      }
 
      
      inline
      const function_symbol& sqrt_word()
      {
        static function_symbol sqrt_word(sqrt_word_name(), make_function_sort_(machine_word(), machine_word()));
        return sqrt_word;
      }
 
      inline
      bool is_sqrt_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_word();
        }
        return false;
      }
 
      
      inline
      application sqrt_word(const data_expression& arg0)
      {
        return sort_machine_word::sqrt_word()(arg0);
      }
 
      
      inline
      void make_sqrt_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::sqrt_word(),arg0);
      }
 
      inline
      bool is_sqrt_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void sqrt_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void sqrt_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==sqrt_word());
        sqrt_word_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& div_doubleword_name()
      {
        static core::identifier_string div_doubleword_name = core::identifier_string("@div_doubleword");
        return div_doubleword_name;
      }
 
      
      inline
      const function_symbol& div_doubleword()
      {
        static function_symbol div_doubleword(div_doubleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word()));
        return div_doubleword;
      }
 
      inline
      bool is_div_doubleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_doubleword();
        }
        return false;
      }
 
      
      inline
      application div_doubleword(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_machine_word::div_doubleword()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_div_doubleword(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_machine_word::div_doubleword(),arg0, arg1, arg2);
      }
 
      inline
      bool is_div_doubleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_doubleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void div_doubleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void div_doubleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==div_doubleword());
        div_doubleword_manual_implementation(result, a[0], a[1], a[2]);
      }
 
 
      inline
      const core::identifier_string& div_double_doubleword_name()
      {
        static core::identifier_string div_double_doubleword_name = core::identifier_string("@div_double_doubleword");
        return div_double_doubleword_name;
      }
 
      
      inline
      const function_symbol& div_double_doubleword()
      {
        static function_symbol div_double_doubleword(div_double_doubleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word(), machine_word()));
        return div_double_doubleword;
      }
 
      inline
      bool is_div_double_doubleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_double_doubleword();
        }
        return false;
      }
 
      
      inline
      application div_double_doubleword(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_machine_word::div_double_doubleword()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_div_double_doubleword(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_machine_word::div_double_doubleword(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_div_double_doubleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_double_doubleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void div_double_doubleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3);
 
 
      inline
      void div_double_doubleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==div_double_doubleword());
        div_double_doubleword_manual_implementation(result, a[0], a[1], a[2], a[3]);
      }
 
 
      inline
      const core::identifier_string& div_triple_doubleword_name()
      {
        static core::identifier_string div_triple_doubleword_name = core::identifier_string("@div_triple_doubleword");
        return div_triple_doubleword_name;
      }
 
      
      inline
      const function_symbol& div_triple_doubleword()
      {
        static function_symbol div_triple_doubleword(div_triple_doubleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word(), machine_word(), machine_word()));
        return div_triple_doubleword;
      }
 
      inline
      bool is_div_triple_doubleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == div_triple_doubleword();
        }
        return false;
      }
 
      
      inline
      application div_triple_doubleword(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4)
      {
        return sort_machine_word::div_triple_doubleword()(arg0, arg1, arg2, arg3, arg4);
      }
 
      
      inline
      void make_div_triple_doubleword(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_machine_word::div_triple_doubleword(),arg0, arg1, arg2, arg3, arg4);
      }
 
      inline
      bool is_div_triple_doubleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_div_triple_doubleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void div_triple_doubleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3, const data_expression& arg4);
 
 
      inline
      void div_triple_doubleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==div_triple_doubleword());
        div_triple_doubleword_manual_implementation(result, a[0], a[1], a[2], a[3], a[4]);
      }
 
 
      inline
      const core::identifier_string& mod_doubleword_name()
      {
        static core::identifier_string mod_doubleword_name = core::identifier_string("@mod_doubleword");
        return mod_doubleword_name;
      }
 
      
      inline
      const function_symbol& mod_doubleword()
      {
        static function_symbol mod_doubleword(mod_doubleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word()));
        return mod_doubleword;
      }
 
      inline
      bool is_mod_doubleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == mod_doubleword();
        }
        return false;
      }
 
      
      inline
      application mod_doubleword(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_machine_word::mod_doubleword()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_mod_doubleword(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_machine_word::mod_doubleword(),arg0, arg1, arg2);
      }
 
      inline
      bool is_mod_doubleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_mod_doubleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void mod_doubleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void mod_doubleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==mod_doubleword());
        mod_doubleword_manual_implementation(result, a[0], a[1], a[2]);
      }
 
 
      inline
      const core::identifier_string& sqrt_doubleword_name()
      {
        static core::identifier_string sqrt_doubleword_name = core::identifier_string("@sqrt_doubleword");
        return sqrt_doubleword_name;
      }
 
      
      inline
      const function_symbol& sqrt_doubleword()
      {
        static function_symbol sqrt_doubleword(sqrt_doubleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word()));
        return sqrt_doubleword;
      }
 
      inline
      bool is_sqrt_doubleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_doubleword();
        }
        return false;
      }
 
      
      inline
      application sqrt_doubleword(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::sqrt_doubleword()(arg0, arg1);
      }
 
      
      inline
      void make_sqrt_doubleword(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::sqrt_doubleword(),arg0, arg1);
      }
 
      inline
      bool is_sqrt_doubleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_doubleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void sqrt_doubleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void sqrt_doubleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==sqrt_doubleword());
        sqrt_doubleword_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& sqrt_tripleword_name()
      {
        static core::identifier_string sqrt_tripleword_name = core::identifier_string("@sqrt_tripleword");
        return sqrt_tripleword_name;
      }
 
      
      inline
      const function_symbol& sqrt_tripleword()
      {
        static function_symbol sqrt_tripleword(sqrt_tripleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word()));
        return sqrt_tripleword;
      }
 
      inline
      bool is_sqrt_tripleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_tripleword();
        }
        return false;
      }
 
      
      inline
      application sqrt_tripleword(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_machine_word::sqrt_tripleword()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_sqrt_tripleword(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_machine_word::sqrt_tripleword(),arg0, arg1, arg2);
      }
 
      inline
      bool is_sqrt_tripleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_tripleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void sqrt_tripleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void sqrt_tripleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==sqrt_tripleword());
        sqrt_tripleword_manual_implementation(result, a[0], a[1], a[2]);
      }
 
 
      inline
      const core::identifier_string& sqrt_tripleword_overflow_name()
      {
        static core::identifier_string sqrt_tripleword_overflow_name = core::identifier_string("@sqrt_tripleword_overflow");
        return sqrt_tripleword_overflow_name;
      }
 
      
      inline
      const function_symbol& sqrt_tripleword_overflow()
      {
        static function_symbol sqrt_tripleword_overflow(sqrt_tripleword_overflow_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word()));
        return sqrt_tripleword_overflow;
      }
 
      inline
      bool is_sqrt_tripleword_overflow_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_tripleword_overflow();
        }
        return false;
      }
 
      
      inline
      application sqrt_tripleword_overflow(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_machine_word::sqrt_tripleword_overflow()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_sqrt_tripleword_overflow(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_machine_word::sqrt_tripleword_overflow(),arg0, arg1, arg2);
      }
 
      inline
      bool is_sqrt_tripleword_overflow_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_tripleword_overflow_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void sqrt_tripleword_overflow_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void sqrt_tripleword_overflow_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==sqrt_tripleword_overflow());
        sqrt_tripleword_overflow_manual_implementation(result, a[0], a[1], a[2]);
      }
 
 
      inline
      const core::identifier_string& sqrt_quadrupleword_name()
      {
        static core::identifier_string sqrt_quadrupleword_name = core::identifier_string("@sqrt_quadrupleword");
        return sqrt_quadrupleword_name;
      }
 
      
      inline
      const function_symbol& sqrt_quadrupleword()
      {
        static function_symbol sqrt_quadrupleword(sqrt_quadrupleword_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word(), machine_word()));
        return sqrt_quadrupleword;
      }
 
      inline
      bool is_sqrt_quadrupleword_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_quadrupleword();
        }
        return false;
      }
 
      
      inline
      application sqrt_quadrupleword(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_machine_word::sqrt_quadrupleword()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_sqrt_quadrupleword(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_machine_word::sqrt_quadrupleword(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_sqrt_quadrupleword_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_quadrupleword_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void sqrt_quadrupleword_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3);
 
 
      inline
      void sqrt_quadrupleword_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==sqrt_quadrupleword());
        sqrt_quadrupleword_manual_implementation(result, a[0], a[1], a[2], a[3]);
      }
 
 
      inline
      const core::identifier_string& sqrt_quadrupleword_overflow_name()
      {
        static core::identifier_string sqrt_quadrupleword_overflow_name = core::identifier_string("@sqrt_quadrupleword_overflow");
        return sqrt_quadrupleword_overflow_name;
      }
 
      
      inline
      const function_symbol& sqrt_quadrupleword_overflow()
      {
        static function_symbol sqrt_quadrupleword_overflow(sqrt_quadrupleword_overflow_name(), make_function_sort_(machine_word(), machine_word(), machine_word(), machine_word(), machine_word()));
        return sqrt_quadrupleword_overflow;
      }
 
      inline
      bool is_sqrt_quadrupleword_overflow_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == sqrt_quadrupleword_overflow();
        }
        return false;
      }
 
      
      inline
      application sqrt_quadrupleword_overflow(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_machine_word::sqrt_quadrupleword_overflow()(arg0, arg1, arg2, arg3);
      }
 
      
      inline
      void make_sqrt_quadrupleword_overflow(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_machine_word::sqrt_quadrupleword_overflow(),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_sqrt_quadrupleword_overflow_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_sqrt_quadrupleword_overflow_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void sqrt_quadrupleword_overflow_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3);
 
 
      inline
      void sqrt_quadrupleword_overflow_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==sqrt_quadrupleword_overflow());
        sqrt_quadrupleword_overflow_manual_implementation(result, a[0], a[1], a[2], a[3]);
      }
 
 
      inline
      const core::identifier_string& pred_word_name()
      {
        static core::identifier_string pred_word_name = core::identifier_string("@pred_word");
        return pred_word_name;
      }
 
      
      inline
      const function_symbol& pred_word()
      {
        static function_symbol pred_word(pred_word_name(), make_function_sort_(machine_word(), machine_word()));
        return pred_word;
      }
 
      inline
      bool is_pred_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == pred_word();
        }
        return false;
      }
 
      
      inline
      application pred_word(const data_expression& arg0)
      {
        return sort_machine_word::pred_word()(arg0);
      }
 
      
      inline
      void make_pred_word(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::pred_word(),arg0);
      }
 
      inline
      bool is_pred_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_pred_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void pred_word_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void pred_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==pred_word());
        pred_word_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& equal_word_name()
      {
        static core::identifier_string equal_word_name = core::identifier_string("@equal");
        return equal_word_name;
      }
 
      
      inline
      const function_symbol& equal_word()
      {
        static function_symbol equal_word(equal_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return equal_word;
      }
 
      inline
      bool is_equal_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == equal_word();
        }
        return false;
      }
 
      
      inline
      application equal_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::equal_word()(arg0, arg1);
      }
 
      
      inline
      void make_equal_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::equal_word(),arg0, arg1);
      }
 
      inline
      bool is_equal_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_equal_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void equal_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void equal_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==equal_word());
        equal_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& not_equal_word_name()
      {
        static core::identifier_string not_equal_word_name = core::identifier_string("@not_equal");
        return not_equal_word_name;
      }
 
      
      inline
      const function_symbol& not_equal_word()
      {
        static function_symbol not_equal_word(not_equal_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return not_equal_word;
      }
 
      inline
      bool is_not_equal_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == not_equal_word();
        }
        return false;
      }
 
      
      inline
      application not_equal_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::not_equal_word()(arg0, arg1);
      }
 
      
      inline
      void make_not_equal_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::not_equal_word(),arg0, arg1);
      }
 
      inline
      bool is_not_equal_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_not_equal_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void not_equal_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void not_equal_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==not_equal_word());
        not_equal_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& less_word_name()
      {
        static core::identifier_string less_word_name = core::identifier_string("@less");
        return less_word_name;
      }
 
      
      inline
      const function_symbol& less_word()
      {
        static function_symbol less_word(less_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return less_word;
      }
 
      inline
      bool is_less_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == less_word();
        }
        return false;
      }
 
      
      inline
      application less_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::less_word()(arg0, arg1);
      }
 
      
      inline
      void make_less_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::less_word(),arg0, arg1);
      }
 
      inline
      bool is_less_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_less_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void less_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void less_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==less_word());
        less_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& less_equal_word_name()
      {
        static core::identifier_string less_equal_word_name = core::identifier_string("@less_equal");
        return less_equal_word_name;
      }
 
      
      inline
      const function_symbol& less_equal_word()
      {
        static function_symbol less_equal_word(less_equal_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return less_equal_word;
      }
 
      inline
      bool is_less_equal_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == less_equal_word();
        }
        return false;
      }
 
      
      inline
      application less_equal_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::less_equal_word()(arg0, arg1);
      }
 
      
      inline
      void make_less_equal_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::less_equal_word(),arg0, arg1);
      }
 
      inline
      bool is_less_equal_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_less_equal_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void less_equal_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void less_equal_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==less_equal_word());
        less_equal_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& greater_word_name()
      {
        static core::identifier_string greater_word_name = core::identifier_string("@greater");
        return greater_word_name;
      }
 
      
      inline
      const function_symbol& greater_word()
      {
        static function_symbol greater_word(greater_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return greater_word;
      }
 
      inline
      bool is_greater_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == greater_word();
        }
        return false;
      }
 
      
      inline
      application greater_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::greater_word()(arg0, arg1);
      }
 
      
      inline
      void make_greater_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::greater_word(),arg0, arg1);
      }
 
      inline
      bool is_greater_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_greater_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void greater_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void greater_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==greater_word());
        greater_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& greater_equal_word_name()
      {
        static core::identifier_string greater_equal_word_name = core::identifier_string("@greater_equal");
        return greater_equal_word_name;
      }
 
      
      inline
      const function_symbol& greater_equal_word()
      {
        static function_symbol greater_equal_word(greater_equal_word_name(), make_function_sort_(machine_word(), machine_word(), sort_bool::bool_()));
        return greater_equal_word;
      }
 
      inline
      bool is_greater_equal_word_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == greater_equal_word();
        }
        return false;
      }
 
      
      inline
      application greater_equal_word(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::greater_equal_word()(arg0, arg1);
      }
 
      
      inline
      void make_greater_equal_word(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::greater_equal_word(),arg0, arg1);
      }
 
      inline
      bool is_greater_equal_word_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_greater_equal_word_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void greater_equal_word_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void greater_equal_word_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==greater_equal_word());
        greater_equal_word_manual_implementation(result, a[0], a[1]);
      }
 
 
      inline
      const core::identifier_string& rightmost_bit_name()
      {
        static core::identifier_string rightmost_bit_name = core::identifier_string("@rightmost_bit");
        return rightmost_bit_name;
      }
 
      
      inline
      const function_symbol& rightmost_bit()
      {
        static function_symbol rightmost_bit(rightmost_bit_name(), make_function_sort_(machine_word(), sort_bool::bool_()));
        return rightmost_bit;
      }
 
      inline
      bool is_rightmost_bit_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == rightmost_bit();
        }
        return false;
      }
 
      
      inline
      application rightmost_bit(const data_expression& arg0)
      {
        return sort_machine_word::rightmost_bit()(arg0);
      }
 
      
      inline
      void make_rightmost_bit(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_machine_word::rightmost_bit(),arg0);
      }
 
      inline
      bool is_rightmost_bit_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_rightmost_bit_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void rightmost_bit_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void rightmost_bit_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==rightmost_bit());
        rightmost_bit_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& shift_right_name()
      {
        static core::identifier_string shift_right_name = core::identifier_string("@shift_right");
        return shift_right_name;
      }
 
      
      inline
      const function_symbol& shift_right()
      {
        static function_symbol shift_right(shift_right_name(), make_function_sort_(sort_bool::bool_(), machine_word(), machine_word()));
        return shift_right;
      }
 
      inline
      bool is_shift_right_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == shift_right();
        }
        return false;
      }
 
      
      inline
      application shift_right(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_machine_word::shift_right()(arg0, arg1);
      }
 
      
      inline
      void make_shift_right(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_machine_word::shift_right(),arg0, arg1);
      }
 
      inline
      bool is_shift_right_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_shift_right_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void shift_right_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1);
 
 
      inline
      void shift_right_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==shift_right());
        shift_right_manual_implementation(result, a[0], a[1]);
      }
 
      inline
      function_symbol_vector machine_word_generate_functions_code()
      {
        function_symbol_vector result;
        result.push_back(sort_machine_word::one_word());
        result.push_back(sort_machine_word::two_word());
        result.push_back(sort_machine_word::three_word());
        result.push_back(sort_machine_word::four_word());
        result.push_back(sort_machine_word::max_word());
        result.push_back(sort_machine_word::equals_zero_word());
        result.push_back(sort_machine_word::not_equals_zero_word());
        result.push_back(sort_machine_word::equals_one_word());
        result.push_back(sort_machine_word::equals_max_word());
        result.push_back(sort_machine_word::add_word());
        result.push_back(sort_machine_word::add_with_carry_word());
        result.push_back(sort_machine_word::add_overflow_word());
        result.push_back(sort_machine_word::add_with_carry_overflow_word());
        result.push_back(sort_machine_word::times_word());
        result.push_back(sort_machine_word::times_with_carry_word());
        result.push_back(sort_machine_word::times_overflow_word());
        result.push_back(sort_machine_word::times_with_carry_overflow_word());
        result.push_back(sort_machine_word::minus_word());
        result.push_back(sort_machine_word::monus_word());
        result.push_back(sort_machine_word::div_word());
        result.push_back(sort_machine_word::mod_word());
        result.push_back(sort_machine_word::sqrt_word());
        result.push_back(sort_machine_word::div_doubleword());
        result.push_back(sort_machine_word::div_double_doubleword());
        result.push_back(sort_machine_word::div_triple_doubleword());
        result.push_back(sort_machine_word::mod_doubleword());
        result.push_back(sort_machine_word::sqrt_doubleword());
        result.push_back(sort_machine_word::sqrt_tripleword());
        result.push_back(sort_machine_word::sqrt_tripleword_overflow());
        result.push_back(sort_machine_word::sqrt_quadrupleword());
        result.push_back(sort_machine_word::sqrt_quadrupleword_overflow());
        result.push_back(sort_machine_word::pred_word());
        result.push_back(sort_machine_word::equal_word());
        result.push_back(sort_machine_word::not_equal_word());
        result.push_back(sort_machine_word::less_word());
        result.push_back(sort_machine_word::less_equal_word());
        result.push_back(sort_machine_word::greater_word());
        result.push_back(sort_machine_word::greater_equal_word());
        result.push_back(sort_machine_word::rightmost_bit());
        result.push_back(sort_machine_word::shift_right());
        return result;
      }
      
      inline
      function_symbol_vector machine_word_generate_constructors_and_functions_code()
      {
        function_symbol_vector result=machine_word_generate_functions_code();
        for(const function_symbol& f: machine_word_generate_constructors_code())
        {
          result.push_back(f);
        }
        return result;
      }
      
      inline
      function_symbol_vector machine_word_mCRL2_usable_mappings()
      {
        function_symbol_vector result;
        result.push_back(sort_machine_word::one_word());
        result.push_back(sort_machine_word::two_word());
        result.push_back(sort_machine_word::three_word());
        result.push_back(sort_machine_word::four_word());
        result.push_back(sort_machine_word::max_word());
        result.push_back(sort_machine_word::equals_zero_word());
        result.push_back(sort_machine_word::not_equals_zero_word());
        result.push_back(sort_machine_word::equals_one_word());
        result.push_back(sort_machine_word::equals_max_word());
        result.push_back(sort_machine_word::add_word());
        result.push_back(sort_machine_word::add_with_carry_word());
        result.push_back(sort_machine_word::add_overflow_word());
        result.push_back(sort_machine_word::add_with_carry_overflow_word());
        result.push_back(sort_machine_word::times_word());
        result.push_back(sort_machine_word::times_with_carry_word());
        result.push_back(sort_machine_word::times_overflow_word());
        result.push_back(sort_machine_word::times_with_carry_overflow_word());
        result.push_back(sort_machine_word::minus_word());
        result.push_back(sort_machine_word::monus_word());
        result.push_back(sort_machine_word::div_word());
        result.push_back(sort_machine_word::mod_word());
        result.push_back(sort_machine_word::sqrt_word());
        result.push_back(sort_machine_word::div_doubleword());
        result.push_back(sort_machine_word::div_double_doubleword());
        result.push_back(sort_machine_word::div_triple_doubleword());
        result.push_back(sort_machine_word::mod_doubleword());
        result.push_back(sort_machine_word::sqrt_doubleword());
        result.push_back(sort_machine_word::sqrt_tripleword());
        result.push_back(sort_machine_word::sqrt_tripleword_overflow());
        result.push_back(sort_machine_word::sqrt_quadrupleword());
        result.push_back(sort_machine_word::sqrt_quadrupleword_overflow());
        result.push_back(sort_machine_word::pred_word());
        result.push_back(sort_machine_word::equal_word());
        result.push_back(sort_machine_word::not_equal_word());
        result.push_back(sort_machine_word::less_word());
        result.push_back(sort_machine_word::less_equal_word());
        result.push_back(sort_machine_word::greater_word());
        result.push_back(sort_machine_word::greater_equal_word());
        result.push_back(sort_machine_word::rightmost_bit());
        result.push_back(sort_machine_word::shift_right());
        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 machine_word_cpp_implementable_mappings()
      {
        implementation_map result;
        result[sort_machine_word::one_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::one_word_application,"sort_machine_word::one_word_manual_implementation");
        result[sort_machine_word::two_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::two_word_application,"sort_machine_word::two_word_manual_implementation");
        result[sort_machine_word::three_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::three_word_application,"sort_machine_word::three_word_manual_implementation");
        result[sort_machine_word::four_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::four_word_application,"sort_machine_word::four_word_manual_implementation");
        result[sort_machine_word::max_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::max_word_application,"sort_machine_word::max_word_manual_implementation");
        result[sort_machine_word::equals_zero_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::equals_zero_word_application,"sort_machine_word::equals_zero_word_manual_implementation");
        result[sort_machine_word::not_equals_zero_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::not_equals_zero_word_application,"sort_machine_word::not_equals_zero_word_manual_implementation");
        result[sort_machine_word::equals_one_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::equals_one_word_application,"sort_machine_word::equals_one_word_manual_implementation");
        result[sort_machine_word::equals_max_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::equals_max_word_application,"sort_machine_word::equals_max_word_manual_implementation");
        result[sort_machine_word::add_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::add_word_application,"sort_machine_word::add_word_manual_implementation");
        result[sort_machine_word::add_with_carry_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::add_with_carry_word_application,"sort_machine_word::add_with_carry_word_manual_implementation");
        result[sort_machine_word::add_overflow_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::add_overflow_word_application,"sort_machine_word::add_overflow_word_manual_implementation");
        result[sort_machine_word::add_with_carry_overflow_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::add_with_carry_overflow_word_application,"sort_machine_word::add_with_carry_overflow_word_manual_implementation");
        result[sort_machine_word::times_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::times_word_application,"sort_machine_word::times_word_manual_implementation");
        result[sort_machine_word::times_with_carry_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::times_with_carry_word_application,"sort_machine_word::times_with_carry_word_manual_implementation");
        result[sort_machine_word::times_overflow_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::times_overflow_word_application,"sort_machine_word::times_overflow_word_manual_implementation");
        result[sort_machine_word::times_with_carry_overflow_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::times_with_carry_overflow_word_application,"sort_machine_word::times_with_carry_overflow_word_manual_implementation");
        result[sort_machine_word::minus_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::minus_word_application,"sort_machine_word::minus_word_manual_implementation");
        result[sort_machine_word::monus_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::monus_word_application,"sort_machine_word::monus_word_manual_implementation");
        result[sort_machine_word::div_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::div_word_application,"sort_machine_word::div_word_manual_implementation");
        result[sort_machine_word::mod_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::mod_word_application,"sort_machine_word::mod_word_manual_implementation");
        result[sort_machine_word::sqrt_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::sqrt_word_application,"sort_machine_word::sqrt_word_manual_implementation");
        result[sort_machine_word::div_doubleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::div_doubleword_application,"sort_machine_word::div_doubleword_manual_implementation");
        result[sort_machine_word::div_double_doubleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::div_double_doubleword_application,"sort_machine_word::div_double_doubleword_manual_implementation");
        result[sort_machine_word::div_triple_doubleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::div_triple_doubleword_application,"sort_machine_word::div_triple_doubleword_manual_implementation");
        result[sort_machine_word::mod_doubleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::mod_doubleword_application,"sort_machine_word::mod_doubleword_manual_implementation");
        result[sort_machine_word::sqrt_doubleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::sqrt_doubleword_application,"sort_machine_word::sqrt_doubleword_manual_implementation");
        result[sort_machine_word::sqrt_tripleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::sqrt_tripleword_application,"sort_machine_word::sqrt_tripleword_manual_implementation");
        result[sort_machine_word::sqrt_tripleword_overflow()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::sqrt_tripleword_overflow_application,"sort_machine_word::sqrt_tripleword_overflow_manual_implementation");
        result[sort_machine_word::sqrt_quadrupleword()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::sqrt_quadrupleword_application,"sort_machine_word::sqrt_quadrupleword_manual_implementation");
        result[sort_machine_word::sqrt_quadrupleword_overflow()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::sqrt_quadrupleword_overflow_application,"sort_machine_word::sqrt_quadrupleword_overflow_manual_implementation");
        result[sort_machine_word::pred_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::pred_word_application,"sort_machine_word::pred_word_manual_implementation");
        result[sort_machine_word::equal_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::equal_word_application,"sort_machine_word::equal_word_manual_implementation");
        result[sort_machine_word::not_equal_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::not_equal_word_application,"sort_machine_word::not_equal_word_manual_implementation");
        result[sort_machine_word::less_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::less_word_application,"sort_machine_word::less_word_manual_implementation");
        result[sort_machine_word::less_equal_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::less_equal_word_application,"sort_machine_word::less_equal_word_manual_implementation");
        result[sort_machine_word::greater_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::greater_word_application,"sort_machine_word::greater_word_manual_implementation");
        result[sort_machine_word::greater_equal_word()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::greater_equal_word_application,"sort_machine_word::greater_equal_word_manual_implementation");
        result[sort_machine_word::rightmost_bit()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::rightmost_bit_application,"sort_machine_word::rightmost_bit_manual_implementation");
        result[sort_machine_word::shift_right()]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(sort_machine_word::shift_right_application,"sort_machine_word::shift_right_manual_implementation");
        return result;
      }
      inline
      const data_expression& arg(const data_expression& e)
      {
        assert(is_succ_word_application(e) || is_equals_zero_word_application(e) || is_not_equals_zero_word_application(e) || is_equals_one_word_application(e) || is_equals_max_word_application(e) || is_sqrt_word_application(e) || is_pred_word_application(e) || is_rightmost_bit_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& left(const data_expression& e)
      {
        assert(is_add_word_application(e) || is_add_with_carry_word_application(e) || is_add_overflow_word_application(e) || is_add_with_carry_overflow_word_application(e) || is_times_word_application(e) || is_times_overflow_word_application(e) || is_minus_word_application(e) || is_monus_word_application(e) || is_div_word_application(e) || is_mod_word_application(e) || is_equal_word_application(e) || is_not_equal_word_application(e) || is_less_word_application(e) || is_less_equal_word_application(e) || is_greater_word_application(e) || is_greater_equal_word_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& right(const data_expression& e)
      {
        assert(is_add_word_application(e) || is_add_with_carry_word_application(e) || is_add_overflow_word_application(e) || is_add_with_carry_overflow_word_application(e) || is_times_word_application(e) || is_times_overflow_word_application(e) || is_minus_word_application(e) || is_monus_word_application(e) || is_div_word_application(e) || is_mod_word_application(e) || is_equal_word_application(e) || is_not_equal_word_application(e) || is_less_word_application(e) || is_less_equal_word_application(e) || is_greater_word_application(e) || is_greater_equal_word_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg1(const data_expression& e)
      {
        assert(is_times_with_carry_word_application(e) || is_times_with_carry_overflow_word_application(e) || is_div_doubleword_application(e) || is_div_double_doubleword_application(e) || is_div_triple_doubleword_application(e) || is_mod_doubleword_application(e) || is_sqrt_doubleword_application(e) || is_sqrt_tripleword_application(e) || is_sqrt_tripleword_overflow_application(e) || is_sqrt_quadrupleword_application(e) || is_sqrt_quadrupleword_overflow_application(e) || is_shift_right_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg2(const data_expression& e)
      {
        assert(is_times_with_carry_word_application(e) || is_times_with_carry_overflow_word_application(e) || is_div_doubleword_application(e) || is_div_double_doubleword_application(e) || is_div_triple_doubleword_application(e) || is_mod_doubleword_application(e) || is_sqrt_doubleword_application(e) || is_sqrt_tripleword_application(e) || is_sqrt_tripleword_overflow_application(e) || is_sqrt_quadrupleword_application(e) || is_sqrt_quadrupleword_overflow_application(e) || is_shift_right_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg3(const data_expression& e)
      {
        assert(is_times_with_carry_word_application(e) || is_times_with_carry_overflow_word_application(e) || is_div_doubleword_application(e) || is_div_double_doubleword_application(e) || is_div_triple_doubleword_application(e) || is_mod_doubleword_application(e) || is_sqrt_tripleword_application(e) || is_sqrt_tripleword_overflow_application(e) || is_sqrt_quadrupleword_application(e) || is_sqrt_quadrupleword_overflow_application(e));
        return atermpp::down_cast<application>(e)[2];
      }
 
      inline
      const data_expression& arg4(const data_expression& e)
      {
        assert(is_div_double_doubleword_application(e) || is_div_triple_doubleword_application(e) || is_sqrt_quadrupleword_application(e) || is_sqrt_quadrupleword_overflow_application(e));
        return atermpp::down_cast<application>(e)[3];
      }
 
      inline
      const data_expression& arg5(const data_expression& e)
      {
        assert(is_div_triple_doubleword_application(e));
        return atermpp::down_cast<application>(e)[4];
      }
 
      inline
      data_equation_vector machine_word_generate_equations_code()
      {
        variable vw1("w1",machine_word());
        variable vw2("w2",machine_word());
 
        data_equation_vector result;
        result.push_back(data_equation(variable_list({vw1, vw2}), equal_to(vw1, vw2), equal_word(vw1, vw2)));
        result.push_back(data_equation(variable_list({vw1, vw2}), less(vw1, vw2), less_word(vw1, vw2)));
        result.push_back(data_equation(variable_list({vw1, vw2}), less_equal(vw1, vw2), less_equal_word(vw1, vw2)));
        return result;
      }
 
    } // namespace sort_machine_word
 
  } // namespace data
 
} // namespace mcrl2
 
#include "mcrl2/data/detail/machine_word.h" // This file contains the manual implementations of rewrite functions.
#endif // MCRL2_DATA_MACHINE_WORD_H