iSet.key

\sorts {
    Free;  // Built into KeY, do not change! Can be accessed in JML via \free.
}

\functions {
    Free iSet_empty;
    Free iSet_singleton(int);
    Free iSet_minus(Free, Free);
    Free iSet_union(Free, Free);
    Free iSet_intersect(Free, Free);
}

\predicates {
    in(int, Free);
    subseteq(Free, Free);
}

\schemaVariables {
    \term int x, y;
    \term Free setA, setB;
    \variable int iv;
}

\rules {
    inEmpty {
        \find(in(x, iSet_empty))
        \replacewith(false)
        \heuristics(concrete)
    };

    inSingleton {
        \find(in(x, iSet_singleton(y)))
        \replacewith(x = y)
        \heuristics(concrete)
    };

    inSetMinus {
        \find(in(x, iSet_minus(setA, setB)))
        \replacewith(in(x, setA) & !in(x,setB))
        \heuristics(simplify)
    };

    inSetUnion {
        \find(in(x, iSet_union(setA, setB)))
        \replacewith(in(x, setA) | in(x,setB))
        \heuristics(simplify)
    };

    inSetIntersect {
        \find(in(x, iSet_intersect(setA, setB)))
        \replacewith(in(x, setA) & in(x, setB))
        \heuristics(simplify)
    };


    setEq {
        \find(setA = setB)
        \varcond(\notFreeIn(iv, setA, setB))
        \replacewith(\forall iv; (in(iv, setA) <-> in(iv, setB)))
    };
}