proposition: Theorem pup_to_2_ceval : (X !-> 2) =[ pup_to_n ]=> (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; Y !-> 0 ; X !-> 2).
proof: Proof. Admitted. Theorem ceval_deterministic: forall c st st1 st2, st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2. Proof. intros c st st1 st2 E1 E2. generalize dependent st2. induction E1; intros st2 E2; inversion E2; subst. - reflexivity. - reflexivity. - rewrite (IHE1_1 st'0 H1) in *. apply IHE1_2. assumption. - apply IHE1. assumption. - rewrite H in H5. discriminate. - rewrite H in H5. discriminate. - apply IHE1. assumption. - reflexivity. - rewrite H in H2. discriminate. - rewrite H in H4. discriminate. - rewrite (IHE1_1 st'0 H3) in *. apply IHE1_2. assumption. Qed.
imports: Coq(Bool.Bool) Coq(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)