Nominal proof certificates grouped in dependency order.

Certificates from NAR4C089C001Part006.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089SplitAlpha0002 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TAlphaWff [(nb089AlphaDummy051 A B R, nb089AlphaDummy052 u A B R), (nb089AlphaDummy049 A B R, nb089AlphaDummy050 u A B R), (nb089AlphaDummy043 A B R, nb089AlphaDummy044 u A B R), (nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy051 A B R)) (SemanticCore.Class.cab (nb089AlphaDummy045 A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy046 A B R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb089AlphaDummy043 A B R))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy045 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy046 A B R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy051 A B R)) (SemanticCore.Class.cab (nb089AlphaDummy045 A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy046 A B R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb089AlphaDummy043 A B R))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy045 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy046 A B R))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy052 u A B R)) (SemanticCore.Class.cab (nb089AlphaDummy047 u A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy048 u A B R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb089AlphaDummy044 u A B R))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy047 u A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy048 u A B R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy052 u A B R)) (SemanticCore.Class.cab (nb089AlphaDummy047 u A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy048 u A B R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb089AlphaDummy044 u A B R))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy047 u A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy048 u A B R))))))).neg)

Checked nominal proof certificate identified upstream as nb089_split_alpha_0002.

Equations

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

Certificates from NAR4C089C001Part007.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089SplitAlpha0003 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TAlphaWff [(nb089AlphaDummy046 A B R, nb089AlphaDummy048 u A B R), (nb089AlphaDummy045 A B R, nb089AlphaDummy047 u A B R), (nb089AlphaDummy077 A B R, nb089AlphaDummy078 u A B R), (nb089AlphaDummy049 A B R, nb089AlphaDummy050 u A B R), (nb089AlphaDummy043 A B R, nb089AlphaDummy044 u A B R), (nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy046 A B R)) (SemanticCore.Class.cv (nb089AlphaDummy000 A B R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy045 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy046 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy048 u A B R)) (SemanticCore.Class.cv u)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy047 u A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy048 u A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb089_split_alpha_0003.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0007 (A B R : SemanticCore.Class) : nb089AlphaDummy043 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0008 (A B R : SemanticCore.Class) : nb089AlphaDummy043 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0009 (A B R : SemanticCore.Class) : nb089AlphaDummy043 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0212 (A B R : SemanticCore.Class) : nb089AlphaDummy043 A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0010 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy044 u A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0011 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy044 u A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0012 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy044 u A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0213 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy044 u A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0013 (A B R : SemanticCore.Class) : nb089AlphaDummy003 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0014 (A B R : SemanticCore.Class) : nb089AlphaDummy003 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0214 (A B R : SemanticCore.Class) : nb089AlphaDummy003 A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0015 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy004 u A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0016 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy004 u A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0215 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy004 u A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0017 (A B R : SemanticCore.Class) : nb089AlphaDummy000 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0018 (A B R : SemanticCore.Class) : nb089AlphaDummy000 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0216 (A B R : SemanticCore.Class) : nb089AlphaDummy000 A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0217 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : u ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0019 (A B R : SemanticCore.Class) : nb089AlphaDummy005 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0020 (A B R : SemanticCore.Class) : nb089AlphaDummy005 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0218 (A B R : SemanticCore.Class) : nb089AlphaDummy005 A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0021 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy006 u A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0022 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy006 u A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0219 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy006 u A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0023 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0024 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0220 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0025 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_B_u : u ∉ B.fv) : nb089AlphaDummy002 u A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0026 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy002 u A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0221 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_B_u : u ∉ B.fv) : nb089AlphaDummy002 u A B R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_compact_envfresh_0015 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : Nominal.TEnvFresh [(nb089AlphaDummy043 A B R, nb089AlphaDummy044 u A B R), (nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0015 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : Nominal.TReflOn [(nb089AlphaDummy043 A B R, nb089AlphaDummy044 u A B R), (nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

Checked nominal proof certificate identified upstream as nb089_wpp_refl_0015.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0015 u A B R dv_A_u dv_B_u dv_R_u = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0222 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0223 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy002 u A B R ∉ (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_compact_envfresh_0016 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TEnvFresh [(nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0016 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TReflOn [(nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.fv

Checked nominal proof certificate identified upstream as nb089_wpp_refl_0016.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0016 u A B R = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0224 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.neg.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0225 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy002 u A B R ∉ (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.neg.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_compact_envfresh_0018 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TEnvFresh [(nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.neg.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0018 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TReflOn [(nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).neg.neg.fv

Checked nominal proof certificate identified upstream as nb089_wpp_refl_0018.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0018 u A B R = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdglobalrowmap (u : SemanticCore.Var) (A B R : SemanticCore.Class) (__dv_A_B : Disjoint A.fv B.fv) (__dv_A_R : Disjoint A.fv R.fv) (dv_A_u : u ∉ A.fv) (__dv_B_R : Disjoint B.fv R.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdglobalrowmap R A B) (Compiler.CompactSourceSyntax.synCif (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synCmpt u (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))) (Compiler.CompactSourceSyntax.synCfdrowfib R A B (SemanticCore.Class.cv u))) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as nominal_df_fdglobalrowmap.

Equations

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