proposition: Lemma SemiInvariant_triple_rhs : ∀ L₀ L₁ ℓ₁ ℓ₂ ℓ₃ (R : _ → _ → _ → Prop), ℓ₁ \in L₀ :|: L₁ → ℓ₂ \in L₀ :|: L₁ → ℓ₃ \in L₀ :|: L₁ → R (get_heap empty_heap ℓ₁) (get_heap empty_heap ℓ₂) (get_heap empty_heap ℓ₃) → SemiInvariant L₀ L₁ (triple_rhs ℓ₁ ℓ₂ ℓ₃ R).
proof: Proof. intros L₀ L₁ ℓ₁ ℓ₂ ℓ₃ R h₁ h₂ h₃ he. split. - intros s₀ s₁ ℓ v hℓ₀ hℓ₁ ?. assert (hℓ : ℓ \notin L₀ :|: L₁). { rewrite in_fsetU. rewrite (negbTE hℓ₀) (negbTE hℓ₁). reflexivity. } unfold triple_rhs. rewrite !get_set_heap_neq. + auto. + apply /negP => /eqP e. subst. rewrite h₃ in hℓ. discriminate. + apply /negP => /eqP e. subst. rewrite h₂ in hℓ. discriminate. + apply /negP => /eqP e. subst. rewrite h₁ in hℓ. discriminate. - simpl. auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)