Theorem representing the feed forward loop: A & A & B & C & RA& RA& RB ⊢ C.

A feed forward loop [30] is illustrated in the detailed form. In this form, the theorem is reported on line 35, the antecedent (IA, initial aggregate) is the multiset reported on line 1 and is “discharged” by the application of →I. The theorem illustrates the abstract case of a feed forward loop composed of three genes A, B, C, their encoded proteins (A, B, C), and two regulatory proteins RA and RB, such that (i) A is regulated by RA; (ii) B by RB and the protein A; (iii) C by the protein complex A*B. The reader can check that each formula (resource) is used at most once.