NF weak partition development: NominalDfClabProperSubstitutionCoreDev003.

@[reducible, inline]

abbrev NFChoice.DirectNominalPrf.Nominal.DfClabProperSubstitutionCoreDev003.Theory : Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as Theory.

Equations

• NFChoice.DirectNominalPrf.Nominal.DfClabProperSubstitutionCoreDev003.Theory = NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF

def NFChoice.DirectNominalPrf.Nominal.DfClabProperSubstitutionCoreDev003.properSubstRhs (F : Fol.formula Foundation.LNF) (replacement original : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as properSubstRhs.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.DfClabProperSubstitutionCoreDev003.coincidentSubstRhs (F : Fol.formula Foundation.LNF) (source : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as coincidentSubstRhs.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.DfClabProperSubstitutionCoreDev003.properSubstCore (F : Fol.formula Foundation.LNF) (replacement original : Fol.term Foundation.LNF) : Fol.prf Theory.fst (Fol.biimp (F [replacement // 0]f) (properSubstRhs F replacement original))

Pure Flypitch proof of unrestricted proper substitution.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.DfClabProperSubstitutionCoreDev003.coincidentSubstCore (F : Fol.formula Foundation.LNF) (sourceTerm : Fol.term Foundation.LNF) : Fol.prf Theory.fst (Fol.biimp (F [sourceTerm // 0]f) (coincidentSubstRhs F sourceTerm))

Pure Flypitch proof for the captured/coincident source-name branch.

Equations

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