proposition: Lemma CTXT_HYB_equiv_2: CTXT_HYB_pkg_1 ∘ SAMP Key_N true ≈₀ CTXT_HYB_pkg_2.
proof: Proof. apply eq_rel_perf_ind_ignore with (R_loc |: fset1 Tinv'_loc). 1: by rewrite fsubU1set /CTXT_HYB_locs_1 /CTXT_HYB_locs_2 fsub1set !fset_cons !in_fsetU !in_fset1 !eq_refl !Bool.orb_true_r. simplify_eq_rel m. all: ssprove_code_simpl. all: ssprove_code_simpl_more. all: apply: r_get_remember_lhs => R. - ssprove_sync=> r. ssprove_sync=> [|T]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. ssprove_sync=> c. ssprove_sync=> [|Tinv]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. ssprove_sync=> [|S]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. do 3 ssprove_sync. shelve. - ssprove_sync=> [|S]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. ssprove_sync=> H1. ssprove_sync=> [|Tinv]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. apply: r_get_remember_rhs => Tinv'. case: (getm Tinv m) => [c|]. 1: shelve. ssprove_sync=> c. ssprove_sync=> [|T]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. do 2 ssprove_sync. apply: r_put_rhs. shelve. Unshelve. all: apply: r_put_lhs. all: ssprove_restore_mem; last by apply: r_ret. all: by ssprove_invariant. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)