diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 17:37:54 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 17:37:54 +0100 |
| commit | fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794 (patch) | |
| tree | 13682e172f9d723768fe8b81d0b0471a0e8ad2ce /src/hls/Gible.v | |
| parent | fe286deeb5c8a81aad20b81cd2ce9a586cc99dca (diff) | |
| download | vericert-fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794.tar.gz vericert-fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794.zip | |
Finish abstr_seq_reverse_correct_fold
Diffstat (limited to 'src/hls/Gible.v')
| -rw-r--r-- | src/hls/Gible.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index b7959be..d7b0e66 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -440,6 +440,17 @@ Proof. repeat constructor; inv H; erewrite eval_predf_pr_equiv; eauto. Qed. +Lemma step_exists_Iterm: + forall sp i instr ti cf, + step_instr sp (Iexec i) instr (Iterm i cf) -> + state_equiv i ti -> + step_instr sp (Iexec ti) instr (Iterm ti cf). +Proof. + inversion_clear 1; subst; intros. + econstructor. + inv H. eapply truthy_match_state; eauto. +Qed. + End RELABSTR. (*| |