proposition: Theorem rac2_rac3_correct: forall p, (forall e st_rac2 st'_rac2 r, OpRac2.ExpressionStep p e st_rac2 st'_rac2 r -> forall st_rac3, CorrespondingState p st_rac2 st_rac3 -> exists st'_rac3, CorrespondingState p st'_rac2 st'_rac3 /\ OpRac3.ExpressionStep p e st_rac3 st'_rac3 r) /\ (forall l st_rac2 st'_rac2 r, OpRac2.ListSteps p l st_rac2 st'_rac2 r -> forall st_rac3, CorrespondingState p st_rac2 st_rac3 -> exists st'_rac3, CorrespondingState p st'_rac2 st'_rac3 /\ OpRac3.ListSteps p l st_rac3 st'_rac3 r) /\ (forall m b st_rac2 st'_rac2 r, OpRac2.StatementStep p m b st_rac2 st'_rac2 r -> forall st_rac3, CorrespondingState p st_rac2 st_rac3 -> exists st'_rac3, CorrespondingState p st'_rac2 st'_rac3 /\ OpRac3.StatementStep p m b st_rac3 st'_rac3 r) /\ (forall m b st_rac2 st'_rac2 r, OpRac2.BlockStep p m b st_rac2 st'_rac2 r -> forall st_rac3, CorrespondingState p st_rac2 st_rac3-> exists st'_rac3, CorrespondingState p st'_rac2 st'_rac3 /\ OpRac3.BlockStep p m b st_rac3 st'_rac3 r).
proof: Proof. intro p. apply OpRac2.mutual_ind; intros; simpl in *. apply H2 in H11. destruct H11 as[st1_rac3 H11]. destruct H11. destruct H5 with st1_rac3 as [st2_rac3 H13];trivial. destruct H13. set (st3_rac3 := Rac3.Assignables.FieldUpdateAction p loc v st2_rac3). exists ((st3_rac3[h := Heap.update st2_rac3@h loc v])%rac3). split. rewrite H10. destruct H13. apply FieldUpdateAction_Correct with cn um obj fsig;trivial. rewrite <- H15;trivial. rewrite <- H15;trivial. split;trivial. inversion H13. apply (OpRac3.assignment_instance_field_ok p e v obj fsig expr target st_rac3 st1_rac3 st2_rac3 st3_rac3[h := Heap.update st2_rac3@h loc v]%rac3 st3_rac3 loc cn um); trivial. apply (FieldUpdateCheck_Correct loc p st1 st1_rac3); trivial. rewrite <- H16;trivial. rewrite <- H16;trivial. destruct H1 with st_rac3 as (st1_rac3, Htmp); trivial. destruct Htmp. clear H1. destruct H6 with st1_rac3 as (st2_rac3, Htmp); trivial. destruct Htmp. clear H6. set (fr_c1_rac3 := Rac3.NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac3) in |- *. set (st3_rac3 := st2_rac3[fr := fr_c1_rac3]%rac3) in |- *. set (st_c_rac3 := Rac3.Assignables.MethodCallAction p c' m' st3_rac3) in |- *. destruct H15 with st_c_rac3 as (st_c'_rac3, Htmp). assert (CorrespondingState p st3 st3_rac3). unfold st3_rac3 in |- *. rewrite H10 in |- *. apply NewFrame_Correct with (m := m') (param := lv2params m' (Ref this0 :: psv)) (st_rac2 := st2) (st_rac3 := st2_rac3); trivial. unfold st_c_rac3 in |- *. rewrite <- H11. apply MethodCallAction_Correct with (c := c') (m := m') (st_rac2 := st3) (st_rac3 := st3_rac3); trivial. destruct Htmp. set (st'_rac3 := Rac3.Assignables.MethodReturnAction p st_c'_rac3 st2_rac3) in |- *. exists st'_rac3. split. unfold st'_rac3 in |- *. rewrite <- H17 in |- *. apply MethodReturnAction_Correct with st2 st_c' st2_rac3 st_c'_rac3; trivial. apply (OpRac3.method_vcall_ok p e st_rac3 st1_rac3 st2_rac3 st3_rac3 st_c_rac3 st_c'_rac3 st'_rac3 fr_c1_rac3 msig o cn um this0 ps psnv psv v cn' m' c' b body); trivial. inversion H19. rewrite <- H24;trivial. inversion H6. inversion H23. rewrite <- H31. trivial. set (st1_rac3 := Rac3.Assignables.NewObjectAction p o st_rac3) in |- *. exists st1_rac3[h := h']%rac3. split. rewrite H2 in |- *. assert (CorrespondingState p st1 st1_rac3). unfold st1_rac3 in |- *. rewrite <- H1 in |- *. apply NewObjectAction_Correct with o st st_rac3; trivial. replace st@h with st1@h in H0. destruct H4. split;simpl;trivial. rewrite <- CorrectBacklinks_new with cn um o;trivial. rewrite <- H5;trivial. destruct H1. unfold Rac2.Assignables.NewObjectAction. simpl. trivial. apply OpRac3.new_object_ok with (st1 := st1_rac3) (h' := h') (cn := cn) (um := um); trivial. destruct H3. rewrite <- H4; trivial. exists st_rac3. rewrite <- H in |- *. split; trivial. apply OpRac3.ListSteps_nil; trivial. destruct H1 with st_rac3 as (st1_rac3, Htmp); trivial. destruct Htmp. destruct H3 with st1_rac3 as (st'_rac3, Htmp); trivial. destruct Htmp. exists st'_rac3. split; trivial. apply OpRac3.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_rac3); trivial. destruct H1 with st_rac3 as (st'_rac3, Htmp); trivial. destruct Htmp. exists st'_rac3. split; trivial. apply OpRac3.expr_stmt_ok with (v := v) (e := e); trivial. destruct H2. destruct H2. rewrite <- H8 in |- *; trivial. destruct H1 with st_rac3 as (st1_rac3, Htmp); trivial. destruct Htmp. set (fr2_rac3 := Rac3.State.Frame.set_pc st1_rac3@fr%rac3 pc') in |- *. destruct H4 with st1_rac3[fr := fr2_rac3]%rac3 as (st'_rac3, Htmp); trivial. destruct H6. rewrite H2 in |- *. unfold fr2_rac3 in |- *. split; trivial. inversion H6. split;simpl;trivial. destruct Htmp. exists st'_rac3. split; trivial. apply OpRac3.BlockStep_ok_next with (pc' := pc') (st1 := st1_rac3) (fr2 := fr2_rac3); trivial. destruct H5. destruct H5. rewrite <- H13 in |- *. trivial. destruct H1 with st_rac3 as (st'_rac3, Htmp); trivial. destruct Htmp. exists st'_rac3. split; trivial. apply OpRac3.BlockStep_ok_last; trivial. destruct H2. destruct H2. rewrite <- H8 in |- *; trivial. Qed.