Lemma 4 ([Formula representation]). Let F be a field, and let f be computed by a noncommutative formula of size at most s , counting all vertices including scalar leaves. Then f is the value of an acyclic scalar/variable-labelled path …

Associate two vertices, an entrance and an exit, to each formula vertex. For a leaf, join its entrance to its exit by one edge labelled by the leaf's variable or scalar. At a sum gate, join its entrance to both child entrances and both child exits to its exit, using edges labelled 1 . At an ordered product gate, use edges labelled 1 from its entrance to the first child entrance, from the first child exit to the second child entrance, and from the second child exit to its exit. The child subtrees have disjoint vertices because the computation is a formula. Recursively order the vertices of each subtree with its entrance first, its first child subtree before its second, and its exit last. Every edge points forward in this ordering, so the graph is acyclic. A path through a sum gate chooses one of its two child programs; a path through a product gate traverses the two child programs in their prescribed order. Induction on the formula therefore shows that the program from the root entrance to the root exit has value f . There are two program vertices per formula vertex, including each scalar leaf. The claimed coefficient representation now follows from Lemma 3 ([Coefficient representation of a path program]).