proposition: Theorem rac2_equiv_assignables_correct: forall p, (forall e st st' s, OpRac2.ExpressionStep p e st st' s -> EquivAssignables p st st') /\ (forall l st st' s, OpRac2.ListSteps p l st st' s -> EquivAssignables p st st') /\ (forall m b st st' s, OpRac2.StatementStep p m b st st' s -> EquivAssignables p st st') /\ (forall m b st st' s, OpRac2.BlockStep p m b st st' s -> EquivAssignables p st st').
proof: Proof. generalize rac2_length_assignables_correct. intros. specialize H with p. destruct H. destruct H0. destruct H1. apply OpRac2.mutual_ind; intros; simpl in *. apply EquivAssignables_trans with st1; trivial. apply EquivAssignables_trans with st2; trivial. rewrite H14. apply FieldUpdateAction_Equiv; auto. rewrite H14. rewrite <- H13. simpl. unfold FieldUpdateAction. case isPivot. simpl. rewrite map_length. apply Nat.le_min_r. apply Nat.le_min_r. apply H in H5. rewrite H5. apply Nat.le_min_l. apply EquivAssignables_trans with st1; trivial. apply EquivAssignables_trans with st2; trivial. assert (EquivAssignables p st2 st_c). unfold NewFrame in H13. unfold MethodCallAction in H15. unfold EquivAssignables. rewrite H13 in H14. rewrite H14 in H15. simpl in H15. rewrite <- H15. simpl. unfold level. simpl. rewrite nat_compare_n_Sn. rewrite truncate_same. apply EquivAssignables_ind_refl. apply EquivAssignables_trans with st_c'; trivial. apply EquivAssignables_trans with st_c; trivial. apply H2 in H18. rewrite H18. apply Nat.le_min_r. rewrite <- H21. apply MethodReturnAction_Equiv with st2; auto. rewrite <- H21. unfold MethodReturnAction. simpl. unfold pop. case st_c' @fr @assignables. auto with *. intros. simpl. auto with *. apply H0 in H9. rewrite H9. apply Nat.le_min_l. apply H in H4. rewrite H4. apply Nat.le_min_l. apply EquivAssignables_trans with (st' := st1); trivial. apply NewObjectAction_Equiv with o; auto. rewrite H6. apply EquivAssignables_3 with (Heap.ObjectObject cn um) o. replace st1 @h with st @h ; trivial. rewrite <- H5. trivial. rewrite H6. simpl. apply Nat.le_min_r. rewrite H3. apply EquivAssignables_refl. apply EquivAssignables_trans with st1; trivial. apply H0 in H6. rewrite H6. apply Nat.le_min_r. trivial. apply EquivAssignables_trans with st1; trivial. apply EquivAssignables_trans with st1 [fr := fr2]; trivial. unfold EquivAssignables. rewrite H6. simpl. unfold level. rewrite nat_compare_n_n. apply EquivAssignables_ind_refl. rewrite H6. simpl. apply Nat.le_min_l. apply H1 in H4. rewrite H4. apply Nat.le_min_l. trivial. Qed.
imports: Coq(List)