Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C073C001Block004

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C073C001Part008.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb073SplitAlpha0004 (x y : SemanticCore.Var) :
Nominal.TAlphaWff [(nb073AlphaDummy086, nb073AlphaDummy087 x y), (nb073AlphaDummy084, nb073AlphaDummy085 x y), (nb073AlphaDummy015, nb073AlphaDummy017 x y), (nb073AlphaDummy014, nb073AlphaDummy016 x y), (nb073AlphaDummy078, nb073AlphaDummy079 x y), (nb073AlphaDummy002, nb073AlphaDummy003 x y), (nb073AlphaDummy001, y), (nb073AlphaDummy000, x), (nb073AlphaDummy004, nb073AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy086) (SemanticCore.Class.cab nb073AlphaDummy080 (Compiler.CompactSourceSyntax.synWrex nb073AlphaDummy081 (SemanticCore.Class.cv nb073AlphaDummy014) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy080) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy081)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy086) (SemanticCore.Class.cab nb073AlphaDummy080 (Compiler.CompactSourceSyntax.synWrex nb073AlphaDummy081 (SemanticCore.Class.cv nb073AlphaDummy014) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy080) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy081)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy087 x y)) (SemanticCore.Class.cab (nb073AlphaDummy082 x y) (Compiler.CompactSourceSyntax.synWrex (nb073AlphaDummy083 x y) (SemanticCore.Class.cv (nb073AlphaDummy016 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy082 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy083 x y))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy087 x y)) (SemanticCore.Class.cab (nb073AlphaDummy082 x y) (Compiler.CompactSourceSyntax.synWrex (nb073AlphaDummy083 x y) (SemanticCore.Class.cv (nb073AlphaDummy016 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy082 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy083 x y))))))).neg)

Checked nominal proof certificate identified upstream as nb073_split_alpha_0004.

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

    Certificates from NAR4C073C001Part009.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb073SplitAlpha0005 (x y : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb073AlphaDummy112, nb073AlphaDummy113 x y), (nb073AlphaDummy081, nb073AlphaDummy083 x y), (nb073AlphaDummy080, nb073AlphaDummy082 x y), (nb073AlphaDummy110, nb073AlphaDummy111 x y), (nb073AlphaDummy084, nb073AlphaDummy085 x y), (nb073AlphaDummy015, nb073AlphaDummy017 x y), (nb073AlphaDummy014, nb073AlphaDummy016 x y), (nb073AlphaDummy078, nb073AlphaDummy079 x y), (nb073AlphaDummy002, nb073AlphaDummy003 x y), (nb073AlphaDummy001, y), (nb073AlphaDummy000, x), (nb073AlphaDummy004, nb073AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy112) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy081)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy112) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy113 x y)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy083 x y))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy113 x y)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

    Checked nominal proof certificate identified upstream as nb073_split_alpha_0005.

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

      Checked nominal proof certificate identified upstream as nominal_df_cross.

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