MatchingLogic.EntryIII.WitnessElim #
theorem
MatchingLogic.Pattern.AlphaEq.captureAvoidingSubst
{S : Signature}
{p q : Pattern S ℕ}
(h : p.AlphaEq q)
(x y : ℕ)
:
(Pattern.captureAvoidingSubst x y p).AlphaEq (Pattern.captureAvoidingSubst x y q)
Total capture-avoiding substitution respects proof-theoretic alpha equivalence.
theorem
MatchingLogic.Pattern.captureAvoidingSubst_comp_alphaEq
{S : Signature}
{x y z : ℕ}
{p : Pattern S ℕ}
(hy : y ∉ FV p)
:
(captureAvoidingSubst y z (captureAvoidingSubst x y p)).AlphaEq (captureAvoidingSubst x z p)
Source substitution composition modulo alpha equivalence. The intermediate name is fresh only from free variables; the final name is arbitrary.
theorem
MatchingLogic.IsMCS.exList_witness_elim
{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)
(hnested :
Pattern.exList (List.ofFn y)
(Pattern.app sigma fun (i : Fin (S.arity sigma)) =>
(Phi i).and ((Pattern.ex x p).imp (Pattern.captureAvoidingSubst x (y i) p))) ∈ Gamma)
:
Eliminate the nested witnesses produced by Lemma 80 and normalize every sequential raw substitution back to one source-style substitution.
theorem
MatchingLogic.IsMCS.witnessPush_elim
{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)
:
Stage-recursion interface: apply Lemma 80 and immediately eliminate its nested witnesses inside a witnessed MCS.