Nominal proof certificates grouped in dependency order.
Certificates from NAR4C076C001Part006.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076SplitAlpha0000
(g m n a b : SemanticCore.Var)
(dv_m_n : m ≠ n)
:
Nominal.TAlphaWff
[(nb076AlphaDummy023, nb076AlphaDummy024 m n), (nb076AlphaDummy021, nb076AlphaDummy022 m n), (nb076AlphaDummy010, nb076AlphaDummy012 g m n a b), (nb076AlphaDummy009, nb076AlphaDummy011 g m n a b), (nb076AlphaDummy015, nb076AlphaDummy016 g m n a b), (nb076AlphaDummy013, nb076AlphaDummy014 g m n a b), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy023)
(SemanticCore.Class.cab nb076AlphaDummy017
(Compiler.CompactSourceSyntax.synWrex nb076AlphaDummy018 (SemanticCore.Class.cv nb076AlphaDummy003)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy017)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy018)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy023)
(SemanticCore.Class.cab nb076AlphaDummy017
(Compiler.CompactSourceSyntax.synWrex nb076AlphaDummy018 (SemanticCore.Class.cv nb076AlphaDummy003)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy017)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy018)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy024 m n))
(SemanticCore.Class.cab (nb076AlphaDummy019 m n)
(Compiler.CompactSourceSyntax.synWrex (nb076AlphaDummy020 m n) (SemanticCore.Class.cv m)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb076AlphaDummy019 m n))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy020 m n))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy024 m n))
(SemanticCore.Class.cab (nb076AlphaDummy019 m n)
(Compiler.CompactSourceSyntax.synWrex (nb076AlphaDummy020 m n) (SemanticCore.Class.cv m)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb076AlphaDummy019 m n))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy020 m n))))))).neg)
Checked nominal proof certificate identified upstream as nb076_split_alpha_0000.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C076C001Part007.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076SplitAlpha0001
(g m n a b : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb076AlphaDummy049, nb076AlphaDummy050 m n), (nb076AlphaDummy018, nb076AlphaDummy020 m n), (nb076AlphaDummy017, nb076AlphaDummy019 m n), (nb076AlphaDummy047, nb076AlphaDummy048 m n), (nb076AlphaDummy021, nb076AlphaDummy022 m n), (nb076AlphaDummy010, nb076AlphaDummy012 g m n a b), (nb076AlphaDummy009, nb076AlphaDummy011 g m n a b), (nb076AlphaDummy015, nb076AlphaDummy016 g m n a b), (nb076AlphaDummy013, nb076AlphaDummy014 g m n a b), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy049)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy018)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy049)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy050 m n))
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy020 m n))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy050 m n))
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb076_split_alpha_0001.
Equations
- One or more equations did not get rendered due to their size.