NF weak partition development: NAR4C085C001Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085AlphaDummy000 (A B C R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb085_alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085AlphaDummy000 A B C R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv ∪ C.fv)

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_fresh_000 (A B C R : SemanticCore.Class) : nb085AlphaDummy000 A B C R ∉ R.fv ∪ A.fv ∪ B.fv ∪ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_focused_notmem_0000 (A B C R : SemanticCore.Class) : nb085AlphaDummy000 A B C R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_focused_notmem_0001 (A B C R : SemanticCore.Class) : nb085AlphaDummy000 A B C R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_focused_notmem_0002 (A B C R : SemanticCore.Class) : nb085AlphaDummy000 A B C R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_wpp_notmem_0000 (A B C R : SemanticCore.Class) : nb085AlphaDummy000 A B C R ∉ (Compiler.CompactSourceSyntax.synCfdif R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_wpp_notmem_0001 (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (dv_R_d : d ∉ R.fv) : d ∉ (Compiler.CompactSourceSyntax.synCfdif R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_compact_envfresh_0000 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (dv_R_d : d ∉ R.fv) : Nominal.TEnvFresh [(nb085AlphaDummy000 A B C R, d)] (Compiler.CompactSourceSyntax.synCfdif R A B).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085WppRefl0000 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (dv_R_d : d ∉ R.fv) : Nominal.TReflOn [(nb085AlphaDummy000 A B C R, d)] (Compiler.CompactSourceSyntax.synCfdif R A B).fv

Checked nominal proof certificate identified upstream as nb085_wpp_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085WppRefl0000 A B C R d dv_A_d dv_B_d dv_R_d = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_focused_notmem_0003 (A B C R : SemanticCore.Class) : nb085AlphaDummy000 A B C R ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085_compact_envfresh_0001 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_d : d ∉ C.fv) : Nominal.TEnvFresh [(nb085AlphaDummy000 A B C R, d)] C.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085FocusedRefl0000 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_d : d ∉ C.fv) : Nominal.TReflOn [(nb085AlphaDummy000 A B C R, d)] C.fv

Checked nominal proof certificate identified upstream as nb085_focused_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb085FocusedRefl0000 A B C R d dv_C_d = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdrow (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (__dv_A_B : Disjoint A.fv B.fv) (__dv_A_C : Disjoint A.fv C.fv) (__dv_A_R : Disjoint A.fv R.fv) (dv_A_d : d ∉ A.fv) (__dv_B_C : Disjoint B.fv C.fv) (__dv_B_R : Disjoint B.fv R.fv) (dv_B_d : d ∉ B.fv) (__dv_C_R : Disjoint C.fv R.fv) (dv_C_d : d ∉ C.fv) (dv_R_d : d ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrow R A B C) (Compiler.CompactSourceSyntax.synCrab d (Compiler.CompactSourceSyntax.synCfdif R A B) (SemanticCore.Wff.classMem C (SemanticCore.Class.cv d))))

Checked nominal proof certificate identified upstream as nominal_df_fdrow.

Equations

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