Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart053.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtfinrelk (M X : SemanticCore.Class) (hyp_eqtfinrelk_1 : Nominal.NPrf (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCvv)) (hyp_eqtfinrelk_2 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn M) X) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcnvk Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk)) (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.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCidk)) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synCvv)))) (SemanticCore.Wff.classEq X (Compiler.CompactSourceSyntax.synCtfin M)))

Checked nominal proof certificate identified upstream as g_eqtfinrelk.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart054.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinrelkex : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcnvk Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk)) (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.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCidk)) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synCvv))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_tfinrelkex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_tfineq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinprop (M : SemanticCore.Class) (a : SemanticCore.Var) (dv_M_a : a ∉ M.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne M Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin M) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex a M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCtfin M)))))

Checked nominal proof certificate identified upstream as g_tfinprop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinnnul (M : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne M Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCtfin M) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_tfinnnul.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinnul : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtfin Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_tfinnul.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfincl (N : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin N) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_tfincl.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart055.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfin11 (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.synCtfin M) (Compiler.CompactSourceSyntax.synCtfin N))).imp (SemanticCore.Wff.classEq M N))

Checked nominal proof certificate identified upstream as g_tfin11.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinpw1 (A M : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem A M)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCtfin M)))

Checked nominal proof certificate identified upstream as g_tfinpw1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfintfin (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem A V)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtfin (Compiler.CompactSourceSyntax.synCncfin A)) (Compiler.CompactSourceSyntax.synCncfin (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_ncfintfin.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart056.

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

Checked nominal proof certificate identified upstream as g_tfindi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfin0c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtfin Compiler.CompactSourceSyntax.synC0c) Compiler.CompactSourceSyntax.synC0c)

Checked nominal proof certificate identified upstream as g_tfin0c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinsuc (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC0)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtfin (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCtfin A) Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_tfinsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfin1c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtfin Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_tfin1c.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart057.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinltfinlem1 (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk M N) Compiler.CompactSourceSyntax.synCltfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCtfin M) (Compiler.CompactSourceSyntax.synCtfin N)) Compiler.CompactSourceSyntax.synCltfin)))

Checked nominal proof certificate identified upstream as g_tfinltfinlem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinltfin (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.classMem (Compiler.CompactSourceSyntax.synCopk M N) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCtfin M) (Compiler.CompactSourceSyntax.synCtfin N)) Compiler.CompactSourceSyntax.synCltfin)))

Checked nominal proof certificate identified upstream as g_tfinltfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinlefin (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.classMem (Compiler.CompactSourceSyntax.synCopk M N) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCtfin M) (Compiler.CompactSourceSyntax.synCtfin N)) Compiler.CompactSourceSyntax.synClefin)))

Checked nominal proof certificate identified upstream as g_tfinlefin.

Equations

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