Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part026.

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

Checked nominal proof certificate identified upstream as g_vfinncsp.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVinf : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).neg

Checked nominal proof certificate identified upstream as g_vinf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNulnnn : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synCnnc).neg

Checked nominal proof certificate identified upstream as g_nulnnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPeano4 (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c))).imp (SemanticCore.Wff.classEq M N))

Checked nominal proof certificate identified upstream as g_peano4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSuc11nnc (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classEq M N)))

Checked nominal proof certificate identified upstream as g_suc11nnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddccan2 (P M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc M N) (Compiler.CompactSourceSyntax.synCplc M P)) (SemanticCore.Wff.classEq N P)))

Checked nominal proof certificate identified upstream as g_addccan2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddccan1 (P M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc M P) (Compiler.CompactSourceSyntax.synCplc N P)) (SemanticCore.Wff.classEq M N)))

Checked nominal proof certificate identified upstream as g_addccan1.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part028.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfphi2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCphi A) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv))) A))

Checked nominal proof certificate identified upstream as g_dfphi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhieq (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCphi A) (Compiler.CompactSourceSyntax.synCphi B)))

Checked nominal proof certificate identified upstream as g_phieq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhiexg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCphi A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_phiexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhiex (A : SemanticCore.Class) (hyp_phiex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCphi A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_phiex.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfop2lem1 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcomk (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv))))) Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) Compiler.CompactSourceSyntax.synCvv)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))

Checked nominal proof certificate identified upstream as g_dfop2lem1.

Equations

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