Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part022.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0010 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy225 F I, nb077AlphaDummy226 x), (nb077AlphaDummy223 F I, nb077AlphaDummy224 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 (nb077AlphaDummy225 F I)) (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy225 F I)) (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy226 x)) (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy226 x)) (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))))))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0010.

Equations

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

Certificates from NAR4C077C001Part023.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0011 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy253 F I, nb077AlphaDummy254 x), (nb077AlphaDummy251 F I, nb077AlphaDummy252 x), (nb077AlphaDummy220 F I, nb077AlphaDummy222 x), (nb077AlphaDummy219 F I, nb077AlphaDummy221 x), (nb077AlphaDummy249 F I, nb077AlphaDummy250 x), (nb077AlphaDummy223 F I, nb077AlphaDummy224 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 (nb077AlphaDummy253 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy253 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy254 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy254 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0011.

Equations

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