NF weak partition development: NAR4C078C001Part059.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0028
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb078AlphaDummy248, nb078AlphaDummy250 f), (nb078AlphaDummy247, nb078AlphaDummy249 f), (nb078AlphaDummy277, nb078AlphaDummy278 f), (nb078AlphaDummy251, nb078AlphaDummy252 f), (nb078AlphaDummy244, nb078AlphaDummy246 f), (nb078AlphaDummy243, nb078AlphaDummy245 f), (nb078AlphaDummy000, f), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy248) (SemanticCore.Class.cv nb078AlphaDummy243)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy250 f))
(SemanticCore.Class.cv (nb078AlphaDummy245 f))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb078_split_alpha_0028.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0029
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb078AlphaDummy251, nb078AlphaDummy252 f), (nb078AlphaDummy244, nb078AlphaDummy246 f), (nb078AlphaDummy243, nb078AlphaDummy245 f), (nb078AlphaDummy000, f), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy251)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb078AlphaDummy247
(Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy244)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy251)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb078AlphaDummy247
(Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy243)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy252 f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb078AlphaDummy249 f)
(Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy246 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f)))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy252 f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb078AlphaDummy249 f)
(Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy245 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
Checked nominal proof certificate identified upstream as nb078_split_alpha_0029.
Equations
- One or more equations did not get rendered due to their size.