Documentation

LeanPool.NFWeakPartition.Certificates.NAR4H5C091M3BPart006Block001

Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4H5C091M3BPart006Stage2.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091WppRefl0022 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_R_p : p ∉ R.fv) :
Nominal.TReflOn [(nb091AlphaDummy106 D R, nb091AlphaDummy108 R p), (nb091AlphaDummy105 D R, nb091AlphaDummy107 R p), (nb091AlphaDummy103 D R, nb091AlphaDummy104 D R p), (nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

Checked nominal proof certificate identified upstream as nb091_wpp_refl_0022.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0007 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) (dv_R_p : p ∉ R.fv) :
    Nominal.TAlphaWff [(nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy101 D R)) (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy101 D R)) (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy102 D R p)) (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy102 D R p)) (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))).neg)

    Checked nominal proof certificate identified upstream as nb091_split_alpha_0007.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0008 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) (dv_R_p : p ∉ R.fv) :
      Nominal.TAlphaWff [(nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy048 D R)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy050 D R p)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p)))).neg)

      Checked nominal proof certificate identified upstream as nb091_split_alpha_0008.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0070 (D R : SemanticCore.Class) :
        nb091AlphaDummy177 D R ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0071 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy178 D R p ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_envfresh_0028 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
        Nominal.TEnvFresh [(nb091AlphaDummy103 D R, nb091AlphaDummy104 D R p), (nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy177 D R, nb091AlphaDummy178 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] D.fv

        Certificates from AlphaSupport.NAR4H5C091M3BPart006Stage3.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091FocusedRefl0002 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
        Nominal.TReflOn [(nb091AlphaDummy103 D R, nb091AlphaDummy104 D R p), (nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy177 D R, nb091AlphaDummy178 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] D.fv

        Checked nominal proof certificate identified upstream as nb091_focused_refl_0002.

        Equations
        Instances For
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0128 (D R : SemanticCore.Class) :
          nb091AlphaDummy177 D R ∉ ∅
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0129 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy178 D R p ∉ ∅