Documentation

LeanPool.NFWeakPartition.NAR4C059C001Part004

NF weak partition development: NAR4C059C001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059WppRefl0009 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) :
Nominal.TReflOn [(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)] R.fv

Checked nominal proof certificate identified upstream as nb059_wpp_refl_0009.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0005 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) :
    Nominal.TAlphaWff [(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 (nb059AlphaDummy009 R S_cls)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv (nb059AlphaDummy000 R S_cls))) (SemanticCore.Class.cv (nb059AlphaDummy000 R S_cls)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy009 R S_cls)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv (nb059AlphaDummy000 R S_cls))) (SemanticCore.Class.cv (nb059AlphaDummy000 R S_cls)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy010 R a)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy010 R a)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a))).neg)

    Checked nominal proof certificate identified upstream as nb059_split_alpha_0005.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0006 (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), (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_0006.

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