Nominal proof certificates grouped in dependency order.

Certificates from NAR4C057C001Part025.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0065 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy146, nb057AlphaDummy149 f), (nb057AlphaDummy145, nb057AlphaDummy148 f), (nb057AlphaDummy144, nb057AlphaDummy147 f), (nb057AlphaDummy142, nb057AlphaDummy143 f), (nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy136, nb057AlphaDummy137 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy144) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy147 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0065.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0066 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy136, nb057AlphaDummy137 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))))

Checked nominal proof certificate identified upstream as nb057_split_alpha_0066.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0067 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy146, nb057AlphaDummy149 f), (nb057AlphaDummy145, nb057AlphaDummy148 f), (nb057AlphaDummy144, nb057AlphaDummy147 f), (nb057AlphaDummy142, nb057AlphaDummy143 f), (nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy164, nb057AlphaDummy165 f), (nb057AlphaDummy162, nb057AlphaDummy163 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy160, nb057AlphaDummy161 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy144) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy147 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0067.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0068 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy164, nb057AlphaDummy165 f), (nb057AlphaDummy162, nb057AlphaDummy163 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy160, nb057AlphaDummy161 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy138) (SemanticCore.Class.cv nb057AlphaDummy131)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy139) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy138))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy140 f)) (SemanticCore.Class.cv (nb057AlphaDummy133 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy141 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy140 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0068.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0069 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy160, nb057AlphaDummy161 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy160) (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy160) (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy161 f)) (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy161 f)) (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0069.

Equations

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

Certificates from NAR4C057C001Part026.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0070 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy182, nb057AlphaDummy185 f), (nb057AlphaDummy181, nb057AlphaDummy184 f), (nb057AlphaDummy180, nb057AlphaDummy183 f), (nb057AlphaDummy178, nb057AlphaDummy179 f), (nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy172, nb057AlphaDummy173 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy180) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy183 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0070.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0071 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy172, nb057AlphaDummy173 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))))

Checked nominal proof certificate identified upstream as nb057_split_alpha_0071.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0072 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy182, nb057AlphaDummy185 f), (nb057AlphaDummy181, nb057AlphaDummy184 f), (nb057AlphaDummy180, nb057AlphaDummy183 f), (nb057AlphaDummy178, nb057AlphaDummy179 f), (nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy200, nb057AlphaDummy201 f), (nb057AlphaDummy198, nb057AlphaDummy199 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy196, nb057AlphaDummy197 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy180) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy183 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0072.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0073 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy200, nb057AlphaDummy201 f), (nb057AlphaDummy198, nb057AlphaDummy199 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy196, nb057AlphaDummy197 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy174) (SemanticCore.Class.cv nb057AlphaDummy167)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy175) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy174))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy176 f)) (SemanticCore.Class.cv (nb057AlphaDummy169 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy177 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy176 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0073.

Equations

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

Certificates from NAR4C057C001Part027.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0074 (f a : SemanticCore.Var) : Nominal.TAlphaWff [(nb057AlphaDummy196, nb057AlphaDummy197 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy196) (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy196) (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy197 f)) (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy197 f)) (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0074.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057FinalCompositionVariableOccurrence (f a : SemanticCore.Var) (dv_a_f : a ≠ f) : Nominal.TAlphaClass [(nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv f)

Checked nominal proof certificate identified upstream as nb057_final_composition_variable_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0075 (f a : SemanticCore.Var) (dv_a_f : a ≠ f) : Nominal.TAlphaWff [(nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy128) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Class.cv nb057AlphaDummy125))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy124)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Class.cv (nb057AlphaDummy127 f)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy126 f))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0075.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057FinalPairBinderOccurrence (f a : SemanticCore.Var) : Nominal.TAlphaClass [(nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Class.cv nb057AlphaDummy050) (SemanticCore.Class.cv (nb057AlphaDummy051 f))

Checked nominal proof certificate identified upstream as nb057_final_pair_binder_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0076 (f a : SemanticCore.Var) (dv_a_f : a ≠ f) : Nominal.TAlphaWff [(nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv nb057AlphaDummy001)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv nb057AlphaDummy001)) (SemanticCore.Class.cv nb057AlphaDummy000)).neg) ((Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (SemanticCore.Class.cv a)).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0076.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFns (f a : SemanticCore.Var) (dv_a_f : a ≠ f) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCfns (Compiler.CompactSourceSyntax.synCopab f a (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv f) (SemanticCore.Class.cv a))))

Checked nominal proof certificate identified upstream as nominal_df_fns.

Equations

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