Documentation

LeanPool.NFWeakPartition.NAR4H5C095M3Part033

NF weak partition development: NAR4H5C095M3Part033.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0070 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
Nominal.TAlphaWff [(nb095AlphaDummy549 D R S_cls E, nb095AlphaDummy550 f), (nb095AlphaDummy547 D R S_cls E, nb095AlphaDummy548 f), (nb095AlphaDummy387 D R S_cls E, nb095AlphaDummy390 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 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 (nb095AlphaDummy549 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy543 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy544 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy387 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy543 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy549 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy543 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy544 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy387 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy543 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy550 f)) (SemanticCore.Class.cab (nb095AlphaDummy545 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy546 f) (SemanticCore.Class.cv (nb095AlphaDummy390 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy545 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy550 f)) (SemanticCore.Class.cab (nb095AlphaDummy545 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy546 f) (SemanticCore.Class.cv (nb095AlphaDummy390 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy545 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0070.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0071 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb095AlphaDummy575 D R S_cls E, nb095AlphaDummy576 f), (nb095AlphaDummy544 D R S_cls E, nb095AlphaDummy546 f), (nb095AlphaDummy543 D R S_cls E, nb095AlphaDummy545 f), (nb095AlphaDummy573 D R S_cls E, nb095AlphaDummy574 f), (nb095AlphaDummy547 D R S_cls E, nb095AlphaDummy548 f), (nb095AlphaDummy387 D R S_cls E, nb095AlphaDummy390 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy575 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy575 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy576 f)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy576 f)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg

    Checked nominal proof certificate identified upstream as nb095_split_alpha_0071.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0072 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
      Nominal.TAlphaWff [(nb095AlphaDummy103 D R S_cls E, nb095AlphaDummy104 f), (nb095AlphaDummy101 D R S_cls E, nb095AlphaDummy102 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), (nb095AlphaDummy387 D R S_cls E, nb095AlphaDummy390 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 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 (nb095AlphaDummy103 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy103 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy104 f)) (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy104 f)) (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))))))).neg)

      Checked nominal proof certificate identified upstream as nb095_split_alpha_0072.

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