Nominal proof certificates grouped in dependency order.

Certificates from NA50WN14DPart010.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050SplitAlpha0000 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(nb050AlphaDummy019 x A B, nb050AlphaDummy022 x y), (nb050AlphaDummy018 x A B, nb050AlphaDummy021 x y), (nb050AlphaDummy017 x A B, nb050AlphaDummy020 x y), (nb050AlphaDummy015 x A B, nb050AlphaDummy016 x y), (nb050AlphaDummy011 x A B, nb050AlphaDummy013 x y), (nb050AlphaDummy012 x A B, nb050AlphaDummy014 x y), (nb050AlphaDummy004 x A B, nb050AlphaDummy006 x y), (nb050AlphaDummy003 x A B, nb050AlphaDummy005 x y), (nb050AlphaDummy009 x A B, nb050AlphaDummy010 x y), (nb050AlphaDummy007 x A B, nb050AlphaDummy008 x y), (nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb050AlphaDummy018 x A B)) (SemanticCore.Class.cv (nb050AlphaDummy019 x A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy017 x A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb050AlphaDummy018 x A B)) (SemanticCore.Class.cv (nb050AlphaDummy019 x A B)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb050AlphaDummy021 x y)) (SemanticCore.Class.cv (nb050AlphaDummy022 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy020 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb050AlphaDummy021 x y)) (SemanticCore.Class.cv (nb050AlphaDummy022 x y)))).neg)

Checked nominal proof certificate identified upstream as nb050_split_alpha_0000.

Equations

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

Certificates from NA50WN14DPart013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050SplitAlpha0001 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb050AlphaDummy004 x A B, nb050AlphaDummy006 x y), (nb050AlphaDummy003 x A B, nb050AlphaDummy005 x y), (nb050AlphaDummy009 x A B, nb050AlphaDummy010 x y), (nb050AlphaDummy007 x A B, nb050AlphaDummy008 x y), (nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb050AlphaDummy004 x A B)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy003 x A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb050AlphaDummy004 x A B)))).neg).neg ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb050AlphaDummy006 x y)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy005 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb050AlphaDummy006 x y)))).neg).neg

Checked nominal proof certificate identified upstream as nb050_split_alpha_0001.

Equations

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

Certificates from NA50WN14DPart018.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050SplitAlpha0002 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(nb050AlphaDummy019 x A B, nb050AlphaDummy022 x y), (nb050AlphaDummy018 x A B, nb050AlphaDummy021 x y), (nb050AlphaDummy017 x A B, nb050AlphaDummy020 x y), (nb050AlphaDummy015 x A B, nb050AlphaDummy016 x y), (nb050AlphaDummy011 x A B, nb050AlphaDummy013 x y), (nb050AlphaDummy012 x A B, nb050AlphaDummy014 x y), (nb050AlphaDummy037 x A B, nb050AlphaDummy038 x y), (nb050AlphaDummy035 x A B, nb050AlphaDummy036 x y), (nb050AlphaDummy004 x A B, nb050AlphaDummy006 x y), (nb050AlphaDummy003 x A B, nb050AlphaDummy005 x y), (nb050AlphaDummy033 x A B, nb050AlphaDummy034 x y), (nb050AlphaDummy007 x A B, nb050AlphaDummy008 x y), (nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb050AlphaDummy018 x A B)) (SemanticCore.Class.cv (nb050AlphaDummy019 x A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy017 x A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb050AlphaDummy018 x A B)) (SemanticCore.Class.cv (nb050AlphaDummy019 x A B)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb050AlphaDummy021 x y)) (SemanticCore.Class.cv (nb050AlphaDummy022 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy020 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb050AlphaDummy021 x y)) (SemanticCore.Class.cv (nb050AlphaDummy022 x y)))).neg)

Checked nominal proof certificate identified upstream as nb050_split_alpha_0002.

Equations

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

Certificates from NA50WN14DPart021.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050SplitAlpha0003 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(nb050AlphaDummy037 x A B, nb050AlphaDummy038 x y), (nb050AlphaDummy035 x A B, nb050AlphaDummy036 x y), (nb050AlphaDummy004 x A B, nb050AlphaDummy006 x y), (nb050AlphaDummy003 x A B, nb050AlphaDummy005 x y), (nb050AlphaDummy033 x A B, nb050AlphaDummy034 x y), (nb050AlphaDummy007 x A B, nb050AlphaDummy008 x y), (nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb050AlphaDummy037 x A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb050AlphaDummy004 x A B)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb050AlphaDummy037 x A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb050AlphaDummy004 x A B)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb050AlphaDummy038 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb050AlphaDummy006 x y)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb050AlphaDummy038 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb050AlphaDummy006 x y)))).neg)

Checked nominal proof certificate identified upstream as nb050_split_alpha_0003.

Equations

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

Certificates from NA50WN14DPart024.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050SplitAlpha0004 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy001 x A B)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv (nb050AlphaDummy000 x A B)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb050AlphaDummy002 x y A B)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))

Checked nominal proof certificate identified upstream as nb050_split_alpha_0004.

Equations

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

Certificates from NA50WN14DPart025.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_focused_notmem_0000 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy000 x A B ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0110 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy000 x A B ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0111 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : y ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_focused_notmem_0001 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy001 x A B ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0112 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy001 x A B ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_focused_notmem_0002 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy002 x y A B ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0113 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy002 x y A B ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).fv

Certificates from NA50WN14DPart026.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_compact_envfresh_0008 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.TEnvFresh [(nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050WppRefl0008 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.TReflOn [(nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).fv

Checked nominal proof certificate identified upstream as nb050_wpp_refl_0008.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050WppRefl0008 x y A B dv_A_y dv_x_y = ⋯.reflOn

Certificates from NA50WN14DPart027.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_focused_notmem_0003 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy000 x A B ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0114 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy000 x A B ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0115 (y : SemanticCore.Var) (B : SemanticCore.Class) (dv_B_y : y ∉ B.fv) : y ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_focused_notmem_0004 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy001 x A B ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0116 (x : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy001 x A B ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_focused_notmem_0005 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy002 x y A B ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_wpp_notmem_0117 (x y : SemanticCore.Var) (A B : SemanticCore.Class) : nb050AlphaDummy002 x y A B ∉ B.fv

Certificates from NA50WN14DPart028.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050_compact_envfresh_0009 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_y : y ∉ B.fv) : Nominal.TEnvFresh [(nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] B.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050WppRefl0009 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_y : y ∉ B.fv) : Nominal.TReflOn [(nb050AlphaDummy000 x A B, y), (x, x), (nb050AlphaDummy001 x A B, nb050AlphaDummy002 x y A B)] B.fv

Checked nominal proof certificate identified upstream as nb050_wpp_refl_0009.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb050WppRefl0009 x y A B dv_B_y = ⋯.reflOn

Certificates from NA50WN14DPart029.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfMpt (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCmpt x A B) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))

Checked nominal proof certificate identified upstream as nominal_df_mpt.

Equations

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