Nominal proof certificates grouped in dependency order.

Certificates from NAPD051C001Part010.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051SplitAlpha0000 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.TAlphaWff [(nb051AlphaDummy019 x y A B C, nb051AlphaDummy022 x y z), (nb051AlphaDummy018 x y A B C, nb051AlphaDummy021 x y z), (nb051AlphaDummy017 x y A B C, nb051AlphaDummy020 x y z), (nb051AlphaDummy015 x y A B C, nb051AlphaDummy016 x y z), (nb051AlphaDummy011 x y A B C, nb051AlphaDummy013 x y z), (nb051AlphaDummy012 x y A B C, nb051AlphaDummy014 x y z), (nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy009 x y A B C, nb051AlphaDummy010 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy017 x y A B C)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy020 x y z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)))).neg)

Checked nominal proof certificate identified upstream as nb051_split_alpha_0000.

Equations

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

Certificates from NAPD051C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051SplitAlpha0001 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.TAlphaWff [(nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy009 x y A B C, nb051AlphaDummy010 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy003 x y A B C)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))).neg)

Checked nominal proof certificate identified upstream as nb051_split_alpha_0001.

Equations

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

Certificates from NAPD051C001Part018.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051SplitAlpha0002 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.TAlphaWff [(nb051AlphaDummy019 x y A B C, nb051AlphaDummy022 x y z), (nb051AlphaDummy018 x y A B C, nb051AlphaDummy021 x y z), (nb051AlphaDummy017 x y A B C, nb051AlphaDummy020 x y z), (nb051AlphaDummy015 x y A B C, nb051AlphaDummy016 x y z), (nb051AlphaDummy011 x y A B C, nb051AlphaDummy013 x y z), (nb051AlphaDummy012 x y A B C, nb051AlphaDummy014 x y z), (nb051AlphaDummy037 x y A B C, nb051AlphaDummy038 x y z), (nb051AlphaDummy035 x y A B C, nb051AlphaDummy036 x y z), (nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy033 x y A B C, nb051AlphaDummy034 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy017 x y A B C)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy020 x y z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)))).neg)

Checked nominal proof certificate identified upstream as nb051_split_alpha_0002.

Equations

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

Certificates from NAPD051C001Part021.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051SplitAlpha0003 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.TAlphaWff [(nb051AlphaDummy037 x y A B C, nb051AlphaDummy038 x y z), (nb051AlphaDummy035 x y A B C, nb051AlphaDummy036 x y z), (nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy033 x y A B C, nb051AlphaDummy034 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy037 x y A B C)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy037 x y A B C)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy038 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy038 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))).neg)

Checked nominal proof certificate identified upstream as nb051_split_alpha_0003.

Equations

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

Certificates from NAPD051C001Part024.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051VariableOccurrence (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.TAlphaClass [(nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy033 x y A B C, nb051AlphaDummy034 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)) (SemanticCore.Class.cv z)

Checked nominal proof certificate identified upstream as nb051_variable_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051SplitAlpha0004 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.TAlphaWff [(nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy001 x y A B C)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy002 x y z A B C)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)))

Checked nominal proof certificate identified upstream as nb051_split_alpha_0004.

Equations

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

Certificates from NAPD051C001Part025.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0000 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy000 x y A B C ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0001 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy000 x y A B C ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0110 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy000 x y A B C ∉ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0111 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_z : z ∉ A.fv) (dv_B_z : z ∉ B.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : z ∉ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0002 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy001 x y A B C ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0003 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy001 x y A B C ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0112 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy001 x y A B C ∉ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0004 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy002 x y z A B C ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0005 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy002 x y z A B C ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0113 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy002 x y z A B C ∉ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).fv

Certificates from NAPD051C001Part026.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_envfresh_0008 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_z : z ∉ A.fv) (dv_B_z : z ∉ B.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.TEnvFresh [(nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051WppRefl0008 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_z : z ∉ A.fv) (dv_B_z : z ∉ B.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.TReflOn [(nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).fv

Checked nominal proof certificate identified upstream as nb051_wpp_refl_0008.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051WppRefl0008 x y z A B C dv_A_z dv_B_z dv_x_z dv_y_z = ⋯.reflOn

Certificates from NAPD051C001Part027.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0006 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy000 x y A B C ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0114 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy000 x y A B C ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0115 (z : SemanticCore.Var) (C : SemanticCore.Class) (dv_C_z : z ∉ C.fv) : z ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0007 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy001 x y A B C ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0116 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy001 x y A B C ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_focused_notmem_0008 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy002 x y z A B C ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0117 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) : nb051AlphaDummy002 x y z A B C ∉ C.fv

Certificates from NAPD051C001Part028.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_envfresh_0009 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_C_z : z ∉ C.fv) : Nominal.TEnvFresh [(nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] C.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051WppRefl0009 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_C_z : z ∉ C.fv) : Nominal.TReflOn [(nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] C.fv

Checked nominal proof certificate identified upstream as nb051_wpp_refl_0009.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051WppRefl0009 x y z A B C dv_C_z = ⋯.reflOn

Certificates from NAPD051C001Part029.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfMpt2 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_z : z ∉ A.fv) (dv_B_z : z ∉ B.fv) (dv_C_z : z ∉ C.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCmpt2 x A y B C) (Compiler.CompactSourceSyntax.synCoprab x y z (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C))))

Checked nominal proof certificate identified upstream as nominal_df_mpt2.

Equations

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