NF weak partition development: NominalCertificate.

A direct Flypitch executor for named-variable Metamath certificates. Proofs are polymorphic in the assignment of source names to free de Bruijn indices. Consequently ax-gen can bind one source name without choosing a global variable numbering or copying a proof term.

The exact repaired-source trace sidecar has SHA-256 89E80799B18269313FED986238AAEEEB1BE0DBAD2D7F28C3469521701A837E80.

def NFChoice.DirectCertificate.Nominal.sourceMmSha256 : String

Proof-translation construction identified upstream as sourceMmSha256.

Equations

• NFChoice.DirectCertificate.Nominal.sourceMmSha256 = "868DF831E63E28AA924CC099510CD9E5D3BE18CD8416A20B335F5BBF3B42ED3F"

def NFChoice.DirectCertificate.Nominal.exactSliceSha256 : String

Proof-translation construction identified upstream as exactSliceSha256.

Equations

• NFChoice.DirectCertificate.Nominal.exactSliceSha256 = "89E80799B18269313FED986238AAEEEB1BE0DBAD2D7F28C3469521701A837E80"

inductive NFChoice.DirectCertificate.Nominal.Code (Var Atom : Type) : Type

A small nominal source AST sufficient for the exact quantified slice.

• atom {Var Atom : Type} : Atom → Code Var Atom
• falsum {Var Atom : Type} : Code Var Atom
• equal {Var Atom : Type} : Var → Var → Code Var Atom
• imp {Var Atom : Type} : Code Var Atom → Code Var Atom → Code Var Atom
• all {Var Atom : Type} : Var → Code Var Atom → Code Var Atom

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instDecidableEqCode {Var✝ Atom✝ : Type} [DecidableEq Var✝] [DecidableEq Atom✝] : DecidableEq (Code Var✝ Atom✝)

Equations

• NFChoice.DirectCertificate.Nominal.instDecidableEqCode = NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq

def NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq {Var✝ Atom✝ : Type} [DecidableEq Var✝] [DecidableEq Atom✝] (x✝ x✝¹ : Code Var✝ Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.atom a) NFChoice.DirectCertificate.Nominal.Code.falsum = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.atom a) (NFChoice.DirectCertificate.Nominal.Code.equal a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.atom a) (a_1.imp a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.atom a) (NFChoice.DirectCertificate.Nominal.Code.all a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq NFChoice.DirectCertificate.Nominal.Code.falsum (NFChoice.DirectCertificate.Nominal.Code.atom a) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq NFChoice.DirectCertificate.Nominal.Code.falsum NFChoice.DirectCertificate.Nominal.Code.falsum = isTrue ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq NFChoice.DirectCertificate.Nominal.Code.falsum (NFChoice.DirectCertificate.Nominal.Code.equal a a_1) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq NFChoice.DirectCertificate.Nominal.Code.falsum (a.imp a_1) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq NFChoice.DirectCertificate.Nominal.Code.falsum (NFChoice.DirectCertificate.Nominal.Code.all a a_1) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.equal a a_1) (NFChoice.DirectCertificate.Nominal.Code.atom a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.equal a a_1) NFChoice.DirectCertificate.Nominal.Code.falsum = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.equal a a_1) (a_2.imp a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.equal a a_1) (NFChoice.DirectCertificate.Nominal.Code.all a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (a.imp a_1) (NFChoice.DirectCertificate.Nominal.Code.atom a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (a.imp a_1) NFChoice.DirectCertificate.Nominal.Code.falsum = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (a.imp a_1) (NFChoice.DirectCertificate.Nominal.Code.equal a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (a.imp a_1) (NFChoice.DirectCertificate.Nominal.Code.all a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.all a a_1) (NFChoice.DirectCertificate.Nominal.Code.atom a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.all a a_1) NFChoice.DirectCertificate.Nominal.Code.falsum = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.all a a_1) (NFChoice.DirectCertificate.Nominal.Code.equal a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqCode.decEq (NFChoice.DirectCertificate.Nominal.Code.all a a_1) (a_2.imp a_3) = isFalse ⋯

def NFChoice.DirectCertificate.Nominal.instReprCode.repr {Var✝ Atom✝ : Type} [Repr Var✝] [Repr Atom✝] : Code Var✝ Atom✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instReprCode {Var✝ Atom✝ : Type} [Repr Var✝] [Repr Atom✝] : Repr (Code Var✝ Atom✝)

Equations

• NFChoice.DirectCertificate.Nominal.instReprCode = { reprPrec := NFChoice.DirectCertificate.Nominal.instReprCode.repr }

def NFChoice.DirectCertificate.Nominal.bindRho {Var : Type} [DecidableEq Var] (rho : Var → ℕ) (bound : Var) : Var → ℕ

Assignment used below a binder: the bound name becomes index zero.

Equations

• NFChoice.DirectCertificate.Nominal.bindRho rho bound name = if name = bound then 0 else rho name + 1

def NFChoice.DirectCertificate.Nominal.Code.lower {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] (atomFormula : (Var → ℕ) → Atom → Fol.formula L) : (Var → ℕ) → Code Var Atom → Fol.formula L

Compile named source syntax to Flypitch's de Bruijn formula syntax.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectCertificate.Nominal.Code.lower atomFormula x✝ (NFChoice.DirectCertificate.Nominal.Code.atom a) = atomFormula x✝ a
• NFChoice.DirectCertificate.Nominal.Code.lower atomFormula x✝ NFChoice.DirectCertificate.Nominal.Code.falsum = ⊥'
• NFChoice.DirectCertificate.Nominal.Code.lower atomFormula x✝ (NFChoice.DirectCertificate.Nominal.Code.equal x_2 y) = NFChoice.Fol.preformula.equal &(x✝ x_2) &(x✝ y)

def NFChoice.DirectCertificate.Nominal.NPrf {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] (theory : Fol.SentTheory L) (atomFormula : (Var → ℕ) → Atom → Fol.formula L) (code : Code Var Atom) : Type

A proof-valued nominal judgment over a closed sentence theory.

Equations

• NFChoice.DirectCertificate.Nominal.NPrf theory atomFormula code = ((rho : Var → ℕ) → NFChoice.Fol.prf theory.fst (NFChoice.DirectCertificate.Nominal.Code.lower atomFormula rho code))

@[reducible, inline]

abbrev NFChoice.DirectCertificate.Nominal.Packed {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] (theory : Fol.SentTheory L) (atomFormula : (Var → ℕ) → Atom → Fol.formula L) : Type

One shared, dependently typed proof-table entry.

Equations

• NFChoice.DirectCertificate.Nominal.Packed theory atomFormula = ((code : NFChoice.DirectCertificate.Nominal.Code Var Atom) × NFChoice.DirectCertificate.Nominal.NPrf theory atomFormula code)

inductive NFChoice.DirectCertificate.Nominal.Step (Var Atom : Type) : Type

Proof-translation construction identified upstream as Step.

• input {Var Atom : Type} : ℕ → Step Var Atom
• ref {Var Atom : Type} : Var → Step Var Atom
• ax1 {Var Atom : Type} : Code Var Atom → Code Var Atom → Step Var Atom
• mp {Var Atom : Type} : ℕ → ℕ → Step Var Atom
• gen {Var Atom : Type} : Var → ℕ → Step Var Atom

def NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq {Var✝ Atom✝ : Type} [DecidableEq Var✝] [DecidableEq Atom✝] (x✝ x✝¹ : Step Var✝ Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.input a) (NFChoice.DirectCertificate.Nominal.Step.ref a_1) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.input a) (NFChoice.DirectCertificate.Nominal.Step.ax1 a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.input a) (NFChoice.DirectCertificate.Nominal.Step.mp a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.input a) (NFChoice.DirectCertificate.Nominal.Step.gen a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ref a) (NFChoice.DirectCertificate.Nominal.Step.input a_1) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ref a) (NFChoice.DirectCertificate.Nominal.Step.ax1 a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ref a) (NFChoice.DirectCertificate.Nominal.Step.mp a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ref a) (NFChoice.DirectCertificate.Nominal.Step.gen a_1 a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ax1 a a_1) (NFChoice.DirectCertificate.Nominal.Step.input a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ax1 a a_1) (NFChoice.DirectCertificate.Nominal.Step.ref a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ax1 a a_1) (NFChoice.DirectCertificate.Nominal.Step.mp a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.ax1 a a_1) (NFChoice.DirectCertificate.Nominal.Step.gen a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.mp a a_1) (NFChoice.DirectCertificate.Nominal.Step.input a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.mp a a_1) (NFChoice.DirectCertificate.Nominal.Step.ref a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.mp a a_1) (NFChoice.DirectCertificate.Nominal.Step.ax1 a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.mp a a_1) (NFChoice.DirectCertificate.Nominal.Step.gen a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.gen a a_1) (NFChoice.DirectCertificate.Nominal.Step.input a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.gen a a_1) (NFChoice.DirectCertificate.Nominal.Step.ref a_2) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.gen a a_1) (NFChoice.DirectCertificate.Nominal.Step.ax1 a_2 a_3) = isFalse ⋯
• NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq (NFChoice.DirectCertificate.Nominal.Step.gen a a_1) (NFChoice.DirectCertificate.Nominal.Step.mp a_2 a_3) = isFalse ⋯

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instDecidableEqStep {Var✝ Atom✝ : Type} [DecidableEq Var✝] [DecidableEq Atom✝] : DecidableEq (Step Var✝ Atom✝)

