The

Restriction: Each of the <operator>s must have <sort> in its domain.<partitioned-by> ::=sort<sort>partitioned by<operator>+,

sort Set partitioned by \in sort Stack partitioned by isEmpty, top, pop

In general, LP translates a statement likewhen \A e (e \in s = e \in s1) yield s = s1 when isEmpty(s) = isEmpty(s1), top(s) = top(s1), pop(s) = pop(s1) yield s = s1

into to the deduction rulesort E partitioned by op1:E->R, op2:E,A->R, op3:E,E,A->R

which uses auxiliary variableswhen op1(e1) = op1(e2), \A a (op2(e1, a) = op2(e2, a)), \A a \A e3 (op3(e1, e3, a) = op3(e2, e3, a)), \A a \A e3 (op3(e3, e1, a) = op3(e3, e2, a)) yield e1 = e2