Nominal proof certificates grouped in dependency order.

Certificates from NAR4H5C097M3Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097SplitAlpha0000 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) : Nominal.TAlphaWff [(nb097AlphaDummy009 C F, nb097AlphaDummy011 k m), (nb097AlphaDummy008 C F, nb097AlphaDummy010 k m), (nb097AlphaDummy038 C F, nb097AlphaDummy039 k m), (nb097AlphaDummy012 C F, nb097AlphaDummy013 k m), (nb097AlphaDummy000 C F, k), (nb097AlphaDummy001 C F, m), (nb097AlphaDummy002 C F, nb097AlphaDummy003 C k m F), (nb097AlphaDummy005 C F, nb097AlphaDummy007 C k m F), (nb097AlphaDummy004 C F, nb097AlphaDummy006 C k m F)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb097AlphaDummy009 C F)) (SemanticCore.Class.cv (nb097AlphaDummy000 C F))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb097AlphaDummy008 C F)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb097AlphaDummy009 C F))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb097AlphaDummy011 k m)) (SemanticCore.Class.cv k)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb097AlphaDummy010 k m)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb097AlphaDummy011 k m))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb097_split_alpha_0000.

Equations

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

Certificates from NAR4H5C097M3Part002.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097SplitAlpha0001 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) (dv_k_m : k ≠ m) : Nominal.TAlphaWff [(nb097AlphaDummy012 C F, nb097AlphaDummy013 k m), (nb097AlphaDummy000 C F, k), (nb097AlphaDummy001 C F, m), (nb097AlphaDummy002 C F, nb097AlphaDummy003 C k m F), (nb097AlphaDummy005 C F, nb097AlphaDummy007 C k m F), (nb097AlphaDummy004 C F, nb097AlphaDummy006 C k m F)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb097AlphaDummy012 C F)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb097AlphaDummy008 C F) (Compiler.CompactSourceSyntax.synWrex (nb097AlphaDummy009 C F) (SemanticCore.Class.cv (nb097AlphaDummy001 C F)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb097AlphaDummy008 C F)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb097AlphaDummy009 C F)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb097AlphaDummy012 C F)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb097AlphaDummy008 C F) (Compiler.CompactSourceSyntax.synWrex (nb097AlphaDummy009 C F) (SemanticCore.Class.cv (nb097AlphaDummy000 C F)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb097AlphaDummy008 C F)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb097AlphaDummy009 C F))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb097AlphaDummy013 k m)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb097AlphaDummy010 k m) (Compiler.CompactSourceSyntax.synWrex (nb097AlphaDummy011 k m) (SemanticCore.Class.cv m) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb097AlphaDummy010 k m)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb097AlphaDummy011 k m)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb097AlphaDummy013 k m)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb097AlphaDummy010 k m) (Compiler.CompactSourceSyntax.synWrex (nb097AlphaDummy011 k m) (SemanticCore.Class.cv k) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb097AlphaDummy010 k m)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb097AlphaDummy011 k m))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

Checked nominal proof certificate identified upstream as nb097_split_alpha_0001.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0132 (C F : SemanticCore.Class) : nb097AlphaDummy000 C F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0133 (k : SemanticCore.Var) : k ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0134 (C F : SemanticCore.Class) : nb097AlphaDummy001 C F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0135 (m : SemanticCore.Var) : m ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0136 (C F : SemanticCore.Class) : nb097AlphaDummy002 C F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0137 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) : nb097AlphaDummy003 C k m F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0138 (C F : SemanticCore.Class) : nb097AlphaDummy005 C F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0139 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) : nb097AlphaDummy007 C k m F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0140 (C F : SemanticCore.Class) : nb097AlphaDummy004 C F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_wpp_notmem_0141 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) : nb097AlphaDummy006 C k m F ∉ Compiler.CompactSourceSyntax.synClec.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097_compact_envfresh_0009 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) : Nominal.TEnvFresh [(nb097AlphaDummy000 C F, k), (nb097AlphaDummy001 C F, m), (nb097AlphaDummy002 C F, nb097AlphaDummy003 C k m F), (nb097AlphaDummy005 C F, nb097AlphaDummy007 C k m F), (nb097AlphaDummy004 C F, nb097AlphaDummy006 C k m F)] Compiler.CompactSourceSyntax.synClec.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097WppRefl0009 (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) : Nominal.TReflOn [(nb097AlphaDummy000 C F, k), (nb097AlphaDummy001 C F, m), (nb097AlphaDummy002 C F, nb097AlphaDummy003 C k m F), (nb097AlphaDummy005 C F, nb097AlphaDummy007 C k m F), (nb097AlphaDummy004 C F, nb097AlphaDummy006 C k m F)] Compiler.CompactSourceSyntax.synClec.fv

Checked nominal proof certificate identified upstream as nb097_wpp_refl_0009.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb097WppRefl0009 C k m F = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfWppgamma (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (dv_C_m : m ∉ C.fv) (dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_k_m : k ≠ m) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwppgamma F C) (Compiler.CompactSourceSyntax.synCio m (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k))))))

Checked nominal proof certificate identified upstream as nominal_df_wppgamma.

Equations

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