Schema Disjunction Algorithm

First, convert the Exceptional Instance (e.g. Address Error) so that the "Xi" notation is substituted by the "Delta" notation. This is achived by substituting the "Xi-S" symbol with a "Delta-S" symbol and adding the axiom s=s', where s is the state schema in question (e.g. s=store).

Create the top part (signature part) of the disjoined schema (e.g. Assign) by merging the top parts of the Normal Instance(e.g Assign OK) and the Exceptional Instance (e.g. Address Error), so that each input and output variable is declared only once.

Split the bottom (axiom part) of the disjoined schema into two parts that are conected with the disjunction operator (logical OR). In the LHS part, copy the axiom part of the Normal Instance enclosed in square brackets and on the RHS copy the RHS of the exceptional schema enclosed in brackets. DO not forget that the axiom part of this schema will have an extra axiom (e.g. store=store')