 The proofs start by assuming the premises of the rules. Then by using these assumptions, axioms and rules of PDL, and nothing else, the objective is to establish that the conclusion of the rules logically follows. Hence, for the rule of composition, we start by assuming {A}α1{B}, that is A → [α1]B in its PDL formulation, and by assuming {B}α2{C}, that is B → [α2]C. The objective is to prove that {A}α1;α2{C}. Precisely, we want to establish that A → [α1;α2]C is ⊢-deducible from the set of formulas {A → [α1]B, B → [α2]C}.