MatchingLogic.EntryIII.FreshWitnessElim

theorem MatchingLogic.Pattern.captureAvoidingSubst_comp_eq_of_fresh_result {S : Signature} {x y z : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) (hz : z ∉ p.allVars) (hzs : z ∉ (substVar x y p).allVars) : captureAvoidingSubst y z (captureAvoidingSubst x y p) = captureAvoidingSubst x z p

Exact composition when the result name is fresh for the current body. The z = y case is an inert self-substitution; otherwise support tracking shows that the second capture-avoidance pass is a raw substitution.

theorem MatchingLogic.IsMCS.freshWitness_elim {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) (hW : FreshWitnessed Gamma) {y : ℕ} {q : Pattern S ℕ} (hmem : Pattern.ex y q ∈ Gamma) : ∃ z ∉ q.allVars, Pattern.captureAvoidingSubst y z q ∈ Gamma

One fresh witness may be eliminated inside an MCS while retaining the strong raw freshness fact needed by subsequent substitutions.

def MatchingLogic.Pattern.substList {S : Signature} : List ℕ → List ℕ → Pattern S ℕ → Pattern S ℕ

The body obtained by successively eliminating an ordered list of names.

Equations

• MatchingLogic.Pattern.substList (y :: ys) (z :: zs) x✝ = MatchingLogic.Pattern.substList ys zs (MatchingLogic.substVar y z x✝)
• MatchingLogic.Pattern.substList x✝² x✝¹ x✝ = x✝

def MatchingLogic.Pattern.FreshExListTrace {S : Signature} : List ℕ → List ℕ → Pattern S ℕ → Prop

The stronger freshness record carried through a nested witness elimination. Each returned name is fresh for the exact remaining body.

Equations

• MatchingLogic.Pattern.FreshExListTrace [] [] x✝ = True
• MatchingLogic.Pattern.FreshExListTrace (y :: ys) (z :: zs) x✝ = (z ∉ (MatchingLogic.Pattern.exList ys x✝).allVars ∧ MatchingLogic.Pattern.FreshExListTrace ys zs (MatchingLogic.substVar y z x✝))
• MatchingLogic.Pattern.FreshExListTrace x✝² x✝¹ x✝ = False

theorem MatchingLogic.IsMCS.exList_freshWitness_elim {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) (hW : FreshWitnessed Gamma) (ys : List ℕ) (hys : ys.Nodup) (p : Pattern S ℕ) (hmem : Pattern.exList ys p ∈ Gamma) : ∃ (zs : List ℕ), Pattern.FreshExListTrace ys zs p ∧ Pattern.substList ys zs p ∈ Gamma

Recursively eliminate an exList in a fresh-witness MCS. The result is an actual raw substitution trace, not an appeal to alpha quotienting.

theorem MatchingLogic.IsMCS.witnessPush_freshTrace {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) (hW : FreshWitnessed Gamma) {sigma : S.Sym} (Phi : Fin (S.arity sigma) → Pattern S ℕ) (p : Pattern S ℕ) (x : ℕ) (y : Fin (S.arity sigma) → ℕ) (hyinj : Function.Injective y) (hyfreshP : ∀ (i : Fin (S.arity sigma)), y i ∉ p.allVars) (hyfreshPhi : ∀ (i j : Fin (S.arity sigma)), y i ∉ (Phi j).allVars) (happ : Pattern.app sigma Phi ∈ Gamma) : ∃ (z : List ℕ), Pattern.FreshExListTrace (List.ofFn y) z (Pattern.app sigma fun (i : Fin (S.arity sigma)) => (Phi i).and ((Pattern.ex x p).imp (Pattern.captureAvoidingSubst x (y i) p))) ∧ Pattern.substList (List.ofFn y) z (Pattern.app sigma fun (i : Fin (S.arity sigma)) => (Phi i).and ((Pattern.ex x p).imp (Pattern.captureAvoidingSubst x (y i) p))) ∈ Gamma

Apply Lemma 80 and eliminate its nested existential witnesses using the fresh strengthened interface. FreshExListTrace records exactly the all-variable freshness available at every recursive step, so consumers do not need to guess a raw-syntax normalization convention.