Equations

• NFChoice.DirectCertificate.Nominal.instDecidableEqStep = NFChoice.DirectCertificate.Nominal.instDecidableEqStep.decEq

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instReprStep {Var✝ Atom✝ : Type} [Repr Var✝] [Repr Atom✝] : Repr (Step Var✝ Atom✝)

Equations

• NFChoice.DirectCertificate.Nominal.instReprStep = { reprPrec := NFChoice.DirectCertificate.Nominal.instReprStep.repr }

def NFChoice.DirectCertificate.Nominal.instReprStep.repr {Var✝ Atom✝ : Type} [Repr Var✝] [Repr Atom✝] : Step Var✝ Atom✝ → ℕ → Std.Format

Equations

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

def NFChoice.DirectCertificate.Nominal.castNPrf {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] {theory : Fol.SentTheory L} {atomFormula : (Var → ℕ) → Atom → Fol.formula L} {p q : Code Var Atom} (h : p = q) (proof : NPrf theory atomFormula p) : NPrf theory atomFormula q

Proof-translation construction identified upstream as castNPrf.

Equations

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

def NFChoice.DirectCertificate.Nominal.execStep {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] [DecidableEq Atom] (theory : Fol.SentTheory L) (atomFormula : (Var → ℕ) → Atom → Fol.formula L) (inputs state : Array (Packed theory atomFormula)) : Step Var Atom → Option (Packed theory atomFormula)

Proof-translation construction identified upstream as execStep.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectCertificate.Nominal.execStep theory atomFormula inputs state (NFChoice.DirectCertificate.Nominal.Step.input index) = inputs[index]?

def NFChoice.DirectCertificate.Nominal.run {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] [DecidableEq Atom] (theory : Fol.SentTheory L) (atomFormula : (Var → ℕ) → Atom → Fol.formula L) (inputs : Array (Packed theory atomFormula)) : List (Step Var Atom) → Array (Packed theory atomFormula) → Option (Array (Packed theory atomFormula))

Execute a topologically ordered proof DAG with actual node sharing.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectCertificate.Nominal.run theory atomFormula inputs [] x✝ = some x✝

def NFChoice.DirectCertificate.Nominal.extract {Var Atom : Type} {L : Fol.Language} [DecidableEq Var] [DecidableEq Atom] (theory : Fol.SentTheory L) (atomFormula : (Var → ℕ) → Atom → Fol.formula L) (state : Array (Packed theory atomFormula)) (index : ℕ) (goal : Code Var Atom) : Option (NPrf theory atomFormula goal)

Proof-translation construction identified upstream as extract.

Equations

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

Exact real-source slices

inductive NFChoice.DirectCertificate.Nominal.SourceVar : Type

Proof-translation construction identified upstream as SourceVar.

• x : SourceVar
• y : SourceVar

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instDecidableEqSourceVar : DecidableEq SourceVar

Equations

• NFChoice.DirectCertificate.Nominal.instDecidableEqSourceVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NFChoice.DirectCertificate.Nominal.instReprSourceVar.repr : SourceVar → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instReprSourceVar : Repr SourceVar

Equations

• NFChoice.DirectCertificate.Nominal.instReprSourceVar = { reprPrec := NFChoice.DirectCertificate.Nominal.instReprSourceVar.repr }

inductive NFChoice.DirectCertificate.Nominal.NoAtom : Type

Proof-translation construction identified upstream as NoAtom.

def NFChoice.DirectCertificate.Nominal.instDecidableEqNoAtom.decEq (x✝ x✝¹ : NoAtom) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instDecidableEqNoAtom : DecidableEq NoAtom

Equations

• NFChoice.DirectCertificate.Nominal.instDecidableEqNoAtom = NFChoice.DirectCertificate.Nominal.instDecidableEqNoAtom.decEq

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instReprNoAtom : Repr NoAtom

Equations

• NFChoice.DirectCertificate.Nominal.instReprNoAtom = { reprPrec := NFChoice.DirectCertificate.Nominal.instReprNoAtom.repr }

def NFChoice.DirectCertificate.Nominal.instReprNoAtom.repr : NoAtom → ℕ → Std.Format

def NFChoice.DirectCertificate.Nominal.noAtomFormula : (SourceVar → ℕ) → (atom : NoAtom) → Fol.formula Foundation.LNF

Proof-translation construction identified upstream as noAtomFormula.

@[reducible, inline]

abbrev NFChoice.DirectCertificate.Nominal.eqxx : Code SourceVar NoAtom

Proof-translation construction identified upstream as eqxx.

Equations

• NFChoice.DirectCertificate.Nominal.eqxx = NFChoice.DirectCertificate.Nominal.Code.equal NFChoice.DirectCertificate.Nominal.SourceVar.x NFChoice.DirectCertificate.Nominal.SourceVar.x

