proposition: Lemma CTXT_EVAL_equiv_true: CTXT_EVAL_pkg_tt ∘ EVAL false ≈₀ CTXT_EVAL_SAMP_pkg ∘ EVAL_SAMP false.
proof: Proof. apply eq_rel_perf_ind_ignore with (fset [:: R_loc]). 1: by rewrite -fset1E /CTXT_EVAL_SAMP_locs fsub1set !fset_cons !in_fsetU !in_fset1 eq_refl !Bool.orb_true_r. simplify_eq_rel m. all: simplify_linking. all: ssprove_code_simpl. all: rewrite cast_fun_K. all: ssprove_code_simpl. all: ssprove_code_simpl_more. all: apply: r_get_remember_rhs => R. - ssprove_sync=> r. ssprove_sync=> T. case: (getm T (mkciph m r)) => [c|]. + ssprove_sync=> S. ssprove_sync. shelve. + ssprove_code_simpl_more. rewrite domm_fset_to_chset. ssprove_sync=> H1. ssprove_sync=> c. ssprove_sync=> Tinv. ssprove_swap_seq_lhs [:: 1; 0]. ssprove_swap_seq_rhs [:: 1; 0]. ssprove_sync=> S. do 3 ssprove_sync. shelve. - ssprove_sync=> S. ssprove_sync=> H1. ssprove_sync=> Tinv. case: (getm Tinv m) => [c|]. + shelve. + ssprove_code_simpl_more. rewrite domm_fset_to_chset. ssprove_sync=> H2. ssprove_sync=> c. ssprove_sync=> T. do 2 ssprove_sync. shelve. Unshelve. all: apply: r_put_rhs. 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)