proposition: Theorem HoareSequenceRule : forall (P1 P2 P3:state->Prop)(i1 i2:inst)(s s':state), (forall s1 s2, exec s1 i1 s2 -> P1 s1 -> P2 s2)-> (forall s1 s2, exec s1 i2 s2 -> P2 s1 -> P3 s2)-> exec s (Sequence i1 i2) s' -> P1 s -> P3 s'.
proof: Proof. intros P1 P2 P3 i1 i2 s s' HP12 HP23 Hexec Hp1. inversion Hexec. match goal with id1 : exec s i1 _ , id2 : exec _ i2 s' |- _ => try (apply (HP23 _ _ id2); apply (HP12 _ _ id1); assumption) end. Qed.
imports: ZArith