The JoinProcessor is responsible for executing the joining. Let N1 and N2 be
the nodes which should be joined and let N be the node where the branches of
N1 and N2 join. Further let F be the given decision formula. Then the
following steps are applied:
- Based on the formulas contained in n1 and n2 and the given decision
formula F, a further Formula F' created which is used for the second step.
- Based on F' the delayed-cut mechanism is applied on N.
- The created update in F' is simplified.
The delayed-cut mechanism prunes the proof at a common predecessor,
introduces a cut for a defined decision predicate, and replays the existing
proof afterward. Note that by the means of this approach, there are no
non-local rule applications in the resulting proof. This avoids certain
complications arising from a "defocusing" join rule that establishes a link
between a join node and its partner. However, replaying does not work in
every case, for instance if a subtree of the common parent introduces new
symbols.