Documentation

LeanPool.NFWeakPartition.AlphaSupport.NAR4H5C095M3Part038Stage2

NF weak partition development: NAR4H5C095M3Part038.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0085 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :

Nominal.TAlphaWff [(nb095AlphaDummy631 D R S_cls E, nb095AlphaDummy632 x D R), (nb095AlphaDummy629 D R S_cls E, nb095AlphaDummy630 x D R), (nb095AlphaDummy620 D R S_cls E, nb095AlphaDummy622 x D R), (nb095AlphaDummy619 D R S_cls E, nb095AlphaDummy621 x D R), (nb095AlphaDummy623 D R S_cls E, nb095AlphaDummy624 x D R), (nb095AlphaDummy617 D R S_cls E, nb095AlphaDummy618 x D R), (nb095AlphaDummy615 D R S_cls E, nb095AlphaDummy616 x D R), (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 (nb095AlphaDummy631 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy625 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy626 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy619 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy625 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy631 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy625 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy626 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy619 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy625 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy632 x D R)) (SemanticCore.Class.cab (nb095AlphaDummy627 x D R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy628 x D R) (SemanticCore.Class.cv (nb095AlphaDummy621 x D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy627 x D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy632 x D R)) (SemanticCore.Class.cab (nb095AlphaDummy627 x D R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy628 x D R) (SemanticCore.Class.cv (nb095AlphaDummy621 x D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy627 x D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0085.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0086 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :

Nominal.TAlphaWff [(nb095AlphaDummy659 D R S_cls E, nb095AlphaDummy660 x D R), (nb095AlphaDummy657 D R S_cls E, nb095AlphaDummy658 x D R), (nb095AlphaDummy626 D R S_cls E, nb095AlphaDummy628 x D R), (nb095AlphaDummy625 D R S_cls E, nb095AlphaDummy627 x D R), (nb095AlphaDummy655 D R S_cls E, nb095AlphaDummy656 x D R), (nb095AlphaDummy629 D R S_cls E, nb095AlphaDummy630 x D R), (nb095AlphaDummy620 D R S_cls E, nb095AlphaDummy622 x D R), (nb095AlphaDummy619 D R S_cls E, nb095AlphaDummy621 x D R), (nb095AlphaDummy623 D R S_cls E, nb095AlphaDummy624 x D R), (nb095AlphaDummy617 D R S_cls E, nb095AlphaDummy618 x D R), (nb095AlphaDummy615 D R S_cls E, nb095AlphaDummy616 x D R), (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 (nb095AlphaDummy659 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy659 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy660 x D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy660 x D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R)))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0086.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0056 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy620 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0057 (x : SemanticCore.Var) (D R : SemanticCore.Class) :

nb095AlphaDummy622 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0058 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy619 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0059 (x : SemanticCore.Var) (D R : SemanticCore.Class) :

nb095AlphaDummy621 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0060 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy623 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0061 (x : SemanticCore.Var) (D R : SemanticCore.Class) :

nb095AlphaDummy624 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0062 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy617 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0063 (x : SemanticCore.Var) (D R : SemanticCore.Class) :

nb095AlphaDummy618 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0064 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy615 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0065 (x : SemanticCore.Var) (D R : SemanticCore.Class) :

nb095AlphaDummy616 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0298 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) :

Nominal.TEnvFresh [(nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy620 D R S_cls E, nb095AlphaDummy622 x D R), (nb095AlphaDummy619 D R S_cls E, nb095AlphaDummy621 x D R), (nb095AlphaDummy623 D R S_cls E, nb095AlphaDummy624 x D R), (nb095AlphaDummy617 D R S_cls E, nb095AlphaDummy618 x D R), (nb095AlphaDummy615 D R S_cls E, nb095AlphaDummy616 x D R), (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)] D.fv