Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block004

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part013.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0000 (x y f : SemanticCore.Var) :
Nominal.TAlphaWff [(nb068AlphaDummy021, nb068AlphaDummy024 x y), (nb068AlphaDummy020, nb068AlphaDummy023 x y), (nb068AlphaDummy019, nb068AlphaDummy022 x y), (nb068AlphaDummy017, nb068AlphaDummy018 x y), (nb068AlphaDummy013, nb068AlphaDummy015 x y), (nb068AlphaDummy014, nb068AlphaDummy016 x y), (nb068AlphaDummy006, nb068AlphaDummy008 x y), (nb068AlphaDummy005, nb068AlphaDummy007 x y), (nb068AlphaDummy011, nb068AlphaDummy012 x y), (nb068AlphaDummy009, nb068AlphaDummy010 x y), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy019) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy022 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0000.

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

    Certificates from NAR4C068C001Part014.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0001 (x y f : SemanticCore.Var) (dv_x_y : x ≠ y) :
    Nominal.TAlphaWff [(nb068AlphaDummy006, nb068AlphaDummy008 x y), (nb068AlphaDummy005, nb068AlphaDummy007 x y), (nb068AlphaDummy011, nb068AlphaDummy012 x y), (nb068AlphaDummy009, nb068AlphaDummy010 x y), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy006) (SemanticCore.Class.cv nb068AlphaDummy001)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy008 x y)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y)))).neg)

    Checked nominal proof certificate identified upstream as nb068_split_alpha_0001.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0002 (x y f : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb068AlphaDummy021, nb068AlphaDummy024 x y), (nb068AlphaDummy020, nb068AlphaDummy023 x y), (nb068AlphaDummy019, nb068AlphaDummy022 x y), (nb068AlphaDummy017, nb068AlphaDummy018 x y), (nb068AlphaDummy013, nb068AlphaDummy015 x y), (nb068AlphaDummy014, nb068AlphaDummy016 x y), (nb068AlphaDummy039, nb068AlphaDummy040 x y), (nb068AlphaDummy037, nb068AlphaDummy038 x y), (nb068AlphaDummy006, nb068AlphaDummy008 x y), (nb068AlphaDummy005, nb068AlphaDummy007 x y), (nb068AlphaDummy035, nb068AlphaDummy036 x y), (nb068AlphaDummy009, nb068AlphaDummy010 x y), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy019) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy022 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y)))).neg)

      Checked nominal proof certificate identified upstream as nb068_split_alpha_0002.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0003 (x y f : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb068AlphaDummy039, nb068AlphaDummy040 x y), (nb068AlphaDummy037, nb068AlphaDummy038 x y), (nb068AlphaDummy006, nb068AlphaDummy008 x y), (nb068AlphaDummy005, nb068AlphaDummy007 x y), (nb068AlphaDummy035, nb068AlphaDummy036 x y), (nb068AlphaDummy009, nb068AlphaDummy010 x y), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy039) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy039) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy040 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy040 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y)))).neg)

        Checked nominal proof certificate identified upstream as nb068_split_alpha_0003.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0004 (x y f : SemanticCore.Var) (dv_x_y : x ≠ y) :
          Nominal.TAlphaWff [(nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy003) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy001) (SemanticCore.Class.cv nb068AlphaDummy002))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy004 x y f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))

          Checked nominal proof certificate identified upstream as nb068_split_alpha_0004.

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