proposition: Lemma TAG_EVAL_equiv_true: TAG_EVAL_pkg_tt ∘ EVAL false ≈₀ TAG_GUESS_pkg ∘ GUESS true.
proof: Proof. apply eq_rel_perf_ind_ignore with (fset [:: S_loc]). 1: { apply: fsubset_trans. - by apply fsubsetUl. - by apply fsubsetUr. } simplify_eq_rel m. 2: case: m => [m t]. all: simplify_linking. all: simplify_linking. all: ssprove_code_simpl. all: ssprove_code_simpl_more. 2: { apply: (@r_reflexivity_alt _ (fset1 T_loc)). all: by ssprove_invariant. } 1: apply: r_get_remember_rhs => S. ssprove_sync=> T. case (getm T _) => [t|]. 2: ssprove_sync=> t. 2: ssprove_sync. 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)