diff options
| -rw-r--r-- | backend/ForwardMovesproof.v | 8 |
1 files changed, 5 insertions, 3 deletions
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. |