From b8823bfa481e4322e809d600624c59634447ec4d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 9 Jan 2020 17:50:12 +0100 Subject: nearly done --- backend/ForwardMovesproof.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'backend/ForwardMovesproof.v') diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index b1425401..8c036851 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -468,10 +468,12 @@ Proof. subst args. rewrite MOVE in GE. simpl in H0. - destruct (map # pc') as [mpc' | ] in *; try discriminate. simpl in GE. - admit. - admit. + apply get_rb_sem_ge with (rb2 := Some (move src res mpc)). + assumption. + replace v with (rs # src) by congruence. + apply move_ok. + assumption. } admit. -- cgit