merc_syntax 2.0.0

% Author(s): Aad Mathijssen, 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)
%
% Specification of the Set data sort.

cons @set: (S -> Bool) # FSet(S) -> Set(S);
% I think that @setfset and @setcomp should not be part of the rewrite system, but
% become part of the internal generation of set representations. JFG
map @setfset: FSet(S) -> Set(S);
    @setcomp: (S -> Bool) -> Set(S);
    in: S # Set(S) -> Bool;
    !: Set(S) -> Set(S);
    +: Set(S) # Set(S) -> Set(S);
    *: Set(S) # Set(S) -> Set(S);
    *: FSet(S) # Set(S) -> FSet(S);
    *: Set(S) # FSet(S) -> FSet(S);
    -: Set(S) # Set(S) -> Set(S);
    -: FSet(S) # Set(S) -> FSet(S);
    @false_: S -> Bool;
    @true_: S -> Bool;
    @not_: (S -> Bool) -> S -> Bool;
    @and_: (S -> Bool) # (S -> Bool) -> S -> Bool;
    @or_: (S -> Bool) # (S -> Bool) -> S -> Bool;
    @fset_union: (S -> Bool) # (S -> Bool) # FSet(S) # FSet(S) -> FSet(S);
    @fset_inter: (S -> Bool) # (S -> Bool) # FSet(S) # FSet(S) -> FSet(S);

var d : S;
    e : S;
    s : FSet(S);
    t : FSet(S);
    f : S->Bool;
    g : S->Bool;
    x : Set(S);
    y : Set(S);

eqn @setfset(s)  =  @set(@false_, s);
    @setcomp(f)  =  @set(f, {});
    in(e, @set(f, s))  =  f(e) != in(e, s);
    @set(f, s) == @set(g, t)  =  forall c:S. (f(c) == g(c)) == (in(c,s) == in(c,t));
    x < y  = (x <= y) && (x != y);
    x <= y = x * y == x;
    !(@set(f, s))  =  @set(@not_(f), s);
    x + x = x;
    x + (x + y) = x + y;
    x + (y + x) = y + x;
    (x + y) + x = x + y;
    (y + x) + x = y + x;
    @set(f, s) + @set(g, t)  =  @set(@or_(f, g), @fset_union(f, g, s, t));
    x * x = x;
    x * (x * y) = x * y;
    x * (y * x) = y * x;
    (x * y) * x = x * y;
    (y * x) * x = y * x;
    @set(f, s) * @set(g, t)  =  @set(@and_(f, g), @fset_inter(f, g, s, t));
    {} * x = {};
    @fset_cons(d, s) * x = if(in(d, x), @fset_cons(d, s * x), s * x);
    x * s = s * x;
    x - y =  x * !(y);
    s - x = s * !(x);
    @false_(e)  =  false;
    @true_(e)  =  true;
    @false_ == @true_  =  false;
    @true_ == @false_  =  false;
    @not_(f)(e)  =  !(f(e));
    @not_(@false_)  =  @true_;
    @not_(@true_)  =  @false_;
    @and_(f, g)(e)  =  f(e) && g(e);
    @and_(f, f)  =  f;
    @and_(f, @false_)  =  @false_;
    @and_(@false_, f)  =  @false_;
    @and_(f, @true_)  =  f;
    @and_(@true_, f)  =  f;
    @or_(f, f)  =  f;
    @or_(f, @false_)  =  f;
    @or_(@false_, f)  =  f;
    @or_(f, @true_)  =  @true_;
    @or_(@true_, f)  =  @true_;
    @or_(f, g)(e)  =  f(e) || g(e);
    @fset_union(@false_, @false_, s, t)  = s + t;
    @fset_union(f, g, {}, {})  =  {};
    @fset_union(f, g, @fset_cons(d, s), {})  =  @fset_cinsert(d, !(g(d)), @fset_union(f, g, s, {}));
    @fset_union(f, g, {}, @fset_cons(e, t))  =  @fset_cinsert(e, !(f(e)), @fset_union(f, g, {}, t));
    @fset_union(f, g, @fset_cons(d, s), @fset_cons(d, t))  =  @fset_cinsert(d, f(d) == g(d), @fset_union(f, g, s, t));
    d < e  ->  @fset_union(f, g, @fset_cons(d, s), @fset_cons(e, t))  =  @fset_cinsert(d, !(g(d)), @fset_union(f, g, s, @fset_cons(e, t)));
    e < d  ->  @fset_union(f, g, @fset_cons(d, s), @fset_cons(e, t))  =  @fset_cinsert(e, !(f(e)), @fset_union(f, g, @fset_cons(d, s), t));
    @fset_inter(f, g, {}, {})  =  {};
    @fset_inter(f, g, @fset_cons(d, s), {})  =  @fset_cinsert(d, g(d), @fset_inter(f, g, s, {}));
    @fset_inter(f, g, {}, @fset_cons(e, t))  =  @fset_cinsert(e, f(e), @fset_inter(f, g, {}, t));
    @fset_inter(f, g, @fset_cons(d, s), @fset_cons(d, t))  =  @fset_cinsert(d, f(d) == g(d), @fset_inter(f, g, s, t));
    d < e  ->  @fset_inter(f, g, @fset_cons(d, s), @fset_cons(e, t))  =  @fset_cinsert(d, g(d), @fset_inter(f, g, s, @fset_cons(e, t)));
    e < d  ->  @fset_inter(f, g, @fset_cons(d, s), @fset_cons(e, t))  =  @fset_cinsert(e, f(e), @fset_inter(f, g, @fset_cons(d, s), t));