NF weak partition development: NominalRecanonTransportDev.

@[reducible, inline]

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

Proof-translation construction identified upstream as Theory.

Equations

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

The existing semantic certificate relation lives in Prop. Flypitch proof objects live in Type, so Lean correctly forbids eliminating that relation to construct a proof object. This byte-for-byte structural counterpart lives in Type; the source emitter produces it directly.

inductive NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.TRecanonClass : SemanticCore.Class → SemanticCore.Class → Type

Proof-translation construction identified upstream as TRecanonClass.

• same (A : SemanticCore.Class) : TRecanonClass A A
• cab {x : SemanticCore.Var} {p q : SemanticCore.Wff} (h : TRecanonWff p q) : TRecanonClass (SemanticCore.Class.cab x p) (SemanticCore.Class.cab x q)

inductive NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.TRecanonWff : SemanticCore.Wff → SemanticCore.Wff → Type

Proof-translation construction identified upstream as TRecanonWff.

• same (p : SemanticCore.Wff) : TRecanonWff p p
• imp {p p' q q' : SemanticCore.Wff} (hp : TRecanonWff p p') (hq : TRecanonWff q q') : TRecanonWff (p.imp q) (p'.imp q')
• all {x : SemanticCore.Var} {p q : SemanticCore.Wff} (h : TRecanonWff p q) : TRecanonWff (SemanticCore.Wff.all x p) (SemanticCore.Wff.all x q)
• objEq_classEq (x y : SemanticCore.Var) : TRecanonWff (SemanticCore.Wff.objEq x y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))
• classEq_objEq (x y : SemanticCore.Var) : TRecanonWff (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.objEq x y)
• objMem_classMem (x y : SemanticCore.Var) : TRecanonWff (SemanticCore.Wff.objMem x y) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))
• classMem_objMem (x y : SemanticCore.Var) : TRecanonWff (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.objMem x y)
• classEq {A A' B B' : SemanticCore.Class} (hA : TRecanonClass A A') (hB : TRecanonClass B B') : TRecanonWff (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq A' B')
• classMem {A A' B B' : SemanticCore.Class} (hA : TRecanonClass A A') (hB : TRecanonClass B B') : TRecanonWff (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A' B')

noncomputable def NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.liftedTheoryBiimp {p q : Fol.formula Foundation.LNF} (h : Fol.prf Theory.fst (Fol.biimp p q)) : Fol.prf (Fol.liftFormula1 '' Theory.fst) (Fol.biimp p q)

Proof-translation construction identified upstream as liftedTheoryBiimp.

Equations

• NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.liftedTheoryBiimp h = ⋯.mpr h

noncomputable def NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.impCongr {L : Fol.Language} {Γ : Set (Fol.formula L)} {p p' q q' : Fol.formula L} (hp : Fol.prf Γ (Fol.biimp p p')) (hq : Fol.prf Γ (Fol.biimp q q')) : Fol.prf Γ (Fol.biimp (Fol.preformula.imp p q) (Fol.preformula.imp p' q'))

Proof-translation construction identified upstream as impCongr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.andCongr {L : Fol.Language} {Γ : Set (Fol.formula L)} {p p' q q' : Fol.formula L} (hp : Fol.prf Γ (Fol.biimp p p')) (hq : Fol.prf Γ (Fol.biimp q q')) : Fol.prf Γ (Fol.biimp (Fol.and' p q) (Fol.and' p' q'))

Proof-translation construction identified upstream as andCongr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.classBridge {A B : SemanticCore.Class} : TRecanonClass A B → (rho : SemanticCore.Var → ℕ) → (candidate : ℕ) → Fol.prf Theory.fst (Fol.biimp (lowerClassPred rho candidate A) (lowerClassPred rho candidate B))

Proof-translation construction identified upstream as classBridge.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.wffBridge {p q : SemanticCore.Wff} : TRecanonWff p q → (rho : SemanticCore.Var → ℕ) → Fol.prf Theory.fst (Fol.biimp (lowerWff rho p) (lowerWff rho q))

Proof-translation construction identified upstream as wffBridge.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.transport {p q : SemanticCore.Wff} (h : TRecanonWff p q) (hp : NPrf p) : NPrf q

Proof-translation construction identified upstream as transport.

Equations

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