MatchingLogic.EntryIII.Alpha

theorem MatchingLogic.Pattern.substVar_eq_self_of_not_mem_allVars {S : Signature} {x y : ℕ} {p : Pattern S ℕ} (hx : x ∉ p.allVars) : substVar x y p = p

Substitution does nothing when its source name occurs neither free nor bound.

theorem MatchingLogic.Pattern.substVar_roundtrip {S : Signature} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : substVar y x (substVar x y p) = p

Replacing x by a wholly fresh y, then y by x, is literally the original raw pattern. No quotient by alpha equivalence is used.

theorem MatchingLogic.Pattern.captureFree_of_not_mem_allVars {S : Signature} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : CaptureFree x y p

A name absent from all raw occurrences is capture-free as a replacement.

theorem MatchingLogic.Pattern.captureFree_reverse_substVar {S : Signature} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : CaptureFree y x (substVar x y p)

The reverse leg of a fresh substitution is itself capture-free.

theorem MatchingLogic.Pattern.substVar_source_not_mem_FV {S : Signature} {x y : ℕ} (p : Pattern S ℕ) (hxy : x ≠ y) : x ∉ FV (substVar x y p)

If source and replacement differ, no free source occurrence remains after variable-for-variable substitution.

theorem MatchingLogic.Provable.alphaEx_forward {S : Signature} {Gamma : Set (Pattern S ℕ)} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : Provable Gamma ((Pattern.ex x p).imp (Pattern.ex y (substVar x y p)))

Derived forward alpha conversion for an existential binder.

theorem MatchingLogic.Provable.alphaEx_backward {S : Signature} {Gamma : Set (Pattern S ℕ)} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : Provable Gamma ((Pattern.ex y (substVar x y p)).imp (Pattern.ex x p))

Derived backward alpha conversion for an existential binder.