Documentation

LeanPool.NFWeakPartition.Certificates.NAR4H5C095M3Part043Block001

Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4H5C095M3Part043Stage1.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0095 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) :
Nominal.TAlphaWff [(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 (nb095AlphaDummy662 D R S_cls E)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy661 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy662 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy663 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0095.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0072 (D R S_cls E : SemanticCore.Class) :
    nb095AlphaDummy791 D R S_cls E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0073 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
    nb095AlphaDummy792 u S_cls E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0074 (D R S_cls E : SemanticCore.Class) :
    nb095AlphaDummy789 D R S_cls E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0075 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
    nb095AlphaDummy790 u S_cls E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0076 (D R S_cls E : SemanticCore.Class) :
    nb095AlphaDummy004 D R S_cls E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0077 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    nb095AlphaDummy006 x u D R S_cls f E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0078 (D R S_cls E : SemanticCore.Class) :
    nb095AlphaDummy003 D R S_cls E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0079 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    nb095AlphaDummy005 x u D R S_cls f E ∉ S_cls.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0328 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) :
    Nominal.TEnvFresh [(nb095AlphaDummy791 D R S_cls E, nb095AlphaDummy792 u S_cls E), (nb095AlphaDummy789 D R S_cls E, nb095AlphaDummy790 u S_cls 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)] S_cls.fv

    Certificates from AlphaSupport.NAR4H5C095M3Part043Stage2.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0009 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) :
    Nominal.TReflOn [(nb095AlphaDummy791 D R S_cls E, nb095AlphaDummy792 u S_cls E), (nb095AlphaDummy789 D R S_cls E, nb095AlphaDummy790 u S_cls 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)] S_cls.fv

    Checked nominal proof certificate identified upstream as nb095_focused_refl_0009.

    Equations
    Instances For
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0614 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy794 D R S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0615 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
      nb095AlphaDummy796 u S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0616 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy793 D R S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0617 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
      nb095AlphaDummy795 u S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0618 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy797 D R S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0619 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
      nb095AlphaDummy798 u S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0620 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy791 D R S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0621 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
      nb095AlphaDummy792 u S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0622 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy789 D R S_cls E ∉ ∅
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0623 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :
      nb095AlphaDummy790 u S_cls E ∉ ∅