Documentation

LeanPool.NFWeakPartition.NominalOneFreeCompletenessBridgeDev003

NF weak partition development: NominalOneFreeCompletenessBridgeDev003.

source
@[reducible, inline]
abbrev NFChoice.DirectNominalPrf.Nominal.OneFreeCompletenessBridgeDev003.NFTheory :
Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as NFTheory.

Equations
Instances For
    source
    theorem NFChoice.DirectNominalPrf.Nominal.OneFreeCompletenessBridgeDev003.oneFreeLoweringAsSubst (x : SemanticCore.Var) (p : SemanticCore.Wff) (hfv : p.fv ⊆ {x}) (rho : SemanticCore.Var → ℕ) :
    lowerWff rho p = Fol.BoundedPreformula.fst (SemanticCore.Lowering.lowerWff (fun (x : SemanticCore.Var) => 0) p).toFlypitch [&(rho x) // 0]f
    source
    noncomputable def NFChoice.DirectNominalPrf.Nominal.OneFreeCompletenessBridgeDev003.oneFreeNPrfOfValidity (x : SemanticCore.Var) (p : SemanticCore.Wff) (hfv : p.fv ⊆ {x}) (hvalid : ∀ (S : Fol.Structure Foundation.LNF), Nonempty S.carrier → Fol.allRealizeSentence S NFTheory → SemanticCore.Wff.Valid S p) :
    NPrf p

    Proof-translation construction identified upstream as oneFreeNPrfOfValidity.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For