proposition: Lemma cexec_modified: forall x s1 c s2, cexec s1 c s2 -> ~modified_by c x -> s2 x = s1 x.
proof: Proof. induction 1; cbn; intros MB. - auto. - unfold update. destruct (string_dec x0 x); congruence. - rewrite IHcexec2, IHcexec1 by tauto. auto. - apply IHcexec. destruct (beval b s); tauto. - auto. - rewrite IHcexec2, IHcexec1 by tauto. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)