Nominal proof certificates grouped in dependency order.
Certificates from NAR4C068C001Part043.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0108
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy450, nb068AlphaDummy452 f), (nb068AlphaDummy449, nb068AlphaDummy451 f), (nb068AlphaDummy479, nb068AlphaDummy480 f), (nb068AlphaDummy453, nb068AlphaDummy454 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy450) (SemanticCore.Class.cv nb068AlphaDummy407))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy452 f))
(SemanticCore.Class.cv (nb068AlphaDummy409 f)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg
Checked nominal proof certificate identified upstream as nb068_split_alpha_0108.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0109
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146)
(SemanticCore.Class.cv nb068AlphaDummy147))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146)
(SemanticCore.Class.cv nb068AlphaDummy147))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f))
(SemanticCore.Class.cv (nb068AlphaDummy150 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f))
(SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0109.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0110
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139)
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139)
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143) (SemanticCore.Class.cv nb068AlphaDummy139))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc).neg))
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f))
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f))
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f))
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f))
(SemanticCore.Class.cv (nb068AlphaDummy141 f)))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f))
Compiler.CompactSourceSyntax.synCnnc).neg))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0110.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C068C001Part044.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0111
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146)
(SemanticCore.Class.cv nb068AlphaDummy147))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146)
(SemanticCore.Class.cv nb068AlphaDummy147))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f))
(SemanticCore.Class.cv (nb068AlphaDummy150 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f))
(SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0111.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0112
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139)
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139)
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143) (SemanticCore.Class.cv nb068AlphaDummy139))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc).neg))
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f))
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f))
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f))
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f))
(SemanticCore.Class.cv (nb068AlphaDummy141 f)))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f))
Compiler.CompactSourceSyntax.synCnnc).neg))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0112.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0113
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161)
(SemanticCore.Class.cab nb068AlphaDummy131
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f))
(SemanticCore.Class.cab (nb068AlphaDummy133 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0113.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0114
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy135)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb068AlphaDummy131
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy125)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy135)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb068AlphaDummy131
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy136 f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb068AlphaDummy133 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy136 f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb068AlphaDummy133 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0114.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C068C001Part045.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0115
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182)
(SemanticCore.Class.cv nb068AlphaDummy183))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182)
(SemanticCore.Class.cv nb068AlphaDummy183))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f))
(SemanticCore.Class.cv (nb068AlphaDummy186 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f))
(SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0115.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0116
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175)
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175)
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179) (SemanticCore.Class.cv nb068AlphaDummy175))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc).neg))
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f))
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f))
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f))
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f))
(SemanticCore.Class.cv (nb068AlphaDummy177 f)))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f))
Compiler.CompactSourceSyntax.synCnnc).neg))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0116.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0117
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182)
(SemanticCore.Class.cv nb068AlphaDummy183))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182)
(SemanticCore.Class.cv nb068AlphaDummy183))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f))
(SemanticCore.Class.cv (nb068AlphaDummy186 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f))
(SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0117.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0118
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175)
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175)
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179) (SemanticCore.Class.cv nb068AlphaDummy175))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc).neg))
((Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f))
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f))
Compiler.CompactSourceSyntax.synC1c))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f))
Compiler.CompactSourceSyntax.synCnnc)).neg.imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f))
(SemanticCore.Class.cv (nb068AlphaDummy177 f)))
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f))
Compiler.CompactSourceSyntax.synCnnc).neg))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0118.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C068C001Part046.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0119
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy168) (SemanticCore.Class.cv nb068AlphaDummy125)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy170 f))
(SemanticCore.Class.cv (nb068AlphaDummy127 f))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0119.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0120
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy171)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb068AlphaDummy167
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy126)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy171)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb068AlphaDummy167
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy172 f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb068AlphaDummy169 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy172 f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb068AlphaDummy169 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0120.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0121
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
(SemanticCore.Wff.classMem
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy408)
(SemanticCore.Class.cv nb068AlphaDummy407))
(Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)))
(SemanticCore.Wff.classMem
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy410 f))
(SemanticCore.Class.cv (nb068AlphaDummy409 f)))
(Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0121.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0122
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy411)
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy407)
(SemanticCore.Class.cv nb068AlphaDummy408))).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy408)
(Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))
(SemanticCore.Class.cv nb068AlphaDummy407)).neg)
((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy412 f))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy409 f))
(SemanticCore.Class.cv (nb068AlphaDummy410 f)))).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy410 f))
(Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))
(SemanticCore.Class.cv (nb068AlphaDummy409 f))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0122.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0123
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy501, nb068AlphaDummy504 f), (nb068AlphaDummy500, nb068AlphaDummy503 f), (nb068AlphaDummy499, nb068AlphaDummy502 f), (nb068AlphaDummy497, nb068AlphaDummy498 f), (nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy491, nb068AlphaDummy492 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy500)
(SemanticCore.Class.cv nb068AlphaDummy501))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy499)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy500)
(SemanticCore.Class.cv nb068AlphaDummy501))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy503 f))
(SemanticCore.Class.cv (nb068AlphaDummy504 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy502 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy503 f))
(SemanticCore.Class.cv (nb068AlphaDummy504 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0123.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C068C001Part047.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0124
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy491, nb068AlphaDummy492 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) (SemanticCore.Class.cv nb068AlphaDummy486)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy494)
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy493)
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv nb068AlphaDummy493))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f))
(SemanticCore.Class.cv (nb068AlphaDummy488 f))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy496 f))
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f))
Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy495 f))
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv (nb068AlphaDummy495 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0124.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0125
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy501, nb068AlphaDummy504 f), (nb068AlphaDummy500, nb068AlphaDummy503 f), (nb068AlphaDummy499, nb068AlphaDummy502 f), (nb068AlphaDummy497, nb068AlphaDummy498 f), (nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy519, nb068AlphaDummy520 f), (nb068AlphaDummy517, nb068AlphaDummy518 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy515, nb068AlphaDummy516 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy500)
(SemanticCore.Class.cv nb068AlphaDummy501))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy499)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy500)
(SemanticCore.Class.cv nb068AlphaDummy501))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy503 f))
(SemanticCore.Class.cv (nb068AlphaDummy504 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy502 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy503 f))
(SemanticCore.Class.cv (nb068AlphaDummy504 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0125.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0126
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy519, nb068AlphaDummy520 f), (nb068AlphaDummy517, nb068AlphaDummy518 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy515, nb068AlphaDummy516 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) (SemanticCore.Class.cv nb068AlphaDummy486)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy494)
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy493)
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv nb068AlphaDummy493))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f))
(SemanticCore.Class.cv (nb068AlphaDummy488 f))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy496 f))
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f))
Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy495 f))
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv (nb068AlphaDummy495 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0126.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0127
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy515, nb068AlphaDummy516 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy515)
(SemanticCore.Class.cab nb068AlphaDummy485
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy486 (SemanticCore.Class.cv nb068AlphaDummy328)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy515)
(SemanticCore.Class.cab nb068AlphaDummy485
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy486 (SemanticCore.Class.cv nb068AlphaDummy328)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy516 f))
(SemanticCore.Class.cab (nb068AlphaDummy487 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy488 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy516 f))
(SemanticCore.Class.cab (nb068AlphaDummy487 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy488 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0127.
Equations
- One or more equations did not get rendered due to their size.