NF weak partition development: NAR4H5C096M3Part002.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0000
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb096AlphaDummy035 D R, nb096AlphaDummy036 D R q), (nb096AlphaDummy009 D R, nb096AlphaDummy010 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)]
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy035 D R))
(SemanticCore.Class.cab (nb096AlphaDummy005 D R)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy006 D R) (SemanticCore.Class.cv (nb096AlphaDummy001 D R))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy005 D R))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy006 D R)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy036 D R q))
(SemanticCore.Class.cab (nb096AlphaDummy007 D R q)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy008 D R q)
(SemanticCore.Class.cv (nb096AlphaDummy002 D R q))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy007 D R q))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy008 D R q)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg
Checked nominal proof certificate identified upstream as nb096_split_alpha_0000.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0001
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb096AlphaDummy035 D R, nb096AlphaDummy036 D R q), (nb096AlphaDummy009 D R, nb096AlphaDummy010 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy035 D R))
(SemanticCore.Class.cab (nb096AlphaDummy005 D R)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy006 D R)
(SemanticCore.Class.cv (nb096AlphaDummy001 D R))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy005 D R))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy006 D R)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy035 D R))
(SemanticCore.Class.cab (nb096AlphaDummy005 D R)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy006 D R)
(SemanticCore.Class.cv (nb096AlphaDummy001 D R))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy005 D R))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy006 D R)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy036 D R q))
(SemanticCore.Class.cab (nb096AlphaDummy007 D R q)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy008 D R q)
(SemanticCore.Class.cv (nb096AlphaDummy002 D R q))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy007 D R q))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy008 D R q)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy036 D R q))
(SemanticCore.Class.cab (nb096AlphaDummy007 D R q)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy008 D R q)
(SemanticCore.Class.cv (nb096AlphaDummy002 D R q))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy007 D R q))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy008 D R q)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
Checked nominal proof certificate identified upstream as nb096_split_alpha_0001.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0002
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)]
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy003 D R))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb096AlphaDummy000 D R))
(SemanticCore.Class.cv (nb096AlphaDummy001 D R))))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy004 D R q))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv q) (SemanticCore.Class.cv (nb096AlphaDummy002 D R q))))
Checked nominal proof certificate identified upstream as nb096_split_alpha_0002.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0001
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
nb096AlphaDummy002 D R q ∉ D.fv
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0109
(D : SemanticCore.Class)
(q : SemanticCore.Var)
(dv_D_q : q ∉ D.fv)
:
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0004
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
nb096AlphaDummy004 D R q ∉ D.fv
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_compact_envfresh_0007
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
(dv_D_q : q ∉ D.fv)
: