Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C059C001Block001

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C059C001Part002.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059WppRefl0001 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) :
Nominal.TReflOn [(nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] S_cls.fv

Checked nominal proof certificate identified upstream as nb059_wpp_refl_0001.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0000 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb059AlphaDummy033 R S_cls, nb059AlphaDummy036 R a), (nb059AlphaDummy032 R S_cls, nb059AlphaDummy035 R a), (nb059AlphaDummy031 R S_cls, nb059AlphaDummy034 R a), (nb059AlphaDummy029 R S_cls, nb059AlphaDummy030 R a), (nb059AlphaDummy025 R S_cls, nb059AlphaDummy027 R a), (nb059AlphaDummy026 R S_cls, nb059AlphaDummy028 R a), (nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy023 R S_cls, nb059AlphaDummy024 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy011 R S_cls, nb059AlphaDummy012 R a), (nb059AlphaDummy009 R S_cls, nb059AlphaDummy010 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy031 R S_cls)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb059AlphaDummy035 R a)) (SemanticCore.Class.cv (nb059AlphaDummy036 R a))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy034 R a)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb059AlphaDummy035 R a)) (SemanticCore.Class.cv (nb059AlphaDummy036 R a)))).neg)

    Checked nominal proof certificate identified upstream as nb059_split_alpha_0000.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Certificates from NAR4C059C001Part003.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0001 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy023 R S_cls, nb059AlphaDummy024 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy011 R S_cls, nb059AlphaDummy012 R a), (nb059AlphaDummy009 R S_cls, nb059AlphaDummy010 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))))

      Checked nominal proof certificate identified upstream as nb059_split_alpha_0001.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0002 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb059AlphaDummy033 R S_cls, nb059AlphaDummy036 R a), (nb059AlphaDummy032 R S_cls, nb059AlphaDummy035 R a), (nb059AlphaDummy031 R S_cls, nb059AlphaDummy034 R a), (nb059AlphaDummy029 R S_cls, nb059AlphaDummy030 R a), (nb059AlphaDummy025 R S_cls, nb059AlphaDummy027 R a), (nb059AlphaDummy026 R S_cls, nb059AlphaDummy028 R a), (nb059AlphaDummy051 R S_cls, nb059AlphaDummy052 R a), (nb059AlphaDummy049 R S_cls, nb059AlphaDummy050 R a), (nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy047 R S_cls, nb059AlphaDummy048 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy011 R S_cls, nb059AlphaDummy012 R a), (nb059AlphaDummy009 R S_cls, nb059AlphaDummy010 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy031 R S_cls)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb059AlphaDummy035 R a)) (SemanticCore.Class.cv (nb059AlphaDummy036 R a))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy034 R a)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb059AlphaDummy035 R a)) (SemanticCore.Class.cv (nb059AlphaDummy036 R a)))).neg)

        Checked nominal proof certificate identified upstream as nb059_split_alpha_0002.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0003 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb059AlphaDummy025 R S_cls, nb059AlphaDummy027 R a), (nb059AlphaDummy026 R S_cls, nb059AlphaDummy028 R a), (nb059AlphaDummy051 R S_cls, nb059AlphaDummy052 R a), (nb059AlphaDummy049 R S_cls, nb059AlphaDummy050 R a), (nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy047 R S_cls, nb059AlphaDummy048 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy011 R S_cls, nb059AlphaDummy012 R a), (nb059AlphaDummy009 R S_cls, nb059AlphaDummy010 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy026 R S_cls)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy027 R a)) (SemanticCore.Class.cv (nb059AlphaDummy020 R a))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy028 R a)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy027 R a)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb059AlphaDummy027 R a)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb059AlphaDummy027 R a)))).neg)

          Checked nominal proof certificate identified upstream as nb059_split_alpha_0003.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For