Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part011.

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

Checked nominal proof certificate identified upstream as g_pw1fnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnpw1fn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCpw1fn Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_fnpw1fn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrpw1fn (A B : SemanticCore.Class) (hyp_brpw1fn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synCpw1fn B) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_brpw1fn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1fnf1o : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o Compiler.CompactSourceSyntax.synCpw1fn Compiler.CompactSourceSyntax.synC1c (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c))

Checked nominal proof certificate identified upstream as g_pw1fnf1o.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfullfunlem1 (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid F) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCid) F)) B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A F B) (SemanticCore.Wff.all x ((Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) B)))))

Checked nominal proof certificate identified upstream as g_fnfullfunlem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfullfunlem2 (F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid F) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCid) F)))

Checked nominal proof certificate identified upstream as g_fnfullfunlem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfullfun (F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfullfun F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fnfullfun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFullfunexg (F V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem F V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfullfun F) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fullfunexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFullfunex (F : SemanticCore.Class) (hyp_fullfunex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfullfun F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fullfunex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvfullfunlem1 (x y : SemanticCore.Var) (F : SemanticCore.Class) (dv_F_x : x ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid F) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCid) F))) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) F (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_fvfullfunlem1.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvfullfunlem2 (F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid F) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCid) F)) F)

Checked nominal proof certificate identified upstream as g_fvfullfunlem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvfullfunlem3 (A F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid F) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCid) F)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid F) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCid) F)) A) (Compiler.CompactSourceSyntax.synCfv F A)))

Checked nominal proof certificate identified upstream as g_fvfullfunlem3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvfullfun (A F : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfullfun F) A) (Compiler.CompactSourceSyntax.synCfv F A))

Checked nominal proof certificate identified upstream as g_fvfullfun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvdomfn (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCdomfn A) (Compiler.CompactSourceSyntax.synCdm A)))

Checked nominal proof certificate identified upstream as g_fvdomfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvranfn (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCranfn A) (Compiler.CompactSourceSyntax.synCrn A)))

Checked nominal proof certificate identified upstream as g_fvranfn.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part014.

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

Checked nominal proof certificate identified upstream as g_domfnex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ranfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1eq1 (R S T : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq S T).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCclos1 S R) (Compiler.CompactSourceSyntax.synCclos1 T R)))

Checked nominal proof certificate identified upstream as g_clos1eq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1eq2 (R S T : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq R T).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCclos1 S R) (Compiler.CompactSourceSyntax.synCclos1 S T)))

Checked nominal proof certificate identified upstream as g_clos1eq2.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1ex (R S : SemanticCore.Class) (hyp_clos1ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1ex_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCclos1 S R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_clos1ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1exg (R S V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem S V) (SemanticCore.Wff.classMem R W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCclos1 S R) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_clos1exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1base (C R S : SemanticCore.Class) (hyp_clos1base_1 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss S C)

Checked nominal proof certificate identified upstream as g_clos1base.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1conn (A B C R S : SemanticCore.Class) (hyp_clos1base_1 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (Compiler.CompactSourceSyntax.synWbr A R B)).imp (SemanticCore.Wff.classMem B C))

Checked nominal proof certificate identified upstream as g_clos1conn.

Equations

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