Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C075C001Block002

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C075C001Part005.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb075SplitAlpha0002 (x : SemanticCore.Var) :
Nominal.TAlphaWff [(nb075AlphaDummy001, nb075AlphaDummy002 x), (nb075AlphaDummy000, x), (nb075AlphaDummy003, nb075AlphaDummy004 x)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy003) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb075AlphaDummy000) (SemanticCore.Class.cv nb075AlphaDummy001))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy004 x)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv (nb075AlphaDummy002 x))))

Checked nominal proof certificate identified upstream as nb075_split_alpha_0002.

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

    Certificates from NAR4C075C001Part006.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb075SplitAlpha0003 (x : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb075AlphaDummy046, nb075AlphaDummy048 x), (nb075AlphaDummy045, nb075AlphaDummy047 x), (nb075AlphaDummy075, nb075AlphaDummy076 x), (nb075AlphaDummy049, nb075AlphaDummy050 x), (nb075AlphaDummy042, nb075AlphaDummy044 x), (nb075AlphaDummy041, nb075AlphaDummy043 x), (nb075AlphaDummy001, nb075AlphaDummy002 x), (nb075AlphaDummy000, x), (nb075AlphaDummy003, nb075AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb075AlphaDummy046) (SemanticCore.Class.cv nb075AlphaDummy041)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy045) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb075AlphaDummy046)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb075AlphaDummy048 x)) (SemanticCore.Class.cv (nb075AlphaDummy043 x))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy047 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb075AlphaDummy048 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

    Checked nominal proof certificate identified upstream as nb075_split_alpha_0003.

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

      Certificates from NAR4C075C001Part007.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb075SplitAlpha0004 (x : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb075AlphaDummy049, nb075AlphaDummy050 x), (nb075AlphaDummy042, nb075AlphaDummy044 x), (nb075AlphaDummy041, nb075AlphaDummy043 x), (nb075AlphaDummy001, nb075AlphaDummy002 x), (nb075AlphaDummy000, x), (nb075AlphaDummy003, nb075AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb075AlphaDummy049) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb075AlphaDummy045 (Compiler.CompactSourceSyntax.synWrex nb075AlphaDummy046 (SemanticCore.Class.cv nb075AlphaDummy042) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy045) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb075AlphaDummy046))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb075AlphaDummy049) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb075AlphaDummy045 (Compiler.CompactSourceSyntax.synWrex nb075AlphaDummy046 (SemanticCore.Class.cv nb075AlphaDummy041) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy045) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb075AlphaDummy046)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb075AlphaDummy050 x)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb075AlphaDummy047 x) (Compiler.CompactSourceSyntax.synWrex (nb075AlphaDummy048 x) (SemanticCore.Class.cv (nb075AlphaDummy044 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy047 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb075AlphaDummy048 x)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb075AlphaDummy050 x)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb075AlphaDummy047 x) (Compiler.CompactSourceSyntax.synWrex (nb075AlphaDummy048 x) (SemanticCore.Class.cv (nb075AlphaDummy043 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy047 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb075AlphaDummy048 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

      Checked nominal proof certificate identified upstream as nb075_split_alpha_0004.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfRanfn (x : SemanticCore.Var) :
        Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCranfn (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv x))))

        Checked nominal proof certificate identified upstream as nominal_df_ranfn.

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