proposition: Lemma CTXT_HYB_equiv_5: CTXT_HYB_pkg_4 ≈₀ CTXT_HYB_pkg_5.
proof: Proof. apply eq_rel_perf_ind with ( (fun '(h0, h1) => h0 = h1) ⋊ couple_rhs Tinv_loc Tinv'_loc eq ). 1: { ssprove_invariant=> //. all: by rewrite /CTXT_HYB_locs_2 !fset_cons !in_fsetU !in_fset1 eq_refl !Bool.orb_true_r. } simplify_eq_rel m. - apply: (@r_reflexivity_alt _ (S_loc |: fset1 R_loc)) => [loc H|loc v H]. all: ssprove_invariant; first by move=> ? ? ->. all: rewrite in_fsetU !in_fset1 in H. all: apply /eqP. all: by move: H => /orP [/eqP|/eqP] ->. - ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync=> [|S]; first by move=> ? ? ->. ssprove_sync=> H1. apply: r_get_vs_get_remember => Tinv. apply: r_get_vs_get_remember => Tinv'. apply: (r_rem_couple_rhs Tinv_loc Tinv'_loc) => ->. case: (getm Tinv' m) => [c|]. + ssprove_forget_all. by apply: r_ret. + ssprove_sync=> c. ssprove_sync=> [|T]; first by move=> ? ? ->. ssprove_sync; first by move=> ? ? ->. do 2 apply: r_put_vs_put. ssprove_restore_mem; last by apply: r_ret. 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)