B.3.3 split: Split Proof State

B.3.3 split: Split Proof State

Synopsis

Alternative Invocations

• Button : split
• Formula Menu [F]: split F

Applicable

In proving mode.

Description

This command generates two or more child states by splitting some selected formula according to some of the rules listed below (there is at most one rule applicable). The form split may only applied in a proof state with a single goal which is thus implicitly selected for splitting. The form split F explicitly selects the formula (assumption or goal) with label S for splitting. The rules are applied recursively to the generated child states by splitting the formulas resulting from the previous split until no more splitting is possible. If no rule is applicable for splitting the selected formula, no child state is generated.

The applied rules are:

[E] ..., A_1, ... |- ... 
[E] ..., A_2, ... |- ...
...
[E] ..., A_n, ... |- ...
---------------------------------------------
[E] ..., A_1 \/ A_2 \/ ... \/ A_n, ... |- ...

[E] ... |- ..., A_1, ... 
[E] ... |- ..., A_2, ... 
... 
[E] ... |- ..., A_n, ... 
--------------------------------------------
[E] ... |- ..., A_1 \/ A_2 \/ ... \/ A_n,...

[E] ..., ~A_1, ... |- ... 
[E] ..., A_2, ... |- ... 
-------------------------------
[E] ..., A_1 => A_2,...  |- ...

[E] ... |- ..., A_1 => A_2, ... 
[E] ... |- ..., A_2 => A_1, ... 
-------------------------------
[E] ... |- ..., A_1 <=> A_2,... 

[E] ... |- ..., A_1 => ~A_2, ... 
[E] ... |- ..., A_2 => ~A_1, ... 
--------------------------------
[E] ... |- ..., A_1 xor A_2,... 

Pragmatics

By the recursive application of the rules, e.g. a single application of split to the assumption of the proof state

[E] A \/ (B => C \/ D) |- ...

generates four child states:

[E]  A |- ...
[E] ~B |- ...
[E]  C |- ...
[E]  D |- ...

The command is used by the command scatter.

B.3.3 split: Split Proof State