diff options
-rw-r--r-- | backend/CSE3analysisproof.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index a012771c..29d171eb 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1341,6 +1341,20 @@ Section SOUNDNESS. unfold sem_rel in REL. eapply REL; eassumption. Qed. + + Lemma apply_cond_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel_b (apply_cond (ctx:=ctx) pc cond args rel) rs m). + Proof. + unfold apply_cond. + intros. + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. + Qed. (* Section INDUCTIVENESS. |