NF weak partition development: NAR4H5C096M3Part004.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0005
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb096AlphaDummy102 D R, nb096AlphaDummy104 D R q), (nb096AlphaDummy101 D R, nb096AlphaDummy103 D R q), (nb096AlphaDummy131 D R, nb096AlphaDummy132 D R q), (nb096AlphaDummy105 D R, nb096AlphaDummy106 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 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 (nb096AlphaDummy102 D R))
(SemanticCore.Class.cv (nb096AlphaDummy041 D R))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy101 D R))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy102 D R)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy104 D R q))
(SemanticCore.Class.cv (nb096AlphaDummy043 D R q))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy103 D R q))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy104 D R q)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb096_split_alpha_0005.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0006
(D R : SemanticCore.Class)
(q : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb096AlphaDummy105 D R, nb096AlphaDummy106 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 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 (nb096AlphaDummy105 D R))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb096AlphaDummy101 D R)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy102 D R)
(SemanticCore.Class.cv (nb096AlphaDummy042 D R))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy101 D R))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy102 D R)))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy105 D R))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb096AlphaDummy101 D R)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy102 D R)
(SemanticCore.Class.cv (nb096AlphaDummy041 D R))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy101 D R))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy102 D R)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy106 D R q))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb096AlphaDummy103 D R q)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy104 D R q)
(SemanticCore.Class.cv (nb096AlphaDummy044 D R q))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy103 D R q))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy104 D R q)))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy106 D R q))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb096AlphaDummy103 D R q)
(Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy104 D R q)
(SemanticCore.Class.cv (nb096AlphaDummy043 D R q))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy103 D R q))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy104 D R q)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
Checked nominal proof certificate identified upstream as nb096_split_alpha_0006.
Equations
- One or more equations did not get rendered due to their size.