Downward Flow

It is not uncommon to find a theorem statement in the literature that draws two conclusions C1 and C2 (which we would represent in Proofscape as two nodes Thm.C1 and Thm.C2), and having a proof that first deduces conclusion C1 and then goes on to use C1 together with further argumentation in order to deduce conclusion C2.

In Proofscape, due to the unidirectional flow convention for diagrams, such a proof must be broken into two separate deductions.

Fig. 24 On the left, downward flow conflicts with multiple conclusions. On the right, we solve the problem by splitting into two proofs.

The problem, as illustrated on the left of Fig. 24, is that when the first conclusion node Thm.C1 is used in combination with further argumentation in the proof, the diagram has to have an arrow that goes backwards, terminating higher in the diagram than it originates.

Backward arrows like the arrow from Thm.C1 to A4 in Fig. 24 are not allowed in Proofscape. One reason for this is that this breaks the desired visual convention, in which the argument always flows in one direction. Another reason is that such backward edges can be hard for layout algorithms to handle.

The solution is simply to break the proof into two deductions, as illustrated on the right in Fig. 24.