MatchingLogic.Soundness

theorem MatchingLogic.Pattern.substVar_eq_self_of_not_mem_FV {S : Signature} {Var : Type} [DecidableEq Var] {x y : Var} {φ : Pattern S Var} (hx : x ∉ FV φ) : substVar x y φ = φ

Raw variable substitution is inert when its source variable is not free.

theorem MatchingLogic.Model.denote_substVar_of_captureFree {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) {x y : Var} {φ : Pattern S Var} (hcf : CaptureFree x y φ) : M.denote ρ (substVar x y φ) = M.denote (Function.update ρ x (ρ y)) φ

Semantic substitution for the capture-free variable-for-variable substitution used by rule (3).

theorem MatchingLogic.soundness {S : Signature} {Var : Type} [DecidableEq Var] : Soundness S Var

(S) is provable, not merely assumable. The paper cites soundness to its reference [3]; every rule of Figure 2 is sound for global consequence, so it can be discharged here. Doing so removes one of the two black boxes from Corollary 15.