Nominal proof certificates grouped in dependency order.
Certificates from NAR4C057C001Part007.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0000
(f a : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb057AlphaDummy020, nb057AlphaDummy023 f a), (nb057AlphaDummy019, nb057AlphaDummy022 f a), (nb057AlphaDummy018, nb057AlphaDummy021 f a), (nb057AlphaDummy016, nb057AlphaDummy017 f a), (nb057AlphaDummy012, nb057AlphaDummy014 f a), (nb057AlphaDummy013, nb057AlphaDummy015 f a), (nb057AlphaDummy005, nb057AlphaDummy007 f a), (nb057AlphaDummy004, nb057AlphaDummy006 f a), (nb057AlphaDummy010, nb057AlphaDummy011 f a), (nb057AlphaDummy008, nb057AlphaDummy009 f a), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy019)
(SemanticCore.Class.cv nb057AlphaDummy020))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy018)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy019)
(SemanticCore.Class.cv nb057AlphaDummy020))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy022 f a))
(SemanticCore.Class.cv (nb057AlphaDummy023 f a)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy021 f a))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy022 f a))
(SemanticCore.Class.cv (nb057AlphaDummy023 f a)))).neg)
Checked nominal proof certificate identified upstream as nb057_split_alpha_0000.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C057C001Part008.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0001
(f a : SemanticCore.Var)
(dv_a_f : a ≠ f)
:
Nominal.TAlphaWff
[(nb057AlphaDummy005, nb057AlphaDummy007 f a), (nb057AlphaDummy004, nb057AlphaDummy006 f a), (nb057AlphaDummy010, nb057AlphaDummy011 f a), (nb057AlphaDummy008, nb057AlphaDummy009 f a), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy005) (SemanticCore.Class.cv nb057AlphaDummy001)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy007 f a)) (SemanticCore.Class.cv f)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a)))).neg)
Checked nominal proof certificate identified upstream as nb057_split_alpha_0001.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0002
(f a : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb057AlphaDummy020, nb057AlphaDummy023 f a), (nb057AlphaDummy019, nb057AlphaDummy022 f a), (nb057AlphaDummy018, nb057AlphaDummy021 f a), (nb057AlphaDummy016, nb057AlphaDummy017 f a), (nb057AlphaDummy012, nb057AlphaDummy014 f a), (nb057AlphaDummy013, nb057AlphaDummy015 f a), (nb057AlphaDummy038, nb057AlphaDummy039 f a), (nb057AlphaDummy036, nb057AlphaDummy037 f a), (nb057AlphaDummy005, nb057AlphaDummy007 f a), (nb057AlphaDummy004, nb057AlphaDummy006 f a), (nb057AlphaDummy034, nb057AlphaDummy035 f a), (nb057AlphaDummy008, nb057AlphaDummy009 f a), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy019)
(SemanticCore.Class.cv nb057AlphaDummy020))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy018)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy019)
(SemanticCore.Class.cv nb057AlphaDummy020))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy022 f a))
(SemanticCore.Class.cv (nb057AlphaDummy023 f a)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy021 f a))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy022 f a))
(SemanticCore.Class.cv (nb057AlphaDummy023 f a)))).neg)
Checked nominal proof certificate identified upstream as nb057_split_alpha_0002.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0003
(f a : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb057AlphaDummy038, nb057AlphaDummy039 f a), (nb057AlphaDummy036, nb057AlphaDummy037 f a), (nb057AlphaDummy005, nb057AlphaDummy007 f a), (nb057AlphaDummy004, nb057AlphaDummy006 f a), (nb057AlphaDummy034, nb057AlphaDummy035 f a), (nb057AlphaDummy008, nb057AlphaDummy009 f a), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy038)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy038)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy039 f a))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy039 f a))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a)))).neg)
Checked nominal proof certificate identified upstream as nb057_split_alpha_0003.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057OrderedPairBinderOccurrence
(f a : SemanticCore.Var)
:
Checked nominal proof certificate identified upstream as
nb057_ordered_pair_binder_occurrence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0004
(f a : SemanticCore.Var)
(dv_a_f : a ≠ f)
:
Nominal.TAlphaWff [(nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)]
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy002)
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb057AlphaDummy001)
(SemanticCore.Class.cv nb057AlphaDummy000)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy003 f a))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv f) (SemanticCore.Class.cv a)))
Checked nominal proof certificate identified upstream as nb057_split_alpha_0004.
Equations
- One or more equations did not get rendered due to their size.