proposition: Theorem nestedRandomFunc_spec : forall st s1 s2 (d : D), (nestedRandomFunc_pred st s1 s2) -> comp_spec (fun p1 p2 => fst p1 = fst p2 /\ (nestedRandomFunc_pred st (snd p1) (snd p2))) (randomFunc RndR _ s1 d) (nestedRandomFunc st s2 d).
proof: Proof. unfold nestedRandomFunc_pred in *; intros. unfold nestedRandomFunc. case_eq (arrayLookup _ st d); intros. unfold randomFunc. rewrite H. erewrite arrayLookup_app_Some; eauto. eapply comp_spec_ret; intuition idtac. simpl in *. rewrite H. case_eq (eqb d0 d); intros. rewrite eqb_leibniz in H1. subst. repeat erewrite (arrayLookup_app_Some); eauto. case_eq (arrayLookup _ st d0); intros. repeat erewrite (arrayLookup_app_Some); eauto. repeat rewrite (arrayLookup_app_None); eauto. simpl. rewrite H1. trivial. unfold randomFunc. rewrite H. rewrite arrayLookup_app_None. case_eq (arrayLookup _ s2 d); intros. eapply comp_spec_ret; intuition idtac. fcf_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. eapply comp_spec_ret; intuition idtac. simpl. rewrite H. case_eq (eqb d0 d); intros. rewrite eqb_leibniz in H4. subst. rewrite arrayLookup_app_None; eauto. simpl. rewrite eqb_refl. trivial. case_eq (arrayLookup _ st d0); intros. repeat erewrite (arrayLookup_app_Some); eauto. repeat rewrite arrayLookup_app_None; eauto. simpl. rewrite H4. trivial. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid