proposition: Theorem OpSem_deterministic: forall p, (forall e st st' r', ExpressionStep p e st st' r' -> forall st'' r'', ExpressionStep p e st st'' r'' -> st' = st'' /\ r' = r'') /\ (forall l st st' r', ListSteps p l st st' r' -> forall st'' r'', ListSteps p l st st'' r'' -> st' = st'' /\ r' = r'') /\ (forall m b st st' r', StatementStep p m b st st' r' -> forall st'' r'', StatementStep p m b st st'' r'' -> st' = st'' /\ r' = r'') /\ (forall m b st st' r', BlockStep p m b st st' r' -> forall st'' r'', BlockStep p m b st st'' r'' -> st' = st'' /\ r' = r'').
proof: Proof. intro p. apply mutual_ind; intros; simpl in *. inversion H11; try (rewrite H12 in H; discriminate H). subst. inversion H12. subst. destruct H2 with st4 (normal_step_v (Ref obj0)); trivial. inversion H0. subst. destruct H5 with st5 (normal_step_v v0); trivial. inversion H9. rewrite H in |- *. tauto. inversion H18; try (rewrite H19 in H; discriminate H). subst. inversion H19. subst. destruct H1 with st4 (normal_step_v (Ref this1)); trivial. inversion H7. subst. destruct H6 with st5 psnv0; trivial. subst. rewrite H2 in H21. inversion H21. subst. assert ((cn', m') = (cn'0, m'0)). apply (lookup_deterministic p cn0 (snd msig0) (cn', m') (cn'0, m'0)); trivial. inversion H. subst. rewrite H12 in H30; inversion H30; subst. rewrite H13 in H31; inversion H31; subst. rewrite H4 in H23; inversion H23; subst. destruct H15 with st_c'0 normal_step; trivial. subst. rewrite <- H16 in H33; inversion H33; subst. tauto. inversion H3; try (rewrite H4 in H; discriminate H). rewrite H4 in H. inversion H. subst. rewrite H0 in H5; inversion H5; subst. tauto. inversion H0. subst. tauto. discriminate H1. inversion H4; try (rewrite <- H6 in H; discriminate H). subst. inversion H5. subst. destruct H1 with st2 (normal_step_v v0); trivial. subst. inversion H8. subst. destruct H3 with st'' lr0; trivial. subst. tauto. inversion H2; try (rewrite H4 in H; discriminate H). subst. rewrite H3 in H; inversion H; subst. destruct H1 with st'' (normal_step_v v0); trivial. tauto. inversion H5; try (rewrite H6 in H; discriminate H). subst. destruct H1 with st2 normal_step; trivial. subst. rewrite H6 in H; inversion H; subst. destruct H4 with st'' normal_step; trivial. tauto. inversion H2; try (rewrite H3 in H; discriminate H). subst. destruct H1 with st'' normal_step; trivial. tauto. Qed.
imports: Coq(List) Coq(Relation_Operators)