NF weak partition development: NAR4C067C001Part021.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0036 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy271, nb067AlphaDummy272 f), (nb067AlphaDummy245, nb067AlphaDummy246 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy271) (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy271) (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy272 f)) (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy272 f)) (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0036.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0037 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy083) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy085)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy084)).neg) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb067AlphaDummy088 f))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy087 f))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0037.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0696 : nb067AlphaDummy081 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0697 (f : SemanticCore.Var) : nb067AlphaDummy082 f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0698 : nb067AlphaDummy079 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0699 (f : SemanticCore.Var) : nb067AlphaDummy080 f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0700 : nb067AlphaDummy000 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0701 (f : SemanticCore.Var) : f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0702 : nb067AlphaDummy003 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0703 (x y f : SemanticCore.Var) : nb067AlphaDummy004 x y f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0704 : nb067AlphaDummy002 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0705 (y : SemanticCore.Var) : y ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0706 : nb067AlphaDummy001 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0707 (x : SemanticCore.Var) : x ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0708 : nb067AlphaDummy005 ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_wpp_notmem_0709 (x y f : SemanticCore.Var) : nb067AlphaDummy006 x y f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_envfresh_0050 (x y f : SemanticCore.Var) : Nominal.TEnvFresh [(nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] Compiler.CompactSourceSyntax.synCid.fv