Nominal proof certificates grouped in dependency order.

Certificates from NAR4C066C001Part002.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066WppRefl0000 (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.TReflOn [(nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] A.fv

Checked nominal proof certificate identified upstream as nb066_wpp_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066WppRefl0000 x y A R dv_A_x dv_A_y = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066SplitAlpha0000 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : Nominal.TAlphaWff [(nb066AlphaDummy024 A R, nb066AlphaDummy027 x R), (nb066AlphaDummy023 A R, nb066AlphaDummy026 x R), (nb066AlphaDummy022 A R, nb066AlphaDummy025 x R), (nb066AlphaDummy020 A R, nb066AlphaDummy021 x R), (nb066AlphaDummy016 A R, nb066AlphaDummy018 x R), (nb066AlphaDummy017 A R, nb066AlphaDummy019 x R), (nb066AlphaDummy009 A R, nb066AlphaDummy011 x R), (nb066AlphaDummy008 A R, nb066AlphaDummy010 x R), (nb066AlphaDummy014 A R, nb066AlphaDummy015 x R), (nb066AlphaDummy012 A R, nb066AlphaDummy013 x R), (nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy022 A R)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy025 x R)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R)))).neg)

Checked nominal proof certificate identified upstream as nb066_split_alpha_0000.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066SplitAlpha0001 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : Nominal.TAlphaWff [(nb066AlphaDummy009 A R, nb066AlphaDummy011 x R), (nb066AlphaDummy008 A R, nb066AlphaDummy010 x R), (nb066AlphaDummy014 A R, nb066AlphaDummy015 x R), (nb066AlphaDummy012 A R, nb066AlphaDummy013 x R), (nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy009 A R)) (SemanticCore.Class.cv (nb066AlphaDummy003 A R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy008 A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy011 x R)) (SemanticCore.Class.cv (nb066AlphaDummy005 x R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy010 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R)))).neg)

Checked nominal proof certificate identified upstream as nb066_split_alpha_0001.

Equations

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

Certificates from NAR4C066C001Part003.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066SplitAlpha0002 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : Nominal.TAlphaWff [(nb066AlphaDummy024 A R, nb066AlphaDummy027 x R), (nb066AlphaDummy023 A R, nb066AlphaDummy026 x R), (nb066AlphaDummy022 A R, nb066AlphaDummy025 x R), (nb066AlphaDummy020 A R, nb066AlphaDummy021 x R), (nb066AlphaDummy016 A R, nb066AlphaDummy018 x R), (nb066AlphaDummy017 A R, nb066AlphaDummy019 x R), (nb066AlphaDummy042 A R, nb066AlphaDummy043 x R), (nb066AlphaDummy040 A R, nb066AlphaDummy041 x R), (nb066AlphaDummy009 A R, nb066AlphaDummy011 x R), (nb066AlphaDummy008 A R, nb066AlphaDummy010 x R), (nb066AlphaDummy038 A R, nb066AlphaDummy039 x R), (nb066AlphaDummy012 A R, nb066AlphaDummy013 x R), (nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy022 A R)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy025 x R)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R)))).neg)

Checked nominal proof certificate identified upstream as nb066_split_alpha_0002.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066SplitAlpha0003 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : Nominal.TAlphaClass [(nb066AlphaDummy042 A R, nb066AlphaDummy043 x R), (nb066AlphaDummy040 A R, nb066AlphaDummy041 x R), (nb066AlphaDummy009 A R, nb066AlphaDummy011 x R), (nb066AlphaDummy008 A R, nb066AlphaDummy010 x R), (nb066AlphaDummy038 A R, nb066AlphaDummy039 x R), (nb066AlphaDummy012 A R, nb066AlphaDummy013 x R), (nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] (SemanticCore.Class.cab (nb066AlphaDummy017 A R) (Compiler.CompactSourceSyntax.synWrex (nb066AlphaDummy016 A R) (SemanticCore.Class.cv (nb066AlphaDummy009 A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy017 A R)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy016 A R)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb066AlphaDummy016 A R)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb066AlphaDummy016 A R)))))) (SemanticCore.Class.cab (nb066AlphaDummy019 x R) (Compiler.CompactSourceSyntax.synWrex (nb066AlphaDummy018 x R) (SemanticCore.Class.cv (nb066AlphaDummy011 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy019 x R)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy018 x R)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb066AlphaDummy018 x R)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb066AlphaDummy018 x R))))))

Checked nominal proof certificate identified upstream as nb066_split_alpha_0003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066SplitAlpha0004 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : Nominal.TAlphaWff [(nb066AlphaDummy038 A R, nb066AlphaDummy039 x R), (nb066AlphaDummy012 A R, nb066AlphaDummy013 x R), (nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy038 A R)) (SemanticCore.Class.cab (nb066AlphaDummy008 A R) (Compiler.CompactSourceSyntax.synWrex (nb066AlphaDummy009 A R) (SemanticCore.Class.cv (nb066AlphaDummy002 A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy008 A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy038 A R)) (SemanticCore.Class.cab (nb066AlphaDummy008 A R) (Compiler.CompactSourceSyntax.synWrex (nb066AlphaDummy009 A R) (SemanticCore.Class.cv (nb066AlphaDummy002 A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy008 A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy039 x R)) (SemanticCore.Class.cab (nb066AlphaDummy010 x R) (Compiler.CompactSourceSyntax.synWrex (nb066AlphaDummy011 x R) (SemanticCore.Class.cv (nb066AlphaDummy004 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy010 x R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy039 x R)) (SemanticCore.Class.cab (nb066AlphaDummy010 x R) (Compiler.CompactSourceSyntax.synWrex (nb066AlphaDummy011 x R) (SemanticCore.Class.cv (nb066AlphaDummy004 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb066AlphaDummy010 x R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb066_split_alpha_0004.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0002 (A R : SemanticCore.Class) : nb066AlphaDummy003 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0118 (A R : SemanticCore.Class) : nb066AlphaDummy003 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0003 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb066AlphaDummy005 x R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0119 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb066AlphaDummy005 x R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0004 (A R : SemanticCore.Class) : nb066AlphaDummy002 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0120 (A R : SemanticCore.Class) : nb066AlphaDummy002 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0005 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb066AlphaDummy004 x R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0121 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb066AlphaDummy004 x R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0006 (A R : SemanticCore.Class) : nb066AlphaDummy000 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0122 (A R : SemanticCore.Class) : nb066AlphaDummy000 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0123 (x : SemanticCore.Var) (R : SemanticCore.Class) (dv_R_x : x ∉ R.fv) : x ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0007 (A R : SemanticCore.Class) : nb066AlphaDummy001 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0124 (A R : SemanticCore.Class) : nb066AlphaDummy001 A R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0125 (y : SemanticCore.Var) (R : SemanticCore.Class) (dv_R_y : y ∉ R.fv) : y ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_compact_envfresh_0008 (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) : Nominal.TEnvFresh [(nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] R.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066WppRefl0008 (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) : Nominal.TReflOn [(nb066AlphaDummy003 A R, nb066AlphaDummy005 x R), (nb066AlphaDummy002 A R, nb066AlphaDummy004 x R), (nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] R.fv

Checked nominal proof certificate identified upstream as nb066_wpp_refl_0008.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066WppRefl0008 x y A R dv_R_x dv_R_y = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfQs (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCqs A R) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) R)))))

Checked nominal proof certificate identified upstream as nominal_df_qs.

Equations

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