Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpfinex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCspfin Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_spfinex.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcvspfin : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synCspfin)

Checked nominal proof certificate identified upstream as g_ncvspfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpfinsfincl (X Z : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCspfin) (Compiler.CompactSourceSyntax.synWsfin Z X)).imp (SemanticCore.Wff.classMem Z Compiler.CompactSourceSyntax.synCspfin))

Checked nominal proof certificate identified upstream as g_spfinsfincl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpfininduct (x z : SemanticCore.Var) (B V : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_z : x ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem B V) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv) B) (Compiler.CompactSourceSyntax.synWral x Compiler.CompactSourceSyntax.synCspfin (SemanticCore.Wff.all z ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (Compiler.CompactSourceSyntax.synWsfin (SemanticCore.Class.cv z) (SemanticCore.Class.cv x))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) B))))).imp (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCspfin B))

Checked nominal proof certificate identified upstream as g_spfininduct.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinspnn : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCspfin (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0))))

Checked nominal proof certificate identified upstream as g_vfinspnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1cvsfin : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (Compiler.CompactSourceSyntax.synWsfin (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_n_1cvsfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1cspfin : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCspfin))

Checked nominal proof certificate identified upstream as g_n_1cspfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTncveqnc1fin : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtfin (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_tncveqnc1fin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gT1csfin1c : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (Compiler.CompactSourceSyntax.synWsfin (Compiler.CompactSourceSyntax.synCtfin (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_t1csfin1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfintle (N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne N Compiler.CompactSourceSyntax.synC0)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCtfin N) (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synClefin))

Checked nominal proof certificate identified upstream as g_vfintle.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfin1cltv : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv)) Compiler.CompactSourceSyntax.synCltfin))

Checked nominal proof certificate identified upstream as g_vfin1cltv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinncvntnn (N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCtfin N) (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_vfinncvntnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinncvntsp (x a : SemanticCore.Var) (dv_a_x : a ≠ x) : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCspfin (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv x)))))).neg)

Checked nominal proof certificate identified upstream as g_vfinncvntsp.

Equations

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