diff options
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
-rw-r--r-- | src/hls/GiblePargenproofBackward.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index ebb2744..93b1778 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -67,7 +67,7 @@ Context (prog: GibleSeq.program) (tprog : GiblePar.program). Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. -Lemma sem_equiv_execution : +(*Lemma sem_equiv_execution : forall sp x i i' ti cf x' ti', abstract_sequence x = Some x' -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> @@ -81,7 +81,7 @@ Lemma sem_exists_execution : abstract_sequence x = Some x' -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf). -Proof. Admitted. +Proof. Admitted. *) Lemma abstr_seq_reverse_correct : forall sp x i i' ti cf x', @@ -91,9 +91,10 @@ Lemma abstr_seq_reverse_correct : exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - intros. exploit sem_exists_execution; eauto; simplify. +(* intros. exploit sem_exists_execution; eauto; simplify. eauto using sem_equiv_execution. -Qed. +Qed. *) + intros. (*| Proof Sketch: |