Documentation

LeanPool.NFWeakPartition.NAR4H5C095M3Part015

NF weak partition development: NAR4H5C095M3Part015.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0017 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
Nominal.TAlphaWff [(nb095AlphaDummy139 D R S_cls E, nb095AlphaDummy140 f), (nb095AlphaDummy137 D R S_cls E, nb095AlphaDummy138 f), (nb095AlphaDummy092 D R S_cls E, nb095AlphaDummy094 f), (nb095AlphaDummy091 D R S_cls E, nb095AlphaDummy093 f), (nb095AlphaDummy095 D R S_cls E, nb095AlphaDummy096 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy139 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy139 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy140 f)) (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy140 f)) (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0017.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0018 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb095AlphaDummy167 D R S_cls E, nb095AlphaDummy168 f), (nb095AlphaDummy165 D R S_cls E, nb095AlphaDummy166 f), (nb095AlphaDummy134 D R S_cls E, nb095AlphaDummy136 f), (nb095AlphaDummy133 D R S_cls E, nb095AlphaDummy135 f), (nb095AlphaDummy163 D R S_cls E, nb095AlphaDummy164 f), (nb095AlphaDummy137 D R S_cls E, nb095AlphaDummy138 f), (nb095AlphaDummy092 D R S_cls E, nb095AlphaDummy094 f), (nb095AlphaDummy091 D R S_cls E, nb095AlphaDummy093 f), (nb095AlphaDummy095 D R S_cls E, nb095AlphaDummy096 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy167 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy167 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f)))).neg)

    Checked nominal proof certificate identified upstream as nb095_split_alpha_0018.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0019 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
      Nominal.TAlphaWff [(nb095AlphaDummy175 D R S_cls E, nb095AlphaDummy176 f), (nb095AlphaDummy173 D R S_cls E, nb095AlphaDummy174 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy175 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy175 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy176 f)) (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy176 f)) (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))))))).neg)

      Checked nominal proof certificate identified upstream as nb095_split_alpha_0019.

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