Nominal proof certificates grouped in dependency order.

Certificates from NAR5H088P001Part006.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088SplitAlpha0003 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : Nominal.TAlphaWff [(nb088AlphaDummy047 A B C R, nb088AlphaDummy048 u A B R), (nb088AlphaDummy041 A B C R, nb088AlphaDummy042 u A B R), (nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy047 A B C R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb088AlphaDummy043 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy044 A B C R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb088AlphaDummy041 A B C R))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy043 A B C R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy044 A B C R)))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy048 u A B R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb088AlphaDummy045 u A B R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy046 u A B R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb088AlphaDummy042 u A B R))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy045 u A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy046 u A B R))))))))

Checked nominal proof certificate identified upstream as nb088_split_alpha_0003.

Equations

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

Certificates from NAR5H088P001Part007.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088SplitAlpha0004 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : Nominal.TAlphaWff [(nb088AlphaDummy044 A B C R, nb088AlphaDummy046 u A B R), (nb088AlphaDummy043 A B C R, nb088AlphaDummy045 u A B R), (nb088AlphaDummy075 A B C R, nb088AlphaDummy076 u A B R), (nb088AlphaDummy047 A B C R, nb088AlphaDummy048 u A B R), (nb088AlphaDummy041 A B C R, nb088AlphaDummy042 u A B R), (nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy044 A B C R)) (SemanticCore.Class.cv (nb088AlphaDummy000 A B C R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy043 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy044 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy046 u A B R)) (SemanticCore.Class.cv u)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy045 u A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy046 u A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb088_split_alpha_0004.

Equations

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0202 (A B C R : SemanticCore.Class) : nb088AlphaDummy041 A B C R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0204 (A B C R : SemanticCore.Class) : nb088AlphaDummy001 A B C R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0014 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy002 u A B C R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0015 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy002 u A B C R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0016 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy002 u A B C R ∉ R.fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0206 (A B C R : SemanticCore.Class) : nb088AlphaDummy000 A B C R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0207 (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.nb088_focused_notmem_0020 (A B C R : SemanticCore.Class) : nb088AlphaDummy003 A B C R ∉ A.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0208 (A B C R : SemanticCore.Class) : nb088AlphaDummy003 A B C R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0023 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy004 u A B C R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0024 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy004 u A B C R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0025 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy004 u A B C R ∉ R.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_compact_envfresh_0015 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : Nominal.TEnvFresh [(nb088AlphaDummy041 A B C R, nb088AlphaDummy042 u A B R), (nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088WppRefl0015 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : Nominal.TReflOn [(nb088AlphaDummy041 A B C R, nb088AlphaDummy042 u A B R), (nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

Checked nominal proof certificate identified upstream as nb088_wpp_refl_0015.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdcodemap2 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) (__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_u : u ∉ A.fv) (__dv_B_C : Disjoint B.fv C.fv) (__dv_B_R : Disjoint B.fv R.fv) (dv_B_u : u ∉ B.fv) (__dv_C_R : Disjoint C.fv R.fv) (dv_C_u : u ∉ C.fv) (dv_R_u : u ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdcodemap2 R A B C) (Compiler.CompactSourceSyntax.synCmpt u (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)) (Compiler.CompactSourceSyntax.synCfdrowfib R A B (SemanticCore.Class.cv u))))

Checked nominal proof certificate identified upstream as nominal_df_fdcodemap2.

Equations

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