proposition: Lemma CTXT_HYB_equiv_4: CTXT_HYB_pkg_3 ≈₀ CTXT_HYB_pkg_4.
proof: Proof. apply eq_rel_perf_ind_ignore with (T_loc |: fset1 Tinv_loc). 1: by rewrite fsubU1set /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. - ssprove_sync=> r. apply: r_get_remember_lhs => T. ssprove_sync=> c. apply: r_get_remember_lhs => Tinv. ssprove_sync=> [|S]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. do 2 apply: r_put_lhs. shelve. - ssprove_sync=> [|S]; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. ssprove_sync=> H1. apply: r_get_remember_lhs => Tinv_l. apply: r_get_remember_rhs => Tinv_r. ssprove_sync=> [|Tinv']; first by rewrite in_fsetU !in_fset1; apply /norP; split; apply /eqP. case: (getm Tinv' m) => [c|]. + ssprove_forget_all. by apply: r_ret. + ssprove_sync=> c. apply: r_get_remember_lhs => Tl. apply: r_get_remember_rhs => Tr. apply: r_put_lhs. apply: r_put_rhs. apply: r_put_vs_put. shelve. Unshelve. all: ssprove_restore_mem; first by ssprove_invariant. all: ssprove_sync. all: by apply: r_ret. 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)