Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part031.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0017 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(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 (nb077AlphaDummy057 F I)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy057 F I)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy058 x F)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy058 x F)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0017.

Equations

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

Certificates from NAR4C077C001Part032.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0018 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy023 F I, nb077AlphaDummy024 x F I), (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 (nb077AlphaDummy023 F I)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I)))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy024 x F I)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))))))))

Checked nominal proof certificate identified upstream as nb077_split_alpha_0018.

Equations

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

Certificates from NAR4C077C001Part033.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0019 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy020 F I, nb077AlphaDummy022 x F I), (nb077AlphaDummy019 F I, nb077AlphaDummy021 x F I), (nb077AlphaDummy049 F I, nb077AlphaDummy050 x F I), (nb077AlphaDummy023 F I, nb077AlphaDummy024 x F I), (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.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))

Checked nominal proof certificate identified upstream as nb077_split_alpha_0019.

Equations

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