proposition: Theorem pup_to_2_ceval : pup_to_n / (t_update empty_state X 2) \\ t_update (t_update (t_update (t_update (t_update (t_update empty_state X 2) Y 0) Y 2) X 1) Y 3) X 0.
proof: Proof. Admitted. Theorem ceval_deterministic: forall c st st1 st2, c / st \\ st1 -> c / st \\ st2 -> st1 = st2. Proof. intros c st st1 st2 E1 E2. generalize dependent st2. induction E1; intros st2 E2; inversion E2; subst. - reflexivity. - reflexivity. - assert (st' = st'0) as EQ1. { apply IHE1_1; assumption. } subst st'0. apply IHE1_2. assumption. - apply IHE1. assumption. - rewrite H in H5. inversion H5. - rewrite H in H5. inversion H5. - apply IHE1. assumption. - reflexivity. - rewrite H in H2. inversion H2. - rewrite H in H4. inversion H4. - assert (st' = st'0) as EQ1. { apply IHE1_1; assumption. } subst st'0. apply IHE1_2. assumption. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps