Documentation

LeanPool.NFWeakPartition.NAR4H5C094M3Part003

NF weak partition development: NAR4H5C094M3Part003.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094SplitAlpha0003 (x y : SemanticCore.Var) :
Nominal.TAlphaWff [(nb094AlphaDummy007, nb094AlphaDummy009 x y), (nb094AlphaDummy006, nb094AlphaDummy008 x y), (nb094AlphaDummy072, nb094AlphaDummy073 x y), (nb094AlphaDummy010, nb094AlphaDummy011 x y), (nb094AlphaDummy002, nb094AlphaDummy003 x y), (nb094AlphaDummy001, y), (nb094AlphaDummy000, x), (nb094AlphaDummy004, nb094AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy007) (SemanticCore.Class.cv nb094AlphaDummy002)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy009 x y)) (SemanticCore.Class.cv (nb094AlphaDummy003 x y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb094_split_alpha_0003.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfLndifop (x y : SemanticCore.Var) (dv_x_y : x ≠ y) :
    Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synClndifop (Compiler.CompactSourceSyntax.synCmpt2 x Compiler.CompactSourceSyntax.synCvv y Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))

    Checked nominal proof certificate identified upstream as nominal_df_lndifop.

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