NF weak partition development: NAR4C080C001Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080AlphaDummy000 (A B : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb080_alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080AlphaDummy000 A B = NFChoice.ReplaySupport.freshVar (A.fv ∪ B.fv)

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080_fresh_000 (A B : SemanticCore.Class) : nb080AlphaDummy000 A B ∉ A.fv ∪ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080_focused_notmem_0000 (A B : SemanticCore.Class) : nb080AlphaDummy000 A B ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080_compact_envfresh_0000 (z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_z : z ∉ A.fv) : Nominal.TEnvFresh [(nb080AlphaDummy000 A B, z)] A.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080FocusedRefl0000 (z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_z : z ∉ A.fv) : Nominal.TReflOn [(nb080AlphaDummy000 A B, z)] A.fv

Checked nominal proof certificate identified upstream as nb080_focused_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080FocusedRefl0000 z A B dv_A_z = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080_focused_notmem_0001 (A B : SemanticCore.Class) : nb080AlphaDummy000 A B ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080_compact_envfresh_0001 (z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_z : z ∉ B.fv) : Nominal.TEnvFresh [(nb080AlphaDummy000 A B, z)] B.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080FocusedRefl0001 (z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_z : z ∉ B.fv) : Nominal.TReflOn [(nb080AlphaDummy000 A B, z)] B.fv

Checked nominal proof certificate identified upstream as nb080_focused_refl_0001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb080FocusedRefl0001 z A B dv_B_z = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfSep2 (z : SemanticCore.Var) (A B : SemanticCore.Class) (__dv_A_B : Disjoint A.fv B.fv) (dv_A_z : z ∉ A.fv) (dv_B_z : z ∉ B.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsep2 A B) (SemanticCore.Class.cab z (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (SemanticCore.Class.cv z)) (SemanticCore.Wff.classMem B (SemanticCore.Class.cv z)).neg) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (SemanticCore.Class.cv z)) (SemanticCore.Wff.classMem A (SemanticCore.Class.cv z)).neg))))

Checked nominal proof certificate identified upstream as nominal_df_sep2.

Equations

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