Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C074C001Block002

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C074C001Part008.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb074SplitAlpha0003 (x : SemanticCore.Var) :
Nominal.TAlphaWff [(nb074AlphaDummy046, nb074AlphaDummy048 x), (nb074AlphaDummy045, nb074AlphaDummy047 x), (nb074AlphaDummy075, nb074AlphaDummy076 x), (nb074AlphaDummy049, nb074AlphaDummy050 x), (nb074AlphaDummy042, nb074AlphaDummy044 x), (nb074AlphaDummy041, nb074AlphaDummy043 x), (nb074AlphaDummy001, nb074AlphaDummy002 x), (nb074AlphaDummy000, x), (nb074AlphaDummy003, nb074AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy046) (SemanticCore.Class.cv nb074AlphaDummy041)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy045) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy046)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy048 x)) (SemanticCore.Class.cv (nb074AlphaDummy043 x))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy047 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy048 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb074_split_alpha_0003.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb074SplitAlpha0004 (x : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb074AlphaDummy049, nb074AlphaDummy050 x), (nb074AlphaDummy042, nb074AlphaDummy044 x), (nb074AlphaDummy041, nb074AlphaDummy043 x), (nb074AlphaDummy001, nb074AlphaDummy002 x), (nb074AlphaDummy000, x), (nb074AlphaDummy003, nb074AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy049) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb074AlphaDummy045 (Compiler.CompactSourceSyntax.synWrex nb074AlphaDummy046 (SemanticCore.Class.cv nb074AlphaDummy042) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy045) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy046))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy049) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb074AlphaDummy045 (Compiler.CompactSourceSyntax.synWrex nb074AlphaDummy046 (SemanticCore.Class.cv nb074AlphaDummy041) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy045) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy046)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy050 x)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb074AlphaDummy047 x) (Compiler.CompactSourceSyntax.synWrex (nb074AlphaDummy048 x) (SemanticCore.Class.cv (nb074AlphaDummy044 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy047 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy048 x)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy050 x)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb074AlphaDummy047 x) (Compiler.CompactSourceSyntax.synWrex (nb074AlphaDummy048 x) (SemanticCore.Class.cv (nb074AlphaDummy043 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy047 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy048 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

    Checked nominal proof certificate identified upstream as nb074_split_alpha_0004.

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

      Certificates from NAR4C074C001Part009.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb074SplitAlpha0005 (x : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb074AlphaDummy093, nb074AlphaDummy094 x), (nb074AlphaDummy091, nb074AlphaDummy092 x), (nb074AlphaDummy082, nb074AlphaDummy084 x), (nb074AlphaDummy081, nb074AlphaDummy083 x), (nb074AlphaDummy085, nb074AlphaDummy086 x), (nb074AlphaDummy042, nb074AlphaDummy044 x), (nb074AlphaDummy041, nb074AlphaDummy043 x), (nb074AlphaDummy001, nb074AlphaDummy002 x), (nb074AlphaDummy000, x), (nb074AlphaDummy003, nb074AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy093) (SemanticCore.Class.cab nb074AlphaDummy087 (Compiler.CompactSourceSyntax.synWrex nb074AlphaDummy088 (SemanticCore.Class.cv nb074AlphaDummy081) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy087) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy088)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy093) (SemanticCore.Class.cab nb074AlphaDummy087 (Compiler.CompactSourceSyntax.synWrex nb074AlphaDummy088 (SemanticCore.Class.cv nb074AlphaDummy081) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy087) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy088)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy094 x)) (SemanticCore.Class.cab (nb074AlphaDummy089 x) (Compiler.CompactSourceSyntax.synWrex (nb074AlphaDummy090 x) (SemanticCore.Class.cv (nb074AlphaDummy083 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy089 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy090 x))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy094 x)) (SemanticCore.Class.cab (nb074AlphaDummy089 x) (Compiler.CompactSourceSyntax.synWrex (nb074AlphaDummy090 x) (SemanticCore.Class.cv (nb074AlphaDummy083 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy089 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy090 x))))))).neg)

      Checked nominal proof certificate identified upstream as nb074_split_alpha_0005.

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