Nominal proof certificates grouped in dependency order.

Certificates from NAR4C089C001Part004.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089SplitAlpha0000 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TAlphaWff [(nb089AlphaDummy008 A B R, nb089AlphaDummy010 u A B R), (nb089AlphaDummy007 A B R, nb089AlphaDummy009 u A B R), (nb089AlphaDummy037 A B R, nb089AlphaDummy038 u A B R), (nb089AlphaDummy011 A B R, nb089AlphaDummy012 u A B R), (nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy008 A B R)) (SemanticCore.Class.cv (nb089AlphaDummy003 A B R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy007 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy008 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy010 u A B R)) (SemanticCore.Class.cv (nb089AlphaDummy004 u A B R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy009 u A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy010 u A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb089_split_alpha_0000.

Equations

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

Certificates from NAR4C089C001Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089SplitAlpha0001 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : Nominal.TAlphaWff [(nb089AlphaDummy011 A B R, nb089AlphaDummy012 u A B R), (nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy011 A B R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb089AlphaDummy007 A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy008 A B R) (SemanticCore.Class.cv (nb089AlphaDummy000 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy007 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy008 A B R)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy011 A B R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb089AlphaDummy007 A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy008 A B R) (SemanticCore.Class.cv (nb089AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy007 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy008 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy012 u A B R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb089AlphaDummy009 u A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy010 u A B R) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy009 u A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy010 u A B R)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb089AlphaDummy012 u A B R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb089AlphaDummy009 u A B R) (Compiler.CompactSourceSyntax.synWrex (nb089AlphaDummy010 u A B R) (SemanticCore.Class.cv (nb089AlphaDummy004 u A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb089AlphaDummy009 u A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb089AlphaDummy010 u A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

Checked nominal proof certificate identified upstream as nb089_split_alpha_0001.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0000 (A B R : SemanticCore.Class) : nb089AlphaDummy003 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0114 (A B R : SemanticCore.Class) : nb089AlphaDummy003 A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0001 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy004 u A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0115 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy004 u A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0002 (A B R : SemanticCore.Class) : nb089AlphaDummy000 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0116 (A B R : SemanticCore.Class) : nb089AlphaDummy000 A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0117 (u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) : u ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0003 (A B R : SemanticCore.Class) : nb089AlphaDummy005 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0118 (A B R : SemanticCore.Class) : nb089AlphaDummy005 A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0004 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy006 u A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0119 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy006 u A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0005 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0120 (A B R : SemanticCore.Class) : nb089AlphaDummy001 A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_focused_notmem_0006 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy002 u A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_wpp_notmem_0121 (u : SemanticCore.Var) (A B R : SemanticCore.Class) : nb089AlphaDummy002 u A B R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089_compact_envfresh_0007 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) : Nominal.TEnvFresh [(nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0007 (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_u : u ∉ A.fv) : Nominal.TReflOn [(nb089AlphaDummy003 A B R, nb089AlphaDummy004 u A B R), (nb089AlphaDummy000 A B R, u), (nb089AlphaDummy005 A B R, nb089AlphaDummy006 u A B R), (nb089AlphaDummy001 A B R, nb089AlphaDummy002 u A B R)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))).fv

Checked nominal proof certificate identified upstream as nb089_wpp_refl_0007.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb089WppRefl0007 u A B R dv_A_u = ⋯.reflOn