Documentation

LeanPool.NFWeakPartition.NAR4H5C095M3Part030

NF weak partition development: NAR4H5C095M3Part030.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0061 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
Nominal.TAlphaWff [(nb095AlphaDummy477 D R S_cls E, nb095AlphaDummy478 f), (nb095AlphaDummy475 D R S_cls E, nb095AlphaDummy476 f), (nb095AlphaDummy466 D R S_cls E, nb095AlphaDummy468 f), (nb095AlphaDummy465 D R S_cls E, nb095AlphaDummy467 f), (nb095AlphaDummy469 D R S_cls E, nb095AlphaDummy470 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 (nb095AlphaDummy477 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy471 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy472 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy465 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy471 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy477 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy471 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy472 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy465 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy471 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy478 f)) (SemanticCore.Class.cab (nb095AlphaDummy473 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy474 f) (SemanticCore.Class.cv (nb095AlphaDummy467 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy473 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy478 f)) (SemanticCore.Class.cab (nb095AlphaDummy473 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy474 f) (SemanticCore.Class.cv (nb095AlphaDummy467 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy473 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0061.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0062 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb095AlphaDummy505 D R S_cls E, nb095AlphaDummy506 f), (nb095AlphaDummy503 D R S_cls E, nb095AlphaDummy504 f), (nb095AlphaDummy472 D R S_cls E, nb095AlphaDummy474 f), (nb095AlphaDummy471 D R S_cls E, nb095AlphaDummy473 f), (nb095AlphaDummy501 D R S_cls E, nb095AlphaDummy502 f), (nb095AlphaDummy475 D R S_cls E, nb095AlphaDummy476 f), (nb095AlphaDummy466 D R S_cls E, nb095AlphaDummy468 f), (nb095AlphaDummy465 D R S_cls E, nb095AlphaDummy467 f), (nb095AlphaDummy469 D R S_cls E, nb095AlphaDummy470 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 (nb095AlphaDummy505 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy505 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy506 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy506 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f)))).neg)

    Checked nominal proof certificate identified upstream as nb095_split_alpha_0062.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0063 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
      Nominal.TAlphaWff [(nb095AlphaDummy513 D R S_cls E, nb095AlphaDummy514 f), (nb095AlphaDummy511 D R S_cls E, nb095AlphaDummy512 f), (nb095AlphaDummy466 D R S_cls E, nb095AlphaDummy468 f), (nb095AlphaDummy465 D R S_cls E, nb095AlphaDummy467 f), (nb095AlphaDummy469 D R S_cls E, nb095AlphaDummy470 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 (nb095AlphaDummy513 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy507 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy508 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy466 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy507 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy513 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy507 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy508 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy466 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy507 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy514 f)) (SemanticCore.Class.cab (nb095AlphaDummy509 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy510 f) (SemanticCore.Class.cv (nb095AlphaDummy468 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy509 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy514 f)) (SemanticCore.Class.cab (nb095AlphaDummy509 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy510 f) (SemanticCore.Class.cv (nb095AlphaDummy468 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy509 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f))))))).neg)

      Checked nominal proof certificate identified upstream as nb095_split_alpha_0063.

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