NF weak partition development: NAR4C086C001Part001.

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

Checked nominal proof certificate identified upstream as nb086_alpha_dummy_000.

Equations

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

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

Checked nominal proof certificate identified upstream as nb086_alpha_dummy_001.

Equations

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

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

Checked nominal proof certificate identified upstream as nb086_alpha_dummy_002.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086AlphaDummy003 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb086_alpha_dummy_003.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086AlphaDummy003 x A B R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv ∪ (NFChoice.SemanticCore.Class.cv x).fv)

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_fresh_000 (A B C R : SemanticCore.Class) : nb086AlphaDummy002 A B C R ∉ R.fv ∪ A.fv ∪ B.fv ∪ (SemanticCore.Class.cv (nb086AlphaDummy001 A B C R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_fresh_001 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : nb086AlphaDummy003 x A B R ∉ R.fv ∪ A.fv ∪ B.fv ∪ (SemanticCore.Class.cv x).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_distinct_004 (A B C R : SemanticCore.Class) : nb086AlphaDummy000 A B C R ≠ nb086AlphaDummy001 A B C R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_support_mem_0000 (A B C R : SemanticCore.Class) : nb086AlphaDummy001 A B C R ∈ R.fv ∪ A.fv ∪ B.fv ∪ (SemanticCore.Class.cv (nb086AlphaDummy001 A B C R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_support_mem_0001 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : x ∈ R.fv ∪ A.fv ∪ B.fv ∪ (SemanticCore.Class.cv x).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_compact_envfresh_0000 (x : SemanticCore.Var) (A B C R : SemanticCore.Class) (q : SemanticCore.Var) (dv_C_q : q ∉ C.fv) (dv_C_x : x ∉ C.fv) : Nominal.TEnvFresh [(nb086AlphaDummy001 A B C R, x), (nb086AlphaDummy000 A B C R, q)] C.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086FocusedRefl0000 (x : SemanticCore.Var) (A B C R : SemanticCore.Class) (q : SemanticCore.Var) (dv_C_q : q ∉ C.fv) (dv_C_x : x ∉ C.fv) : Nominal.TReflOn [(nb086AlphaDummy001 A B C R, x), (nb086AlphaDummy000 A B C R, q)] C.fv

Checked nominal proof certificate identified upstream as nb086_focused_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086FocusedRefl0000 x A B C R q dv_C_q dv_C_x = ⋯.reflOn

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_focused_notmem_0005 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : nb086AlphaDummy003 x A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_focused_notmem_0006 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : nb086AlphaDummy003 x A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_focused_notmem_0007 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : nb086AlphaDummy003 x A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_wpp_notmem_0001 (x : SemanticCore.Var) (A B R : SemanticCore.Class) : nb086AlphaDummy003 x A B R ∉ (Compiler.CompactSourceSyntax.synCfdif R A B).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_wpp_notmem_0003 (x : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) : x ∉ (Compiler.CompactSourceSyntax.synCfdif R A B).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_wpp_notmem_0005 (A B R : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_B_q : q ∉ B.fv) (dv_R_q : q ∉ R.fv) : q ∉ (Compiler.CompactSourceSyntax.synCfdif R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086_compact_envfresh_0001 (x : SemanticCore.Var) (A B C R : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_B_q : q ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_R_q : q ∉ R.fv) (dv_R_x : x ∉ R.fv) : Nominal.TEnvFresh [(nb086AlphaDummy002 A B C R, nb086AlphaDummy003 x A B R), (nb086AlphaDummy001 A B C R, x), (nb086AlphaDummy000 A B C R, q)] (Compiler.CompactSourceSyntax.synCfdif R A B).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086WppRefl0000 (x : SemanticCore.Var) (A B C R : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_B_q : q ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_R_q : q ∉ R.fv) (dv_R_x : x ∉ R.fv) : Nominal.TReflOn [(nb086AlphaDummy002 A B C R, nb086AlphaDummy003 x A B R), (nb086AlphaDummy001 A B C R, x), (nb086AlphaDummy000 A B C R, q)] (Compiler.CompactSourceSyntax.synCfdif R A B).fv

Checked nominal proof certificate identified upstream as nb086_wpp_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb086WppRefl0000 x A B C R q dv_A_q dv_A_x dv_B_q dv_B_x dv_R_q dv_R_x = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdcode (x : SemanticCore.Var) (A B C R : SemanticCore.Class) (q : 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_q : q ∉ A.fv) (dv_A_x : x ∉ A.fv) (__dv_B_C : Disjoint B.fv C.fv) (__dv_B_R : Disjoint B.fv R.fv) (dv_B_q : q ∉ B.fv) (dv_B_x : x ∉ B.fv) (__dv_C_R : Disjoint C.fv R.fv) (dv_C_q : q ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_R_q : q ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_q_x : q ≠ x) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdcode R A B C) (SemanticCore.Class.cab q (Compiler.CompactSourceSyntax.synWrex x C (SemanticCore.Wff.classEq (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as nominal_df_fdcode.

Equations

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