# 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.

The problem, as illustrated on the left of Fig. 18, 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. 18 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. 18.