NF weak partition development: NAR4C077C001Part048.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0034 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy345 F I, nb077AlphaDummy346 x), (nb077AlphaDummy343 F I, nb077AlphaDummy344 x), (nb077AlphaDummy312 F I, nb077AlphaDummy314 x), (nb077AlphaDummy311 F I, nb077AlphaDummy313 x), (nb077AlphaDummy341 F I, nb077AlphaDummy342 x), (nb077AlphaDummy315 F I, nb077AlphaDummy316 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 (nb077AlphaDummy345 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy345 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy346 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy346 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x)))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0034.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_envfresh_0124 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TEnvFresh [(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.synCcnv Compiler.CompactSourceSyntax.synC1st).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0124 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TReflOn [(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.synCcnv Compiler.CompactSourceSyntax.synC1st).fv

Checked nominal proof certificate identified upstream as nb077_wpp_refl_0124.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_envfresh_0125 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TEnvFresh [(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.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd)).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0125 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TReflOn [(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.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd)).fv

Checked nominal proof certificate identified upstream as nb077_wpp_refl_0125.

Equations

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