Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part040.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0026 (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), (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_0026.

Equations

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

Certificates from NAR4C077C001Part041.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0027 (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), (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_0027.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_envfresh_0099 (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), (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.nb077WppRefl0099 (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), (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_0099.

Equations

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