Theorem representing the regulatory loop involving MDM2, MDM2 and TP53 and leading to TP53 degradation: TP53& TP53& MDM2& U& P ⊢ d(TP53).

It is known that TP53, the well-known tumor suppressor [22] binds to the MDM2 gene and activates its transcription, ultimately leading synthesis of the MDM2 protein [23], [28]. But if TP53 binds the protein MDM2, this latter acts as a ubiquitin ligase, leading to TP53 ubiquitination and ultimately to its proteasomal degradation [29], an event that we indicate by d(TP53). Thus, a complex regulatory loop exists involving TP53, the MDM2 gene and the MDM2 protein. The reactions of this pathway are illustrated, in Zsyntax language, in the detailed form. In this form, the theorem is reported on line 27, the antecedent (IA, initial aggregate) is the multiset reported on line 1 and is “discharged” by the application of →I. Abbreviations: U, ubiquitin; P, proteasome. The reader can check that no formula (resource) is used more than once in the derivation process.