Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSrelkex : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_srelkex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfineq1 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsfin A C) (Compiler.CompactSourceSyntax.synWsfin B C)))

Checked nominal proof certificate identified upstream as g_sfineq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfineq2 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsfin C A) (Compiler.CompactSourceSyntax.synWsfin C B)))

Checked nominal proof certificate identified upstream as g_sfineq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfin01 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWsfin Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_sfin01.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfin112 (P M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWsfin M N) (Compiler.CompactSourceSyntax.synWsfin M P)).imp (SemanticCore.Wff.classEq N P))

Checked nominal proof certificate identified upstream as g_sfin112.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfindbl (A : SemanticCore.Class) (n : SemanticCore.Var) (M : SemanticCore.Class) (dv_M_n : n ∉ M.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWsfin M (SemanticCore.Class.cv n)) (Compiler.CompactSourceSyntax.synWsfin (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_sfindbl.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfintfinlem1 (m n : SemanticCore.Var) (dv_m_n : m ≠ n) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m (SemanticCore.Wff.all n ((Compiler.CompactSourceSyntax.synWsfin (SemanticCore.Class.cv m) (SemanticCore.Class.cv n)).imp (Compiler.CompactSourceSyntax.synWsfin (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv m)) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv n)))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_sfintfinlem1.

Equations

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