bag1.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_BAG1_H
#define MCRL2_DATA_BAG1_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/forall.h"
#include "mcrl2/data/container_sort.h"
#include "mcrl2/data/nat1.h"
#include "mcrl2/data/fbag1.h"
#include "mcrl2/data/fset1.h"
#include "mcrl2/data/set1.h"
 
namespace mcrl2 {
 
  namespace data {
 
    namespace sort_bag {
 
      inline
      container_sort bag(const sort_expression& s)
      {
        container_sort bag(bag_container(), s);
        return bag;
      }
 
      inline
      bool is_bag(const sort_expression& e)
      {
        if (is_container_sort(e))
        {
          return container_sort(e).container_name() == bag_container();
        }
        return false;
      }
 
 
      inline
      const core::identifier_string& constructor_name()
      {
        static core::identifier_string constructor_name = core::identifier_string("@bag");
        return constructor_name;
      }
 
      inline
      function_symbol constructor(const sort_expression& s)
      {
        function_symbol constructor(constructor_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), sort_fbag::fbag(s), bag(s)));
        return constructor;
      }
 
      inline
      bool is_constructor_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == constructor_name();
        }
        return false;
      }
 
      inline
      application constructor(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::constructor(s)(arg0, arg1);
      }
 
      inline
      void make_constructor(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::constructor(s),arg0, arg1);
      }
 
      inline
      bool is_constructor_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_constructor_function_symbol(atermpp::down_cast<application>(e).head());
      }
      inline
      function_symbol_vector bag_generate_constructors_code(const sort_expression& s)
      {
        function_symbol_vector result;
        result.push_back(sort_bag::constructor(s));
 
        return result;
      }
      inline
      function_symbol_vector bag_mCRL2_usable_constructors(const sort_expression& s)
      {
        function_symbol_vector result;
        result.push_back(sort_bag::constructor(s));
 
        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 bag_cpp_implementable_constructors(const sort_expression& s)
      {
        implementation_map result;
        static_cast< void >(s); // suppress unused variable warnings
        return result;
      }
 
      inline
      const core::identifier_string& bag_fbag_name()
      {
        static core::identifier_string bag_fbag_name = core::identifier_string("@bagfbag");
        return bag_fbag_name;
      }
 
      inline
      function_symbol bag_fbag(const sort_expression& s)
      {
        function_symbol bag_fbag(bag_fbag_name(), make_function_sort_(sort_fbag::fbag(s), bag(s)));
        return bag_fbag;
      }
 
      inline
      bool is_bag_fbag_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == bag_fbag_name();
        }
        return false;
      }
 
      inline
      application bag_fbag(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::bag_fbag(s)(arg0);
      }
 
      inline
      void make_bag_fbag(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::bag_fbag(s),arg0);
      }
 
      inline
      bool is_bag_fbag_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_bag_fbag_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& bag_comprehension_name()
      {
        static core::identifier_string bag_comprehension_name = core::identifier_string("@bagcomp");
        return bag_comprehension_name;
      }
 
      inline
      function_symbol bag_comprehension(const sort_expression& s)
      {
        function_symbol bag_comprehension(bag_comprehension_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), bag(s)));
        return bag_comprehension;
      }
 
      inline
      bool is_bag_comprehension_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == bag_comprehension_name();
        }
        return false;
      }
 
      inline
      application bag_comprehension(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::bag_comprehension(s)(arg0);
      }
 
      inline
      void make_bag_comprehension(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::bag_comprehension(s),arg0);
      }
 
      inline
      bool is_bag_comprehension_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_bag_comprehension_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& count_name()
      {
        static core::identifier_string count_name = core::identifier_string("count");
        return count_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol count(const sort_expression& , const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort(sort_nat::nat());
        function_symbol count(count_name(), make_function_sort_(s0, s1, target_sort));
        return count;
      }
 
      inline
      bool is_count_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == count_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
        }
        return false;
      }
 
      inline
      application count(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::count(s, arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      inline
      void make_count(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::count(s, arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_count_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_count_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& in_name()
      {
        static core::identifier_string in_name = core::identifier_string("in");
        return in_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol in(const sort_expression& , const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort(sort_bool::bool_());
        function_symbol in(in_name(), make_function_sort_(s0, s1, target_sort));
        return in;
      }
 
      inline
      bool is_in_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == in_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
        }
        return false;
      }
 
      inline
      application in(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::in(s, arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      inline
      void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::in(s, arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_in_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& union_name()
      {
        static core::identifier_string union_name = core::identifier_string("+");
        return union_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol union_(const sort_expression& s, const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == bag(s) && s1 == bag(s))
        {
          target_sort = bag(s);
        }
        else if (s0 == sort_set::set_(s) && s1 == sort_set::set_(s))
        {
          target_sort = sort_set::set_(s);
        }
        else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
        {
          target_sort = sort_fset::fset(s);
        }
        else if (s0 == sort_fbag::fbag(s) && s1 == sort_fbag::fbag(s))
        {
          target_sort = sort_fbag::fbag(s);
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for union_ with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol union_(union_name(), make_function_sort_(s0, s1, target_sort));
        return union_;
      }
 
      inline
      bool is_union_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == union_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
        }
        return false;
      }
 
      inline
      application union_(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::union_(s, arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      inline
      void make_union_(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::union_(s, arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_union_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_union_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& intersection_name()
      {
        static core::identifier_string intersection_name = core::identifier_string("*");
        return intersection_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol intersection(const sort_expression& s, const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == bag(s) && s1 == bag(s))
        {
          target_sort = bag(s);
        }
        else if (s0 == sort_fbag::fbag(s) && s1 == bag(s))
        {
          target_sort = sort_fbag::fbag(s);
        }
        else if (s0 == bag(s) && s1 == sort_fbag::fbag(s))
        {
          target_sort = sort_fbag::fbag(s);
        }
        else if (s0 == sort_set::set_(s) && s1 == sort_set::set_(s))
        {
          target_sort = sort_set::set_(s);
        }
        else if (s0 == sort_fset::fset(s) && s1 == sort_set::set_(s))
        {
          target_sort = sort_fset::fset(s);
        }
        else if (s0 == sort_set::set_(s) && s1 == sort_fset::fset(s))
        {
          target_sort = sort_fset::fset(s);
        }
        else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
        {
          target_sort = sort_fset::fset(s);
        }
        else if (s0 == sort_fbag::fbag(s) && s1 == sort_fbag::fbag(s))
        {
          target_sort = sort_fbag::fbag(s);
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for intersection with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol intersection(intersection_name(), make_function_sort_(s0, s1, target_sort));
        return intersection;
      }
 
      inline
      bool is_intersection_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == intersection_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
        }
        return false;
      }
 
      inline
      application intersection(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::intersection(s, arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      inline
      void make_intersection(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::intersection(s, arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_intersection_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_intersection_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& difference_name()
      {
        static core::identifier_string difference_name = core::identifier_string("-");
        return difference_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol difference(const sort_expression& s, const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == bag(s) && s1 == bag(s))
        {
          target_sort = bag(s);
        }
        else if (s0 == sort_fbag::fbag(s) && s1 == bag(s))
        {
          target_sort = sort_fbag::fbag(s);
        }
        else if (s0 == sort_set::set_(s) && s1 == sort_set::set_(s))
        {
          target_sort = sort_set::set_(s);
        }
        else if (s0 == sort_fset::fset(s) && s1 == sort_set::set_(s))
        {
          target_sort = sort_fset::fset(s);
        }
        else if (s0 == sort_fset::fset(s) && s1 == sort_fset::fset(s))
        {
          target_sort = sort_fset::fset(s);
        }
        else if (s0 == sort_fbag::fbag(s) && s1 == sort_fbag::fbag(s))
        {
          target_sort = sort_fbag::fbag(s);
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for difference with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol difference(difference_name(), make_function_sort_(s0, s1, target_sort));
        return difference;
      }
 
      inline
      bool is_difference_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == difference_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2;
        }
        return false;
      }
 
      inline
      application difference(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::difference(s, arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      inline
      void make_difference(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::difference(s, arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_difference_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_difference_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& bag2set_name()
      {
        static core::identifier_string bag2set_name = core::identifier_string("Bag2Set");
        return bag2set_name;
      }
 
      inline
      function_symbol bag2set(const sort_expression& s)
      {
        function_symbol bag2set(bag2set_name(), make_function_sort_(bag(s), sort_set::set_(s)));
        return bag2set;
      }
 
      inline
      bool is_bag2set_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == bag2set_name();
        }
        return false;
      }
 
      inline
      application bag2set(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::bag2set(s)(arg0);
      }
 
      inline
      void make_bag2set(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::bag2set(s),arg0);
      }
 
      inline
      bool is_bag2set_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_bag2set_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& set2bag_name()
      {
        static core::identifier_string set2bag_name = core::identifier_string("Set2Bag");
        return set2bag_name;
      }
 
      inline
      function_symbol set2bag(const sort_expression& s)
      {
        function_symbol set2bag(set2bag_name(), make_function_sort_(sort_set::set_(s), bag(s)));
        return set2bag;
      }
 
      inline
      bool is_set2bag_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == set2bag_name();
        }
        return false;
      }
 
      inline
      application set2bag(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::set2bag(s)(arg0);
      }
 
      inline
      void make_set2bag(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::set2bag(s),arg0);
      }
 
      inline
      bool is_set2bag_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_set2bag_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& zero_function_name()
      {
        static core::identifier_string zero_function_name = core::identifier_string("@zero_");
        return zero_function_name;
      }
 
      inline
      function_symbol zero_function(const sort_expression& s)
      {
        function_symbol zero_function(zero_function_name(), make_function_sort_(s, sort_nat::nat()));
        return zero_function;
      }
 
      inline
      bool is_zero_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == zero_function_name();
        }
        return false;
      }
 
      inline
      application zero_function(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::zero_function(s)(arg0);
      }
 
      inline
      void make_zero_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::zero_function(s),arg0);
      }
 
      inline
      bool is_zero_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_zero_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& one_function_name()
      {
        static core::identifier_string one_function_name = core::identifier_string("@one_");
        return one_function_name;
      }
 
      inline
      function_symbol one_function(const sort_expression& s)
      {
        function_symbol one_function(one_function_name(), make_function_sort_(s, sort_nat::nat()));
        return one_function;
      }
 
      inline
      bool is_one_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == one_function_name();
        }
        return false;
      }
 
      inline
      application one_function(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::one_function(s)(arg0);
      }
 
      inline
      void make_one_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::one_function(s),arg0);
      }
 
      inline
      bool is_one_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_one_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& add_function_name()
      {
        static core::identifier_string add_function_name = core::identifier_string("@add_");
        return add_function_name;
      }
 
      inline
      function_symbol add_function(const sort_expression& s)
      {
        function_symbol add_function(add_function_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat())));
        return add_function;
      }
 
      inline
      bool is_add_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == add_function_name();
        }
        return false;
      }
 
      inline
      application add_function(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::add_function(s)(arg0, arg1);
      }
 
      inline
      void make_add_function(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::add_function(s),arg0, arg1);
      }
 
      inline
      bool is_add_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_add_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& min_function_name()
      {
        static core::identifier_string min_function_name = core::identifier_string("@min_");
        return min_function_name;
      }
 
      inline
      function_symbol min_function(const sort_expression& s)
      {
        function_symbol min_function(min_function_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat())));
        return min_function;
      }
 
      inline
      bool is_min_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == min_function_name();
        }
        return false;
      }
 
      inline
      application min_function(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::min_function(s)(arg0, arg1);
      }
 
      inline
      void make_min_function(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::min_function(s),arg0, arg1);
      }
 
      inline
      bool is_min_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_min_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& monus_function_name()
      {
        static core::identifier_string monus_function_name = core::identifier_string("@monus_");
        return monus_function_name;
      }
 
      inline
      function_symbol monus_function(const sort_expression& s)
      {
        function_symbol monus_function(monus_function_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat())));
        return monus_function;
      }
 
      inline
      bool is_monus_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == monus_function_name();
        }
        return false;
      }
 
      inline
      application monus_function(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::monus_function(s)(arg0, arg1);
      }
 
      inline
      void make_monus_function(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::monus_function(s),arg0, arg1);
      }
 
      inline
      bool is_monus_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_monus_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& nat2bool_function_name()
      {
        static core::identifier_string nat2bool_function_name = core::identifier_string("@Nat2Bool_");
        return nat2bool_function_name;
      }
 
      inline
      function_symbol nat2bool_function(const sort_expression& s)
      {
        function_symbol nat2bool_function(nat2bool_function_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_bool::bool_())));
        return nat2bool_function;
      }
 
      inline
      bool is_nat2bool_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == nat2bool_function_name();
        }
        return false;
      }
 
      inline
      application nat2bool_function(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::nat2bool_function(s)(arg0);
      }
 
      inline
      void make_nat2bool_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::nat2bool_function(s),arg0);
      }
 
      inline
      bool is_nat2bool_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_nat2bool_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& bool2nat_function_name()
      {
        static core::identifier_string bool2nat_function_name = core::identifier_string("@Bool2Nat_");
        return bool2nat_function_name;
      }
 
      inline
      function_symbol bool2nat_function(const sort_expression& s)
      {
        function_symbol bool2nat_function(bool2nat_function_name(), make_function_sort_(make_function_sort_(s, sort_bool::bool_()), make_function_sort_(s, sort_nat::nat())));
        return bool2nat_function;
      }
 
      inline
      bool is_bool2nat_function_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == bool2nat_function_name();
        }
        return false;
      }
 
      inline
      application bool2nat_function(const sort_expression& s, const data_expression& arg0)
      {
        return sort_bag::bool2nat_function(s)(arg0);
      }
 
      inline
      void make_bool2nat_function(data_expression& result, const sort_expression& s, const data_expression& arg0)
      {
        make_application(result, sort_bag::bool2nat_function(s),arg0);
      }
 
      inline
      bool is_bool2nat_function_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_bool2nat_function_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& fbag_join_name()
      {
        static core::identifier_string fbag_join_name = core::identifier_string("@fbag_join");
        return fbag_join_name;
      }
 
      inline
      function_symbol fbag_join(const sort_expression& s)
      {
        function_symbol fbag_join(fbag_join_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat()), sort_fbag::fbag(s), sort_fbag::fbag(s), sort_fbag::fbag(s)));
        return fbag_join;
      }
 
      inline
      bool is_fbag_join_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == fbag_join_name();
        }
        return false;
      }
 
      inline
      application fbag_join(const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_bag::fbag_join(s)(arg0, arg1, arg2, arg3);
      }
 
      inline
      void make_fbag_join(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_bag::fbag_join(s),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_fbag_join_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_fbag_join_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& fbag_intersect_name()
      {
        static core::identifier_string fbag_intersect_name = core::identifier_string("@fbag_inter");
        return fbag_intersect_name;
      }
 
      inline
      function_symbol fbag_intersect(const sort_expression& s)
      {
        function_symbol fbag_intersect(fbag_intersect_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat()), sort_fbag::fbag(s), sort_fbag::fbag(s), sort_fbag::fbag(s)));
        return fbag_intersect;
      }
 
      inline
      bool is_fbag_intersect_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == fbag_intersect_name();
        }
        return false;
      }
 
      inline
      application fbag_intersect(const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_bag::fbag_intersect(s)(arg0, arg1, arg2, arg3);
      }
 
      inline
      void make_fbag_intersect(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_bag::fbag_intersect(s),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_fbag_intersect_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_fbag_intersect_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& fbag_difference_name()
      {
        static core::identifier_string fbag_difference_name = core::identifier_string("@fbag_diff");
        return fbag_difference_name;
      }
 
      inline
      function_symbol fbag_difference(const sort_expression& s)
      {
        function_symbol fbag_difference(fbag_difference_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), make_function_sort_(s, sort_nat::nat()), sort_fbag::fbag(s), sort_fbag::fbag(s), sort_fbag::fbag(s)));
        return fbag_difference;
      }
 
      inline
      bool is_fbag_difference_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == fbag_difference_name();
        }
        return false;
      }
 
      inline
      application fbag_difference(const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        return sort_bag::fbag_difference(s)(arg0, arg1, arg2, arg3);
      }
 
      inline
      void make_fbag_difference(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2, const data_expression& arg3)
      {
        make_application(result, sort_bag::fbag_difference(s),arg0, arg1, arg2, arg3);
      }
 
      inline
      bool is_fbag_difference_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_fbag_difference_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& fbag2fset_name()
      {
        static core::identifier_string fbag2fset_name = core::identifier_string("@fbag2fset");
        return fbag2fset_name;
      }
 
      inline
      function_symbol fbag2fset(const sort_expression& s)
      {
        function_symbol fbag2fset(fbag2fset_name(), make_function_sort_(make_function_sort_(s, sort_nat::nat()), sort_fbag::fbag(s), sort_fset::fset(s)));
        return fbag2fset;
      }
 
      inline
      bool is_fbag2fset_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == fbag2fset_name();
        }
        return false;
      }
 
      inline
      application fbag2fset(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        return sort_bag::fbag2fset(s)(arg0, arg1);
      }
 
      inline
      void make_fbag2fset(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_bag::fbag2fset(s),arg0, arg1);
      }
 
      inline
      bool is_fbag2fset_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_fbag2fset_function_symbol(atermpp::down_cast<application>(e).head());
      }
      inline
      function_symbol_vector bag_generate_functions_code(const sort_expression& s)
      {
        function_symbol_vector result;
        result.push_back(sort_bag::bag_fbag(s));
        result.push_back(sort_bag::bag_comprehension(s));
        result.push_back(sort_bag::count(s, s, bag(s)));
        result.push_back(sort_bag::in(s, s, bag(s)));
        result.push_back(sort_bag::union_(s, bag(s), bag(s)));
        result.push_back(sort_bag::intersection(s, bag(s), bag(s)));
        result.push_back(sort_bag::intersection(s, sort_fbag::fbag(s), bag(s)));
        result.push_back(sort_bag::intersection(s, bag(s), sort_fbag::fbag(s)));
        result.push_back(sort_bag::difference(s, bag(s), bag(s)));
        result.push_back(sort_bag::difference(s, sort_fbag::fbag(s), bag(s)));
        result.push_back(sort_bag::bag2set(s));
        result.push_back(sort_bag::set2bag(s));
        result.push_back(sort_bag::zero_function(s));
        result.push_back(sort_bag::one_function(s));
        result.push_back(sort_bag::add_function(s));
        result.push_back(sort_bag::min_function(s));
        result.push_back(sort_bag::monus_function(s));
        result.push_back(sort_bag::nat2bool_function(s));
        result.push_back(sort_bag::bool2nat_function(s));
        result.push_back(sort_bag::fbag_join(s));
        result.push_back(sort_bag::fbag_intersect(s));
        result.push_back(sort_bag::fbag_difference(s));
        result.push_back(sort_bag::fbag2fset(s));
        return result;
      }
      
      inline
      function_symbol_vector bag_generate_constructors_and_functions_code(const sort_expression& s)
      {
        function_symbol_vector result=bag_generate_functions_code(s);
        for(const function_symbol& f: bag_generate_constructors_code(s))
        {
          result.push_back(f);
        }
        return result;
      }
      
      inline
      function_symbol_vector bag_mCRL2_usable_mappings(const sort_expression& s)
      {
        function_symbol_vector result;
        result.push_back(sort_bag::bag_fbag(s));
        result.push_back(sort_bag::bag_comprehension(s));
        result.push_back(sort_bag::count(s, s, bag(s)));
        result.push_back(sort_bag::in(s, s, bag(s)));
        result.push_back(sort_bag::union_(s, bag(s), bag(s)));
        result.push_back(sort_bag::intersection(s, bag(s), bag(s)));
        result.push_back(sort_bag::intersection(s, sort_fbag::fbag(s), bag(s)));
        result.push_back(sort_bag::intersection(s, bag(s), sort_fbag::fbag(s)));
        result.push_back(sort_bag::difference(s, bag(s), bag(s)));
        result.push_back(sort_bag::difference(s, sort_fbag::fbag(s), bag(s)));
        result.push_back(sort_bag::bag2set(s));
        result.push_back(sort_bag::set2bag(s));
        result.push_back(sort_bag::zero_function(s));
        result.push_back(sort_bag::one_function(s));
        result.push_back(sort_bag::add_function(s));
        result.push_back(sort_bag::min_function(s));
        result.push_back(sort_bag::monus_function(s));
        result.push_back(sort_bag::nat2bool_function(s));
        result.push_back(sort_bag::bool2nat_function(s));
        result.push_back(sort_bag::fbag_join(s));
        result.push_back(sort_bag::fbag_intersect(s));
        result.push_back(sort_bag::fbag_difference(s));
        result.push_back(sort_bag::fbag2fset(s));
        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 bag_cpp_implementable_mappings(const sort_expression& s)
      {
        implementation_map result;
        static_cast< void >(s); // suppress unused variable warnings
        return result;
      }
      inline
      const data_expression& left(const data_expression& e)
      {
        assert(is_constructor_application(e) || is_count_application(e) || is_in_application(e) || is_union_application(e) || is_intersection_application(e) || is_difference_application(e) || is_add_function_application(e) || is_min_function_application(e) || is_monus_function_application(e) || is_fbag2fset_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& right(const data_expression& e)
      {
        assert(is_constructor_application(e) || is_count_application(e) || is_in_application(e) || is_union_application(e) || is_intersection_application(e) || is_difference_application(e) || is_add_function_application(e) || is_min_function_application(e) || is_monus_function_application(e) || is_fbag2fset_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg(const data_expression& e)
      {
        assert(is_bag_fbag_application(e) || is_bag_comprehension_application(e) || is_bag2set_application(e) || is_set2bag_application(e) || is_zero_function_application(e) || is_one_function_application(e) || is_nat2bool_function_application(e) || is_bool2nat_function_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg1(const data_expression& e)
      {
        assert(is_fbag_join_application(e) || is_fbag_intersect_application(e) || is_fbag_difference_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg2(const data_expression& e)
      {
        assert(is_fbag_join_application(e) || is_fbag_intersect_application(e) || is_fbag_difference_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg3(const data_expression& e)
      {
        assert(is_fbag_join_application(e) || is_fbag_intersect_application(e) || is_fbag_difference_application(e));
        return atermpp::down_cast<application>(e)[2];
      }
 
      inline
      const data_expression& arg4(const data_expression& e)
      {
        assert(is_fbag_join_application(e) || is_fbag_intersect_application(e) || is_fbag_difference_application(e));
        return atermpp::down_cast<application>(e)[3];
      }
 
      inline
      data_equation_vector bag_generate_equations_code(const sort_expression& s)
      {
        variable vb("b",sort_fbag::fbag(s));
        variable vc("c",sort_fbag::fbag(s));
        variable vd("d",s);
        variable ve("e",s);
        variable vf("f",make_function_sort_(s, sort_nat::nat()));
        variable vg("g",make_function_sort_(s, sort_nat::nat()));
        variable vh("h",make_function_sort_(s, sort_bool::bool_()));
        variable vp("p",sort_pos::pos());
        variable vq("q",sort_pos::pos());
        variable vs("s",sort_fset::fset(s));
        variable vx("x",bag(s));
        variable vy("y",bag(s));
 
        data_equation_vector result;
        result.push_back(data_equation(variable_list({vb}), bag_fbag(s, vb), constructor(s, zero_function(s), vb)));
        result.push_back(data_equation(variable_list({vf}), sort_bag::bag_comprehension(s, vf), constructor(s, vf, sort_fbag::empty(s))));
        result.push_back(data_equation(variable_list({vb, ve, vf}), count(s, ve, constructor(s, vf, vb)), sort_nat::swap_zero(vf(ve), count(s, ve, vb))));
        result.push_back(data_equation(variable_list({ve, vx}), in(s, ve, vx), greater(count(s, ve, vx), sort_nat::c0())));
        result.push_back(data_equation(variable_list({vb, vc, vf, vg}), equal_to(constructor(s, vf, vb), constructor(s, vg, vc)), if_(equal_to(vf, vg), equal_to(vb, vc), forall(variable_list({vd}), equal_to(count(s, vd, constructor(s, vf, vb)), count(s, vd, constructor(s, vg, vc)))))));
        result.push_back(data_equation(variable_list({vx, vy}), less(vx, vy), sort_bool::and_(less_equal(vx, vy), not_equal_to(vx, vy))));
        result.push_back(data_equation(variable_list({vx, vy}), less_equal(vx, vy), equal_to(intersection(s, vx, vy), vx)));
        result.push_back(data_equation(variable_list({vb, vc, vf, vg}), union_(s, constructor(s, vf, vb), constructor(s, vg, vc)), constructor(s, add_function(s, vf, vg), fbag_join(s, vf, vg, vb, vc))));
        result.push_back(data_equation(variable_list({vx}), intersection(s, vx, vx), vx));
        result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vx, vy)), intersection(s, vx, vy)));
        result.push_back(data_equation(variable_list({vx, vy}), intersection(s, vx, intersection(s, vy, vx)), intersection(s, vy, vx)));
        result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vx, vy), vx), intersection(s, vx, vy)));
        result.push_back(data_equation(variable_list({vx, vy}), intersection(s, intersection(s, vy, vx), vx), intersection(s, vy, vx)));
        result.push_back(data_equation(variable_list({vb, vc, vf, vg}), intersection(s, constructor(s, vf, vb), constructor(s, vg, vc)), constructor(s, min_function(s, vf, vg), fbag_intersect(s, vf, vg, vb, vc))));
        result.push_back(data_equation(variable_list({vx}), intersection(s, sort_fbag::empty(s), vx), sort_fbag::empty(s)));
        result.push_back(data_equation(variable_list({vb, vd, vp, vx}), intersection(s, sort_fbag::cons_(s, vd, vp, vb), vx), if_(in(s, vd, vx), sort_fbag::cons_(s, vd, sort_nat::minimum(vp, sort_nat::nat2pos(count(s, vd, vx))), intersection(s, vb, vx)), intersection(s, vb, vx))));
        result.push_back(data_equation(variable_list({vb, vx}), intersection(s, vx, vb), intersection(s, vb, vx)));
        result.push_back(data_equation(variable_list({vb, vc, vf, vg}), difference(s, constructor(s, vf, vb), constructor(s, vg, vc)), constructor(s, monus_function(s, vf, vg), fbag_difference(s, vf, vg, vb, vc))));
        result.push_back(data_equation(variable_list({vx}), difference(s, sort_fbag::empty(s), vx), sort_fbag::empty(s)));
        result.push_back(data_equation(variable_list({vb, vd, vp, vx}), difference(s, sort_fbag::cons_(s, vd, vp, vb), vx), if_(greater(sort_nat::pos2nat(vp), count(s, vd, vx)), sort_fbag::cons_(s, vd, sort_nat::nat2pos(sort_nat::monus(sort_nat::pos2nat(vp), count(s, vd, vx))), difference(s, vb, vx)), difference(s, vb, vx))));
        result.push_back(data_equation(variable_list({vb, vf}), bag2set(s, constructor(s, vf, vb)), sort_set::constructor(s, nat2bool_function(s, vf), fbag2fset(s, vf, vb))));
        result.push_back(data_equation(variable_list({vh, vs}), set2bag(s, sort_set::constructor(s, vh, vs)), constructor(s, bool2nat_function(s, vh), sort_fbag::fset2fbag(s, vs))));
        result.push_back(data_equation(variable_list({ve}), zero_function(s, ve), sort_nat::c0()));
        result.push_back(data_equation(variable_list({ve}), one_function(s, ve), sort_nat::cnat(sort_pos::c1())));
        result.push_back(data_equation(variable_list(), equal_to(zero_function(s), one_function(s)), sort_bool::false_()));
        result.push_back(data_equation(variable_list(), equal_to(one_function(s), zero_function(s)), sort_bool::false_()));
        result.push_back(data_equation(variable_list({ve, vf, vg}), add_function(s, vf, vg)(ve), sort_nat::plus(vf(ve), vg(ve))));
        result.push_back(data_equation(variable_list({vf}), add_function(s, vf, zero_function(s)), vf));
        result.push_back(data_equation(variable_list({vf}), add_function(s, zero_function(s), vf), vf));
        result.push_back(data_equation(variable_list({ve, vf, vg}), min_function(s, vf, vg)(ve), sort_nat::minimum(vf(ve), vg(ve))));
        result.push_back(data_equation(variable_list({vf}), min_function(s, vf, vf), vf));
        result.push_back(data_equation(variable_list({vf}), min_function(s, vf, zero_function(s)), zero_function(s)));
        result.push_back(data_equation(variable_list({vf}), min_function(s, zero_function(s), vf), zero_function(s)));
        result.push_back(data_equation(variable_list({ve, vf, vg}), monus_function(s, vf, vg)(ve), sort_nat::monus(vf(ve), vg(ve))));
        result.push_back(data_equation(variable_list({vf}), monus_function(s, vf, vf), zero_function(s)));
        result.push_back(data_equation(variable_list({vf}), monus_function(s, vf, zero_function(s)), vf));
        result.push_back(data_equation(variable_list({vf}), monus_function(s, zero_function(s), vf), zero_function(s)));
        result.push_back(data_equation(variable_list({ve, vf}), nat2bool_function(s, vf)(ve), greater(vf(ve), sort_nat::c0())));
        result.push_back(data_equation(variable_list(), nat2bool_function(s, zero_function(s)), sort_set::false_function(s)));
        result.push_back(data_equation(variable_list(), nat2bool_function(s, one_function(s)), sort_set::true_function(s)));
        result.push_back(data_equation(variable_list({ve, vh}), bool2nat_function(s, vh)(ve), if_(vh(ve), sort_nat::cnat(sort_pos::c1()), sort_nat::c0())));
        result.push_back(data_equation(variable_list(), bool2nat_function(s, sort_set::false_function(s)), zero_function(s)));
        result.push_back(data_equation(variable_list(), bool2nat_function(s, sort_set::true_function(s)), one_function(s)));
        result.push_back(data_equation(variable_list({vf, vg}), fbag_join(s, vf, vg, sort_fbag::empty(s), sort_fbag::empty(s)), sort_fbag::empty(s)));
        result.push_back(data_equation(variable_list({vb, vd, vf, vg, vp}), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::empty(s)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_add(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_join(s, vf, vg, vb, sort_fbag::empty(s)))));
        result.push_back(data_equation(variable_list({vc, ve, vf, vg, vq}), fbag_join(s, vf, vg, sort_fbag::empty(s), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_add(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_join(s, vf, vg, sort_fbag::empty(s), vc))));
        result.push_back(data_equation(variable_list({vb, vc, vd, vf, vg, vp, vq}), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, vd, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_add(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::cnat(vq)), fbag_join(s, vf, vg, vb, vc))));
        result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(vd, ve), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_add(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_join(s, vf, vg, vb, sort_fbag::cons_(s, ve, vq, vc)))));
        result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(ve, vd), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_add(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_join(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), vc))));
        result.push_back(data_equation(variable_list({vf, vg}), fbag_intersect(s, vf, vg, sort_fbag::empty(s), sort_fbag::empty(s)), sort_fbag::empty(s)));
        result.push_back(data_equation(variable_list({vb, vd, vf, vg, vp}), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::empty(s)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_min(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_intersect(s, vf, vg, vb, sort_fbag::empty(s)))));
        result.push_back(data_equation(variable_list({vc, ve, vf, vg, vq}), fbag_intersect(s, vf, vg, sort_fbag::empty(s), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_min(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_intersect(s, vf, vg, sort_fbag::empty(s), vc))));
        result.push_back(data_equation(variable_list({vb, vc, vd, vf, vg, vp, vq}), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, vd, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_min(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::cnat(vq)), fbag_intersect(s, vf, vg, vb, vc))));
        result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(vd, ve), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_min(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_intersect(s, vf, vg, vb, sort_fbag::cons_(s, ve, vq, vc)))));
        result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(ve, vd), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_min(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_intersect(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), vc))));
        result.push_back(data_equation(variable_list({vf, vg}), fbag_difference(s, vf, vg, sort_fbag::empty(s), sort_fbag::empty(s)), sort_fbag::empty(s)));
        result.push_back(data_equation(variable_list({vb, vd, vf, vg, vp}), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::empty(s)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_monus(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_difference(s, vf, vg, vb, sort_fbag::empty(s)))));
        result.push_back(data_equation(variable_list({vc, ve, vf, vg, vq}), fbag_difference(s, vf, vg, sort_fbag::empty(s), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_monus(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_difference(s, vf, vg, sort_fbag::empty(s), vc))));
        result.push_back(data_equation(variable_list({vb, vc, vd, vf, vg, vp, vq}), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, vd, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_monus(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::cnat(vq)), fbag_difference(s, vf, vg, vb, vc))));
        result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(vd, ve), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, vd, sort_nat::swap_zero_monus(vf(vd), vg(vd), sort_nat::cnat(vp), sort_nat::c0()), fbag_difference(s, vf, vg, vb, sort_fbag::cons_(s, ve, vq, vc)))));
        result.push_back(data_equation(variable_list({vb, vc, vd, ve, vf, vg, vp, vq}), less(ve, vd), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), sort_fbag::cons_(s, ve, vq, vc)), sort_fbag::cinsert(s, ve, sort_nat::swap_zero_monus(vf(ve), vg(ve), sort_nat::c0(), sort_nat::cnat(vq)), fbag_difference(s, vf, vg, sort_fbag::cons_(s, vd, vp, vb), vc))));
        result.push_back(data_equation(variable_list({vf}), fbag2fset(s, vf, sort_fbag::empty(s)), sort_fset::empty(s)));
        result.push_back(data_equation(variable_list({vb, vd, vf, vp}), fbag2fset(s, vf, sort_fbag::cons_(s, vd, vp, vb)), sort_fset::cinsert(s, vd, equal_to(equal_to(vf(vd), sort_nat::cnat(vp)), greater(vf(vd), sort_nat::c0())), fbag2fset(s, vf, vb))));
        return result;
      }
 
    } // namespace sort_bag
 
  } // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_BAG1_H