Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C069C001Block001

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C069C001Part002.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb069SplitAlpha0000 (x y a b : SemanticCore.Var) :
Nominal.TAlphaWff [(nb069AlphaDummy022, nb069AlphaDummy025 a b), (nb069AlphaDummy021, nb069AlphaDummy024 a b), (nb069AlphaDummy020, nb069AlphaDummy023 a b), (nb069AlphaDummy018, nb069AlphaDummy019 a b), (nb069AlphaDummy014, nb069AlphaDummy016 a b), (nb069AlphaDummy015, nb069AlphaDummy017 a b), (nb069AlphaDummy007, nb069AlphaDummy009 a b), (nb069AlphaDummy006, nb069AlphaDummy008 a b), (nb069AlphaDummy012, nb069AlphaDummy013 a b), (nb069AlphaDummy010, nb069AlphaDummy011 a b), (nb069AlphaDummy001, b), (nb069AlphaDummy000, a), (nb069AlphaDummy004, nb069AlphaDummy005 x y a b)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb069AlphaDummy021) (SemanticCore.Class.cv nb069AlphaDummy022)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb069AlphaDummy020) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb069AlphaDummy021) (SemanticCore.Class.cv nb069AlphaDummy022))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb069AlphaDummy024 a b)) (SemanticCore.Class.cv (nb069AlphaDummy025 a b))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb069AlphaDummy023 a b)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb069AlphaDummy024 a b)) (SemanticCore.Class.cv (nb069AlphaDummy025 a b)))).neg)

Checked nominal proof certificate identified upstream as nb069_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb069SplitAlpha0001 (x y a b : SemanticCore.Var) (dv_a_b : a ≠ b) :
    Nominal.TAlphaWff [(nb069AlphaDummy007, nb069AlphaDummy009 a b), (nb069AlphaDummy006, nb069AlphaDummy008 a b), (nb069AlphaDummy012, nb069AlphaDummy013 a b), (nb069AlphaDummy010, nb069AlphaDummy011 a b), (nb069AlphaDummy001, b), (nb069AlphaDummy000, a), (nb069AlphaDummy004, nb069AlphaDummy005 x y a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb069AlphaDummy007) (SemanticCore.Class.cv nb069AlphaDummy000)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb069AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb069AlphaDummy007))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb069AlphaDummy009 a b)) (SemanticCore.Class.cv a)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb069AlphaDummy008 a b)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb069AlphaDummy009 a b)))).neg)

    Checked nominal proof certificate identified upstream as nb069_split_alpha_0001.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb069SplitAlpha0002 (x y a b : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb069AlphaDummy022, nb069AlphaDummy025 a b), (nb069AlphaDummy021, nb069AlphaDummy024 a b), (nb069AlphaDummy020, nb069AlphaDummy023 a b), (nb069AlphaDummy018, nb069AlphaDummy019 a b), (nb069AlphaDummy014, nb069AlphaDummy016 a b), (nb069AlphaDummy015, nb069AlphaDummy017 a b), (nb069AlphaDummy040, nb069AlphaDummy041 a b), (nb069AlphaDummy038, nb069AlphaDummy039 a b), (nb069AlphaDummy007, nb069AlphaDummy009 a b), (nb069AlphaDummy006, nb069AlphaDummy008 a b), (nb069AlphaDummy036, nb069AlphaDummy037 a b), (nb069AlphaDummy010, nb069AlphaDummy011 a b), (nb069AlphaDummy001, b), (nb069AlphaDummy000, a), (nb069AlphaDummy004, nb069AlphaDummy005 x y a b)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb069AlphaDummy021) (SemanticCore.Class.cv nb069AlphaDummy022)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb069AlphaDummy020) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb069AlphaDummy021) (SemanticCore.Class.cv nb069AlphaDummy022))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb069AlphaDummy024 a b)) (SemanticCore.Class.cv (nb069AlphaDummy025 a b))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb069AlphaDummy023 a b)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb069AlphaDummy024 a b)) (SemanticCore.Class.cv (nb069AlphaDummy025 a b)))).neg)

      Checked nominal proof certificate identified upstream as nb069_split_alpha_0002.

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

        Certificates from NAR4C069C001Part003.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb069SplitAlpha0003 (x y a b : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb069AlphaDummy040, nb069AlphaDummy041 a b), (nb069AlphaDummy038, nb069AlphaDummy039 a b), (nb069AlphaDummy007, nb069AlphaDummy009 a b), (nb069AlphaDummy006, nb069AlphaDummy008 a b), (nb069AlphaDummy036, nb069AlphaDummy037 a b), (nb069AlphaDummy010, nb069AlphaDummy011 a b), (nb069AlphaDummy001, b), (nb069AlphaDummy000, a), (nb069AlphaDummy004, nb069AlphaDummy005 x y a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb069AlphaDummy040) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb069AlphaDummy007))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb069AlphaDummy040) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb069AlphaDummy007))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb069AlphaDummy041 a b)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb069AlphaDummy009 a b)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb069AlphaDummy041 a b)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb069AlphaDummy009 a b)))).neg)

        Checked nominal proof certificate identified upstream as nb069_split_alpha_0003.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb069SplitAlpha0004 (x y a b : SemanticCore.Var) (dv_a_b : a ≠ b) :
          Nominal.TAlphaWff [(nb069AlphaDummy001, b), (nb069AlphaDummy000, a), (nb069AlphaDummy004, nb069AlphaDummy005 x y a b)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb069AlphaDummy004) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb069AlphaDummy000) (SemanticCore.Class.cv nb069AlphaDummy001))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb069AlphaDummy005 x y a b)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv a) (SemanticCore.Class.cv b)))

          Checked nominal proof certificate identified upstream as nb069_split_alpha_0004.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfLec (x y a b : SemanticCore.Var) (dv_a_b : a ≠ b) (dv_a_x : a ≠ x) (__dv_a_y : a ≠ y) (dv_b_x : b ≠ x) (dv_b_y : b ≠ y) (dv_x_y : x ≠ y) :
            Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCopab a b (Compiler.CompactSourceSyntax.synWrex x (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synWrex y (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

            Checked nominal proof certificate identified upstream as nominal_df_lec.

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