Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part020.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0008 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy189 F I, nb077AlphaDummy190 x), (nb077AlphaDummy187 F I, nb077AlphaDummy188 x), (nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy189 F I)) (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy189 F I)) (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy190 x)) (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy190 x)) (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))))))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0008.

Equations

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

Certificates from NAR4C077C001Part021.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0009 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy217 F I, nb077AlphaDummy218 x), (nb077AlphaDummy215 F I, nb077AlphaDummy216 x), (nb077AlphaDummy184 F I, nb077AlphaDummy186 x), (nb077AlphaDummy183 F I, nb077AlphaDummy185 x), (nb077AlphaDummy213 F I, nb077AlphaDummy214 x), (nb077AlphaDummy187 F I, nb077AlphaDummy188 x), (nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy217 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy217 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy218 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy218 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x)))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0009.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0556 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0557 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0558 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0559 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0560 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0561 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0562 (F I : SemanticCore.Class) : nb077AlphaDummy145 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0563 (x : SemanticCore.Var) : nb077AlphaDummy146 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0564 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0565 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0566 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0567 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0568 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0569 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0570 (F I : SemanticCore.Class) : nb077AlphaDummy065 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0571 (x : SemanticCore.Var) : nb077AlphaDummy066 x ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0572 (F I : SemanticCore.Class) : nb077AlphaDummy057 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0573 (x : SemanticCore.Var) (F : SemanticCore.Class) : nb077AlphaDummy058 x F ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0574 (F I : SemanticCore.Class) : nb077AlphaDummy055 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0575 (x : SemanticCore.Var) (F : SemanticCore.Class) : nb077AlphaDummy056 x F ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0576 (F I : SemanticCore.Class) : nb077AlphaDummy016 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0577 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy018 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0578 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0579 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0580 (F I : SemanticCore.Class) : nb077AlphaDummy013 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0581 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy014 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0582 (F I : SemanticCore.Class) : nb077AlphaDummy011 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0583 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy012 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0584 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0585 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0586 (F I : SemanticCore.Class) : nb077AlphaDummy004 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0587 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy006 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0588 (F I : SemanticCore.Class) : nb077AlphaDummy003 F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0589 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy005 x F I ∉ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_envfresh_0037 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TEnvFresh [(nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] Compiler.CompactSourceSyntax.synC1st.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0037 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TReflOn [(nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] Compiler.CompactSourceSyntax.synC1st.fv

Checked nominal proof certificate identified upstream as nb077_wpp_refl_0037.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0037 x F I = ⋯.reflOn