Nominal proof certificates grouped in dependency order.
Certificates from NAR4C067C001Part010.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0000
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy031, nb067AlphaDummy034 x y), (nb067AlphaDummy030, nb067AlphaDummy033 x y), (nb067AlphaDummy029, nb067AlphaDummy032 x y), (nb067AlphaDummy027, nb067AlphaDummy028 x y), (nb067AlphaDummy023, nb067AlphaDummy025 x y), (nb067AlphaDummy024, nb067AlphaDummy026 x y), (nb067AlphaDummy016, nb067AlphaDummy018 x y), (nb067AlphaDummy015, nb067AlphaDummy017 x y), (nb067AlphaDummy021, nb067AlphaDummy022 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy030)
(SemanticCore.Class.cv nb067AlphaDummy031))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy029)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy030)
(SemanticCore.Class.cv nb067AlphaDummy031))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy033 x y))
(SemanticCore.Class.cv (nb067AlphaDummy034 x y)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy032 x y))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy033 x y))
(SemanticCore.Class.cv (nb067AlphaDummy034 x y)))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0000.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0001
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy016, nb067AlphaDummy018 x y), (nb067AlphaDummy015, nb067AlphaDummy017 x y), (nb067AlphaDummy021, nb067AlphaDummy022 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))))
Checked nominal proof certificate identified upstream as nb067_split_alpha_0001.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0002
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy031, nb067AlphaDummy034 x y), (nb067AlphaDummy030, nb067AlphaDummy033 x y), (nb067AlphaDummy029, nb067AlphaDummy032 x y), (nb067AlphaDummy027, nb067AlphaDummy028 x y), (nb067AlphaDummy023, nb067AlphaDummy025 x y), (nb067AlphaDummy024, nb067AlphaDummy026 x y), (nb067AlphaDummy049, nb067AlphaDummy050 x y), (nb067AlphaDummy047, nb067AlphaDummy048 x y), (nb067AlphaDummy016, nb067AlphaDummy018 x y), (nb067AlphaDummy015, nb067AlphaDummy017 x y), (nb067AlphaDummy045, nb067AlphaDummy046 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy030)
(SemanticCore.Class.cv nb067AlphaDummy031))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy029)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy030)
(SemanticCore.Class.cv nb067AlphaDummy031))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy033 x y))
(SemanticCore.Class.cv (nb067AlphaDummy034 x y)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy032 x y))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy033 x y))
(SemanticCore.Class.cv (nb067AlphaDummy034 x y)))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0002.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C067C001Part011.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0003
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy023, nb067AlphaDummy025 x y), (nb067AlphaDummy024, nb067AlphaDummy026 x y), (nb067AlphaDummy049, nb067AlphaDummy050 x y), (nb067AlphaDummy047, nb067AlphaDummy048 x y), (nb067AlphaDummy016, nb067AlphaDummy018 x y), (nb067AlphaDummy015, nb067AlphaDummy017 x y), (nb067AlphaDummy045, nb067AlphaDummy046 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy023) (SemanticCore.Class.cv nb067AlphaDummy016)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy024)
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy023) Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy023)
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv nb067AlphaDummy023))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy025 x y))
(SemanticCore.Class.cv (nb067AlphaDummy018 x y))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy026 x y))
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy025 x y))
Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy025 x y))
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv (nb067AlphaDummy025 x y)))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0003.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SecondCoordinateOccurrence
(x y f : SemanticCore.Var)
:
Nominal.TAlphaClass
[(nb067AlphaDummy016, nb067AlphaDummy018 x y), (nb067AlphaDummy015, nb067AlphaDummy017 x y), (nb067AlphaDummy045, nb067AlphaDummy046 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
(SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv y)
Checked nominal proof certificate identified upstream as
nb067_second_coordinate_occurrence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0004
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy045, nb067AlphaDummy046 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy045)
(SemanticCore.Class.cab nb067AlphaDummy015
(Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy002)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy045)
(SemanticCore.Class.cab nb067AlphaDummy015
(Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy002)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy046 x y))
(SemanticCore.Class.cab (nb067AlphaDummy017 x y)
(Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv y)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy046 x y))
(SemanticCore.Class.cab (nb067AlphaDummy017 x y)
(Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv y)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0004.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0005
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy059, nb067AlphaDummy062 x y f), (nb067AlphaDummy058, nb067AlphaDummy061 x y f), (nb067AlphaDummy057, nb067AlphaDummy060 x y f), (nb067AlphaDummy055, nb067AlphaDummy056 x y f), (nb067AlphaDummy051, nb067AlphaDummy053 x y f), (nb067AlphaDummy052, nb067AlphaDummy054 x y f), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy058)
(SemanticCore.Class.cv nb067AlphaDummy059))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy057)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy058)
(SemanticCore.Class.cv nb067AlphaDummy059))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))
(SemanticCore.Class.cv (nb067AlphaDummy062 x y f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy060 x y f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))
(SemanticCore.Class.cv (nb067AlphaDummy062 x y f)))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0005.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067FirstCoordinateOccurrence
(x y f : SemanticCore.Var)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaClass
[(nb067AlphaDummy016, nb067AlphaDummy018 x y), (nb067AlphaDummy015, nb067AlphaDummy017 x y), (nb067AlphaDummy021, nb067AlphaDummy022 x y), (nb067AlphaDummy019, nb067AlphaDummy020 x y), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
(SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv x)
Checked nominal proof certificate identified upstream as
nb067_first_coordinate_occurrence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0006
(x y f : SemanticCore.Var)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff
[(nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy013, nb067AlphaDummy014 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy008)
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001)
(SemanticCore.Class.cv nb067AlphaDummy002))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0006.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C067C001Part012.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0007
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb067AlphaDummy059, nb067AlphaDummy062 x y f), (nb067AlphaDummy058, nb067AlphaDummy061 x y f), (nb067AlphaDummy057, nb067AlphaDummy060 x y f), (nb067AlphaDummy055, nb067AlphaDummy056 x y f), (nb067AlphaDummy051, nb067AlphaDummy053 x y f), (nb067AlphaDummy052, nb067AlphaDummy054 x y f), (nb067AlphaDummy077, nb067AlphaDummy078 x y f), (nb067AlphaDummy075, nb067AlphaDummy076 x y f), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy073, nb067AlphaDummy074 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy058)
(SemanticCore.Class.cv nb067AlphaDummy059))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy057)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy058)
(SemanticCore.Class.cv nb067AlphaDummy059))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))
(SemanticCore.Class.cv (nb067AlphaDummy062 x y f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy060 x y f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))
(SemanticCore.Class.cv (nb067AlphaDummy062 x y f)))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0007.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0008
(x y f : SemanticCore.Var)
:
Nominal.TAlphaClass
[(nb067AlphaDummy077, nb067AlphaDummy078 x y f), (nb067AlphaDummy075, nb067AlphaDummy076 x y f), (nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy073, nb067AlphaDummy074 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
(SemanticCore.Class.cab nb067AlphaDummy052
(Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy051 (SemanticCore.Class.cv nb067AlphaDummy008)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy052)
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy051) Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy051)
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv nb067AlphaDummy051)))))
(SemanticCore.Class.cab (nb067AlphaDummy054 x y f)
(Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy053 x y f) (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy054 x y f))
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy053 x y f))
Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy053 x y f))
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv (nb067AlphaDummy053 x y f))))))
Checked nominal proof certificate identified upstream as nb067_split_alpha_0008.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067FunctionGraphOccurrence
(x y f : SemanticCore.Var)
:
Nominal.TAlphaClass
[(nb067AlphaDummy008, nb067AlphaDummy010 x y f), (nb067AlphaDummy007, nb067AlphaDummy009 x y f), (nb067AlphaDummy073, nb067AlphaDummy074 x y f), (nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
(SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f))
Checked nominal proof certificate identified upstream as nb067_function_graph_occurrence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0009
(x y f : SemanticCore.Var)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff
[(nb067AlphaDummy011, nb067AlphaDummy012 x y f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy011)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb067AlphaDummy007
(Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001)
(SemanticCore.Class.cv nb067AlphaDummy002))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy011)
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab nb067AlphaDummy007
(Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (SemanticCore.Class.cv nb067AlphaDummy003)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy012 x y f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb067AlphaDummy009 x y f)
(Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f)
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy012 x y f))
(Compiler.CompactSourceSyntax.synCcompl
(SemanticCore.Class.cab (nb067AlphaDummy009 x y f)
(Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f)
(SemanticCore.Class.cv (nb067AlphaDummy004 x y f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)
Checked nominal proof certificate identified upstream as nb067_split_alpha_0009.
Equations
- One or more equations did not get rendered due to their size.