proposition: Lemma lem_big_to_small : forall c s s', c >> s ==> s' -> (c, s) -->* (Nop, s').
proof: Proof. intros c s s' H. induction H as [ | | | | | | b c s1 s2 ]. - sauto. - sauto. - sauto use: lem_seq_comp. - sauto. - sauto. - sauto. - assert ((While b Do c, s1) -->* (c;; While b Do c, s1)) by sauto. assert ((c;; While b Do c, s1) -->* (Nop;; While b Do c, s2)) by sauto use: lem_star_seq2. sauto. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia Relations