Documentation

LeanPool.NFWeakPartition.NAR4H5C095M3Part042

NF weak partition development: NAR4H5C095M3Part042.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0093 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
Nominal.TAlphaWff [(nb095AlphaDummy753 D R S_cls E, nb095AlphaDummy754 x u D R S_cls f E), (nb095AlphaDummy751 D R S_cls E, nb095AlphaDummy752 x u D R S_cls f E), (nb095AlphaDummy739 D R S_cls E, nb095AlphaDummy740 x u D R S_cls f E), (nb095AlphaDummy741 D R S_cls E, nb095AlphaDummy742 x u D R S_cls f E), (nb095AlphaDummy744 D R S_cls E, nb095AlphaDummy746 x u D R S_cls f E), (nb095AlphaDummy743 D R S_cls E, nb095AlphaDummy745 x u D R S_cls f E), (nb095AlphaDummy662 D R S_cls E, nb095AlphaDummy664 x u D R S_cls f E), (nb095AlphaDummy661 D R S_cls E, nb095AlphaDummy663 x u D R S_cls f E), (nb095AlphaDummy737 D R S_cls E, nb095AlphaDummy738 x u D R S_cls f E), (nb095AlphaDummy665 D R S_cls E, nb095AlphaDummy666 x u D R S_cls f E), (nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (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 (nb095AlphaDummy753 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy747 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy748 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy747 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy753 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy747 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy748 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy747 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy754 x u D R S_cls f E)) (SemanticCore.Class.cab (nb095AlphaDummy749 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy750 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy749 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy754 x u D R S_cls f E)) (SemanticCore.Class.cab (nb095AlphaDummy749 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy750 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy749 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0093.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0094 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb095AlphaDummy781 D R S_cls E, nb095AlphaDummy782 x u D R S_cls f E), (nb095AlphaDummy779 D R S_cls E, nb095AlphaDummy780 x u D R S_cls f E), (nb095AlphaDummy748 D R S_cls E, nb095AlphaDummy750 x u D R S_cls f E), (nb095AlphaDummy747 D R S_cls E, nb095AlphaDummy749 x u D R S_cls f E), (nb095AlphaDummy777 D R S_cls E, nb095AlphaDummy778 x u D R S_cls f E), (nb095AlphaDummy751 D R S_cls E, nb095AlphaDummy752 x u D R S_cls f E), (nb095AlphaDummy739 D R S_cls E, nb095AlphaDummy740 x u D R S_cls f E), (nb095AlphaDummy741 D R S_cls E, nb095AlphaDummy742 x u D R S_cls f E), (nb095AlphaDummy744 D R S_cls E, nb095AlphaDummy746 x u D R S_cls f E), (nb095AlphaDummy743 D R S_cls E, nb095AlphaDummy745 x u D R S_cls f E), (nb095AlphaDummy662 D R S_cls E, nb095AlphaDummy664 x u D R S_cls f E), (nb095AlphaDummy661 D R S_cls E, nb095AlphaDummy663 x u D R S_cls f E), (nb095AlphaDummy737 D R S_cls E, nb095AlphaDummy738 x u D R S_cls f E), (nb095AlphaDummy665 D R S_cls E, nb095AlphaDummy666 x u D R S_cls f E), (nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (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 (nb095AlphaDummy781 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy781 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy782 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy782 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E)))).neg)

    Checked nominal proof certificate identified upstream as nb095_split_alpha_0094.

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