mCRL2
Loading...
Searching...
No Matches
list1.h
Go to the documentation of this file.
1// Author(s): Jeroen Keiren
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
14
15#ifndef MCRL2_DATA_LIST1_H
16#define MCRL2_DATA_LIST1_H
17
18#include "functional" // std::function
25#include "mcrl2/data/standard.h"
27#include "mcrl2/data/bool.h"
28#include "mcrl2/data/pos1.h"
29#include "mcrl2/data/nat1.h"
30
31namespace mcrl2 {
32
33 namespace data {
34
36 namespace sort_list {
37
41 inline
43 {
45 return list;
46 }
47
52 inline
53 bool is_list(const sort_expression& e)
54 {
55 if (is_container_sort(e))
56 {
58 }
59 return false;
60 }
61
62
65 inline
67 {
69 return empty_name;
70 }
71
75 inline
77 {
79 return empty;
80 }
81
85 inline
87 {
88 if (is_function_symbol(e))
89 {
90 return atermpp::down_cast<function_symbol>(e).name() == empty_name();
91 }
92 return false;
93 }
94
97 inline
99 {
101 return cons_name;
102 }
103
107 inline
109 {
111 return cons_;
112 }
113
117 inline
119 {
120 if (is_function_symbol(e))
121 {
122 return atermpp::down_cast<function_symbol>(e).name() == cons_name();
123 }
124 return false;
125 }
126
132 inline
134 {
135 return sort_list::cons_(s)(arg0, arg1);
136 }
137
143 inline
145 {
146 make_application(result, sort_list::cons_(s),arg0, arg1);
147 }
148
153 inline
155 {
156 return is_application(e) && is_cons_function_symbol(atermpp::down_cast<application>(e).head());
157 }
161 inline
163 {
165 result.push_back(sort_list::empty(s));
166 result.push_back(sort_list::cons_(s));
167
168 return result;
169 }
173 inline
175 {
177 result.push_back(sort_list::empty(s));
178 result.push_back(sort_list::cons_(s));
179
180 return result;
181 }
182 // 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
183 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
187 inline
189 {
190 implementation_map result;
191 static_cast< void >(s); // suppress unused variable warnings
192 return result;
193 }
194
197 inline
199 {
201 return in_name;
202 }
203
207 inline
209 {
211 return in;
212 }
213
217 inline
219 {
220 if (is_function_symbol(e))
221 {
222 return atermpp::down_cast<function_symbol>(e).name() == in_name();
223 }
224 return false;
225 }
226
232 inline
234 {
235 return sort_list::in(s)(arg0, arg1);
236 }
237
243 inline
244 void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
245 {
246 make_application(result, sort_list::in(s),arg0, arg1);
247 }
248
253 inline
255 {
256 return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
257 }
258
261 inline
263 {
265 return count_name;
266 }
267
271 inline
273 {
275 return count;
276 }
277
281 inline
283 {
284 if (is_function_symbol(e))
285 {
286 return atermpp::down_cast<function_symbol>(e).name() == count_name();
287 }
288 return false;
289 }
290
295 inline
297 {
298 return sort_list::count(s)(arg0);
299 }
300
305 inline
306 void make_count(data_expression& result, const sort_expression& s, const data_expression& arg0)
307 {
308 make_application(result, sort_list::count(s),arg0);
309 }
310
315 inline
317 {
318 return is_application(e) && is_count_function_symbol(atermpp::down_cast<application>(e).head());
319 }
320
323 inline
325 {
327 return snoc_name;
328 }
329
333 inline
335 {
337 return snoc;
338 }
339
343 inline
345 {
346 if (is_function_symbol(e))
347 {
348 return atermpp::down_cast<function_symbol>(e).name() == snoc_name();
349 }
350 return false;
351 }
352
358 inline
360 {
361 return sort_list::snoc(s)(arg0, arg1);
362 }
363
369 inline
371 {
372 make_application(result, sort_list::snoc(s),arg0, arg1);
373 }
374
379 inline
381 {
382 return is_application(e) && is_snoc_function_symbol(atermpp::down_cast<application>(e).head());
383 }
384
387 inline
389 {
391 return concat_name;
392 }
393
397 inline
399 {
401 return concat;
402 }
403
407 inline
409 {
410 if (is_function_symbol(e))
411 {
412 return atermpp::down_cast<function_symbol>(e).name() == concat_name();
413 }
414 return false;
415 }
416
422 inline
424 {
425 return sort_list::concat(s)(arg0, arg1);
426 }
427
433 inline
435 {
436 make_application(result, sort_list::concat(s),arg0, arg1);
437 }
438
443 inline
445 {
446 return is_application(e) && is_concat_function_symbol(atermpp::down_cast<application>(e).head());
447 }
448
451 inline
453 {
455 return element_at_name;
456 }
457
461 inline
463 {
465 return element_at;
466 }
467
471 inline
473 {
474 if (is_function_symbol(e))
475 {
476 return atermpp::down_cast<function_symbol>(e).name() == element_at_name();
477 }
478 return false;
479 }
480
486 inline
488 {
489 return sort_list::element_at(s)(arg0, arg1);
490 }
491
497 inline
499 {
501 }
502
507 inline
509 {
510 return is_application(e) && is_element_at_function_symbol(atermpp::down_cast<application>(e).head());
511 }
512
515 inline
517 {
519 return head_name;
520 }
521
525 inline
527 {
529 return head;
530 }
531
535 inline
537 {
538 if (is_function_symbol(e))
539 {
540 return atermpp::down_cast<function_symbol>(e).name() == head_name();
541 }
542 return false;
543 }
544
549 inline
551 {
552 return sort_list::head(s)(arg0);
553 }
554
559 inline
560 void make_head(data_expression& result, const sort_expression& s, const data_expression& arg0)
561 {
562 make_application(result, sort_list::head(s),arg0);
563 }
564
569 inline
571 {
572 return is_application(e) && is_head_function_symbol(atermpp::down_cast<application>(e).head());
573 }
574
577 inline
579 {
581 return tail_name;
582 }
583
587 inline
589 {
591 return tail;
592 }
593
597 inline
599 {
600 if (is_function_symbol(e))
601 {
602 return atermpp::down_cast<function_symbol>(e).name() == tail_name();
603 }
604 return false;
605 }
606
611 inline
613 {
614 return sort_list::tail(s)(arg0);
615 }
616
621 inline
622 void make_tail(data_expression& result, const sort_expression& s, const data_expression& arg0)
623 {
624 make_application(result, sort_list::tail(s),arg0);
625 }
626
631 inline
633 {
634 return is_application(e) && is_tail_function_symbol(atermpp::down_cast<application>(e).head());
635 }
636
639 inline
641 {
643 return rhead_name;
644 }
645
649 inline
651 {
653 return rhead;
654 }
655
659 inline
661 {
662 if (is_function_symbol(e))
663 {
664 return atermpp::down_cast<function_symbol>(e).name() == rhead_name();
665 }
666 return false;
667 }
668
673 inline
675 {
676 return sort_list::rhead(s)(arg0);
677 }
678
683 inline
684 void make_rhead(data_expression& result, const sort_expression& s, const data_expression& arg0)
685 {
686 make_application(result, sort_list::rhead(s),arg0);
687 }
688
693 inline
695 {
696 return is_application(e) && is_rhead_function_symbol(atermpp::down_cast<application>(e).head());
697 }
698
701 inline
703 {
705 return rtail_name;
706 }
707
711 inline
713 {
715 return rtail;
716 }
717
721 inline
723 {
724 if (is_function_symbol(e))
725 {
726 return atermpp::down_cast<function_symbol>(e).name() == rtail_name();
727 }
728 return false;
729 }
730
735 inline
737 {
738 return sort_list::rtail(s)(arg0);
739 }
740
745 inline
746 void make_rtail(data_expression& result, const sort_expression& s, const data_expression& arg0)
747 {
748 make_application(result, sort_list::rtail(s),arg0);
749 }
750
755 inline
757 {
758 return is_application(e) && is_rtail_function_symbol(atermpp::down_cast<application>(e).head());
759 }
763 inline
765 {
767 result.push_back(sort_list::in(s));
768 result.push_back(sort_list::count(s));
769 result.push_back(sort_list::snoc(s));
770 result.push_back(sort_list::concat(s));
771 result.push_back(sort_list::element_at(s));
772 result.push_back(sort_list::head(s));
773 result.push_back(sort_list::tail(s));
774 result.push_back(sort_list::rhead(s));
775 result.push_back(sort_list::rtail(s));
776 return result;
777 }
778
782 inline
784 {
787 {
788 result.push_back(f);
789 }
790 return result;
791 }
792
796 inline
798 {
800 result.push_back(sort_list::in(s));
801 result.push_back(sort_list::count(s));
802 result.push_back(sort_list::snoc(s));
803 result.push_back(sort_list::concat(s));
804 result.push_back(sort_list::element_at(s));
805 result.push_back(sort_list::head(s));
806 result.push_back(sort_list::tail(s));
807 result.push_back(sort_list::rhead(s));
808 result.push_back(sort_list::rtail(s));
809 return result;
810 }
811
812
813 // 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
814 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
818 inline
820 {
821 implementation_map result;
822 static_cast< void >(s); // suppress unused variable warnings
823 return result;
824 }
830 inline
832 {
834 return atermpp::down_cast<application>(e)[0];
835 }
836
842 inline
844 {
846 return atermpp::down_cast<application>(e)[1];
847 }
848
854 inline
856 {
858 return atermpp::down_cast<application>(e)[0];
859 }
860
864 inline
866 {
867 variable vd("d",s);
868 variable ve("e",s);
869 variable vs("s",list(s));
870 variable vt("t",list(s));
871 variable vp("p",sort_pos::pos());
872
874 result.push_back(data_equation(variable_list({vd, vs}), equal_to(empty(s), cons_(s, vd, vs)), sort_bool::false_()));
875 result.push_back(data_equation(variable_list({vd, vs}), equal_to(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
876 result.push_back(data_equation(variable_list({vd, ve, vs, vt}), equal_to(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::and_(equal_to(vd, ve), equal_to(vs, vt))));
877 result.push_back(data_equation(variable_list({vd, vs}), less(empty(s), cons_(s, vd, vs)), sort_bool::true_()));
878 result.push_back(data_equation(variable_list({vd, vs}), less(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
879 result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::or_(sort_bool::and_(equal_to(vd, ve), less(vs, vt)), less(vd, ve))));
880 result.push_back(data_equation(variable_list({vd, vs}), less_equal(empty(s), cons_(s, vd, vs)), sort_bool::true_()));
881 result.push_back(data_equation(variable_list({vd, vs}), less_equal(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
882 result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less_equal(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::or_(sort_bool::and_(equal_to(vd, ve), less_equal(vs, vt)), less(vd, ve))));
883 result.push_back(data_equation(variable_list({vd}), in(s, vd, empty(s)), sort_bool::false_()));
884 result.push_back(data_equation(variable_list({vd, ve, vs}), in(s, vd, cons_(s, ve, vs)), sort_bool::or_(equal_to(vd, ve), in(s, vd, vs))));
885 result.push_back(data_equation(variable_list(), count(s, empty(s)), sort_nat::c0()));
886 result.push_back(data_equation(variable_list({vd, vs}), count(s, cons_(s, vd, vs)), sort_nat::cnat(sort_nat::succ(count(s, vs)))));
887 result.push_back(data_equation(variable_list({vd}), snoc(s, empty(s), vd), cons_(s, vd, empty(s))));
888 result.push_back(data_equation(variable_list({vd, ve, vs}), snoc(s, cons_(s, vd, vs), ve), cons_(s, vd, snoc(s, vs, ve))));
889 result.push_back(data_equation(variable_list({vs}), concat(s, empty(s), vs), vs));
890 result.push_back(data_equation(variable_list({vd, vs, vt}), concat(s, cons_(s, vd, vs), vt), cons_(s, vd, concat(s, vs, vt))));
891 result.push_back(data_equation(variable_list({vs}), concat(s, vs, empty(s)), vs));
892 result.push_back(data_equation(variable_list({vd, vs}), element_at(s, cons_(s, vd, vs), sort_nat::c0()), vd));
893 result.push_back(data_equation(variable_list({vd, vp, vs}), element_at(s, cons_(s, vd, vs), sort_nat::cnat(vp)), element_at(s, vs, sort_nat::pred(vp))));
894 result.push_back(data_equation(variable_list({vd, vs}), head(s, cons_(s, vd, vs)), vd));
895 result.push_back(data_equation(variable_list({vd, vs}), tail(s, cons_(s, vd, vs)), vs));
896 result.push_back(data_equation(variable_list({vd}), rhead(s, cons_(s, vd, empty(s))), vd));
897 result.push_back(data_equation(variable_list({vd, ve, vs}), rhead(s, cons_(s, vd, cons_(s, ve, vs))), rhead(s, cons_(s, ve, vs))));
898 result.push_back(data_equation(variable_list({vd}), rtail(s, cons_(s, vd, empty(s))), empty(s)));
899 result.push_back(data_equation(variable_list({vd, ve, vs}), rtail(s, cons_(s, vd, cons_(s, ve, vs))), cons_(s, vd, rtail(s, cons_(s, ve, vs)))));
900 return result;
901 }
902
903 } // namespace sort_list
904
905 } // namespace data
906
907} // namespace mcrl2
908
909#endif // MCRL2_DATA_LIST1_H
The class application.
The class basic_sort.
The standard sort bool_.
Term containing a string.
An application of a data expression to a number of arguments.
\brief A container sort
const container_type & container_name() const
\brief A data equation
\brief A function symbol
\brief Container type for lists
\brief A sort expression
\brief A data variable
Definition variable.h:28
The class container_sort.
The class function symbol.
The class data_equation.
Exception classes for use in libraries and tools.
The class function_sort.
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:299
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
const core::identifier_string & rtail_name()
Generate identifier rtail.
Definition list1.h:702
const core::identifier_string & snoc_name()
Generate identifier <|.
Definition list1.h:324
bool is_rhead_function_symbol(const atermpp::aterm &e)
Recogniser for function rhead.
Definition list1.h:660
bool is_rhead_application(const atermpp::aterm &e)
Recogniser for application of rhead.
Definition list1.h:694
bool is_snoc_function_symbol(const atermpp::aterm &e)
Recogniser for function <|.
Definition list1.h:344
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition list1.h:282
function_symbol_vector list_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for list.
Definition list1.h:174
const core::identifier_string & tail_name()
Generate identifier tail.
Definition list1.h:578
bool is_tail_application(const atermpp::aterm &e)
Recogniser for application of tail.
Definition list1.h:632
bool is_element_at_function_symbol(const atermpp::aterm &e)
Recogniser for function ..
Definition list1.h:472
void make_snoc(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol <|.
Definition list1.h:370
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition list1.h:218
const core::identifier_string & rhead_name()
Generate identifier rhead.
Definition list1.h:640
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings for list.
Definition list1.h:764
implementation_map list_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for list.
Definition list1.h:819
const core::identifier_string & in_name()
Generate identifier in.
Definition list1.h:198
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition list1.h:208
bool is_rtail_function_symbol(const atermpp::aterm &e)
Recogniser for function rtail.
Definition list1.h:722
bool is_concat_application(const atermpp::aterm &e)
Recogniser for application of ++.
Definition list1.h:444
const core::identifier_string & head_name()
Generate identifier head.
Definition list1.h:516
const core::identifier_string & cons_name()
Generate identifier |>.
Definition list1.h:98
const core::identifier_string & concat_name()
Generate identifier ++.
Definition list1.h:388
function_symbol rtail(const sort_expression &s)
Constructor for function symbol rtail.
Definition list1.h:712
const core::identifier_string & count_name()
Generate identifier #.
Definition list1.h:262
void make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol |>.
Definition list1.h:144
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
Definition list1.h:865
void make_rhead(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rhead.
Definition list1.h:684
bool is_tail_function_symbol(const atermpp::aterm &e)
Recogniser for function tail.
Definition list1.h:598
function_symbol_vector list_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for list.
Definition list1.h:797
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition list1.h:254
implementation_map list_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition list1.h:188
function_symbol_vector list_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for list.
Definition list1.h:783
bool is_rtail_application(const atermpp::aterm &e)
Recogniser for application of rtail.
Definition list1.h:756
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
Definition list1.h:76
function_symbol element_at(const sort_expression &s)
Constructor for function symbol ..
Definition list1.h:462
const core::identifier_string & empty_name()
Generate identifier [].
Definition list1.h:66
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
Definition list1.h:162
void make_concat(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ++.
Definition list1.h:434
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition list1.h:244
const core::identifier_string & element_at_name()
Generate identifier ..
Definition list1.h:452
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:526
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of |>.
Definition list1.h:154
bool is_snoc_application(const atermpp::aterm &e)
Recogniser for application of <|.
Definition list1.h:380
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition list1.h:183
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list1.h:42
function_symbol snoc(const sort_expression &s)
Constructor for function symbol <|.
Definition list1.h:334
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition list1.h:272
bool is_element_at_application(const atermpp::aterm &e)
Recogniser for application of ..
Definition list1.h:508
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition list1.h:831
void make_head(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol head.
Definition list1.h:560
function_symbol rhead(const sort_expression &s)
Constructor for function symbol rhead.
Definition list1.h:650
void make_element_at(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ..
Definition list1.h:498
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition list1.h:316
void make_rtail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rtail.
Definition list1.h:746
bool is_head_application(const atermpp::aterm &e)
Recogniser for application of head.
Definition list1.h:570
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition list1.h:306
function_symbol tail(const sort_expression &s)
Constructor for function symbol tail.
Definition list1.h:588
void make_tail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol tail.
Definition list1.h:622
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
Definition list1.h:108
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function |>.
Definition list1.h:118
bool is_concat_function_symbol(const atermpp::aterm &e)
Recogniser for function ++.
Definition list1.h:408
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition list1.h:855
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition list1.h:843
bool is_head_function_symbol(const atermpp::aterm &e)
Recogniser for function head.
Definition list1.h:536
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function [].
Definition list1.h:86
function_symbol concat(const sort_expression &s)
Constructor for function symbol ++.
Definition list1.h:398
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
Definition list1.h:53
function_symbol succ(const sort_expression &s0)
Definition nat1.h:584
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:108
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
const function_symbol & pred()
Constructor for function symbol pred.
Definition nat1.h:648
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
atermpp::term_list< variable > variable_list
\brief list of variables
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
void make_application(atermpp::aterm &result)
Make function for an application.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Standard functions that are available for all sorts.