diff options
| -rw-r--r-- | src/hls/RTLPargenproof.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index df0615a..588f67f 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -742,7 +742,11 @@ Lemma sem_update : match_states st' st''' -> @step_instr A ge sp st''' x st'' -> exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst. -Proof. Admitted. +Proof. + intros. destruct x. + - inv H1. econstructor. simplify. eauto. symmetry; auto. + - inv H1. inv H0. econstructor. + Admitted. Lemma rtlblock_trans_correct : forall bb ge sp st st', |