Unification of Incremental CSET Specifications

When two complete CSET specifications are unified, the following rules are applied: assume that (cset (= a1) (== b1) (+ c1) (- d1)) is unified with (cset (= a2) (== b2) (+ c2) (- d2)),

1.

If both a1 and a2 are instantiated:

(a)

If (set-equal a1 a2) then:

i.

If c1 union c2 is included in a1, return (cset (= a1)) Else return :fail.

ii.

If d1 union d2 intersect with a1, return :fail Else return (cset (= a1))

(b)

else :fail.

2.

If only a1 is instantiated and a2 is null:

(a)

If a1 intersects d1 union d2, then :fail.

(b)

Else (cset (= a1)) is returned.

3.

If neither a1 and a2 is instantiated, compute the unions: b=b1 u b2, c=c1 u c2, d = d1 u d2, and return (cset (== b) (+ c) (- d)).