@[reducible, inline]

abbrev NFChoice.DirectCertificate.Nominal.allEqxx : Code SourceVar NoAtom

Proof-translation construction identified upstream as allEqxx.

Equations

• NFChoice.DirectCertificate.Nominal.allEqxx = NFChoice.DirectCertificate.Nominal.Code.all NFChoice.DirectCertificate.Nominal.SourceVar.x NFChoice.DirectCertificate.Nominal.eqxx

def NFChoice.DirectCertificate.Nominal.stdpc6Certificate : List (Step SourceVar NoAtom)

Exact proof-bearing stdpc6 trace: equid, then ax-gen.

Equations

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

def NFChoice.DirectCertificate.Nominal.stdpc6Result : Option (NPrf Foundation.ExactLiteralTrial.LiteralHailperinNF noAtomFormula allEqxx)

Proof-translation construction identified upstream as stdpc6Result.

Equations

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

def NFChoice.DirectCertificate.Nominal.stdpc6Proof : NPrf Foundation.ExactLiteralTrial.LiteralHailperinNF noAtomFormula allEqxx

Proof-translation construction identified upstream as stdpc6Proof.

Equations

• NFChoice.DirectCertificate.Nominal.stdpc6Proof = NFChoice.DirectCertificate.Nominal.stdpc6Result.get NFChoice.DirectCertificate.Nominal.stdpc6Proof._proof_1

inductive NFChoice.DirectCertificate.Nominal.SchematicAtom : Type

Proof-translation construction identified upstream as SchematicAtom.

• ph : SchematicAtom

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instDecidableEqSchematicAtom : DecidableEq SchematicAtom

Equations

• NFChoice.DirectCertificate.Nominal.instDecidableEqSchematicAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NFChoice.DirectCertificate.Nominal.instReprSchematicAtom.repr : SchematicAtom → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NFChoice.DirectCertificate.Nominal.instReprSchematicAtom : Repr SchematicAtom

Equations

• NFChoice.DirectCertificate.Nominal.instReprSchematicAtom = { reprPrec := NFChoice.DirectCertificate.Nominal.instReprSchematicAtom.repr }

@[reducible, inline]

abbrev NFChoice.DirectCertificate.Nominal.ph : Code SourceVar SchematicAtom

Proof-translation construction identified upstream as ph.

Equations

• NFChoice.DirectCertificate.Nominal.ph = NFChoice.DirectCertificate.Nominal.Code.atom NFChoice.DirectCertificate.Nominal.SchematicAtom.ph

@[reducible, inline]

abbrev NFChoice.DirectCertificate.Nominal.allYPh : Code SourceVar SchematicAtom

Proof-translation construction identified upstream as allYPh.

Equations

• NFChoice.DirectCertificate.Nominal.allYPh = NFChoice.DirectCertificate.Nominal.Code.all NFChoice.DirectCertificate.Nominal.SourceVar.y NFChoice.DirectCertificate.Nominal.ph

@[reducible, inline]

abbrev NFChoice.DirectCertificate.Nominal.allXAllYPh : Code SourceVar SchematicAtom

Proof-translation construction identified upstream as allXAllYPh.

Equations

• NFChoice.DirectCertificate.Nominal.allXAllYPh = NFChoice.DirectCertificate.Nominal.Code.all NFChoice.DirectCertificate.Nominal.SourceVar.x NFChoice.DirectCertificate.Nominal.allYPh

def NFChoice.DirectCertificate.Nominal.gen2Certificate : List (Step SourceVar SchematicAtom)

Exact proof-bearing gen2 trace: input hypothesis and two ax-gens.

Equations

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

def NFChoice.DirectCertificate.Nominal.gen2Result (atomFormula : (SourceVar → ℕ) → SchematicAtom → Fol.formula Foundation.LNF) (hypothesis : NPrf Foundation.ExactLiteralTrial.LiteralHailperinNF atomFormula ph) : Option (NPrf Foundation.ExactLiteralTrial.LiteralHailperinNF atomFormula allXAllYPh)

Proof-translation construction identified upstream as gen2Result.

Equations

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

def NFChoice.DirectCertificate.Nominal.gen2Proof (atomFormula : (SourceVar → ℕ) → SchematicAtom → Fol.formula Foundation.LNF) (hypothesis : NPrf Foundation.ExactLiteralTrial.LiteralHailperinNF atomFormula ph) : NPrf Foundation.ExactLiteralTrial.LiteralHailperinNF atomFormula allXAllYPh

Proof-translation construction identified upstream as gen2Proof.

Equations

• NFChoice.DirectCertificate.Nominal.gen2Proof atomFormula hypothesis = (NFChoice.DirectCertificate.Nominal.gen2Result atomFormula hypothesis).get ⋯