Nominal proof certificates grouped in dependency order.

Certificates from NAR4C090C001Part110.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0088 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) : Nominal.TAlphaWff [(nb090AlphaDummy721 A, nb090AlphaDummy722 v u h), (nb090AlphaDummy719 A, nb090AlphaDummy720 v u h), (nb090AlphaDummy707 A, nb090AlphaDummy708 v u h), (nb090AlphaDummy709 A, nb090AlphaDummy710 v u h), (nb090AlphaDummy712 A, nb090AlphaDummy714 v u h), (nb090AlphaDummy711 A, nb090AlphaDummy713 v u h), (nb090AlphaDummy700 A, nb090AlphaDummy702 v u h), (nb090AlphaDummy699 A, nb090AlphaDummy701 v u h), (nb090AlphaDummy705 A, nb090AlphaDummy706 v u h), (nb090AlphaDummy703 A, nb090AlphaDummy704 v u h), (nb090AlphaDummy042 A, nb090AlphaDummy044 v u h), (nb090AlphaDummy041 A, nb090AlphaDummy043 v u h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy721 A)) (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy721 A)) (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy722 v u h)) (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy722 v u h)) (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))))))).neg)

Checked nominal proof certificate identified upstream as nb090_split_alpha_0088.

Equations

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

Certificates from NAR4C090C001Part111.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0089 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) : Nominal.TAlphaWff [(nb090AlphaDummy749 A, nb090AlphaDummy750 v u h), (nb090AlphaDummy747 A, nb090AlphaDummy748 v u h), (nb090AlphaDummy716 A, nb090AlphaDummy718 v u h), (nb090AlphaDummy715 A, nb090AlphaDummy717 v u h), (nb090AlphaDummy745 A, nb090AlphaDummy746 v u h), (nb090AlphaDummy719 A, nb090AlphaDummy720 v u h), (nb090AlphaDummy707 A, nb090AlphaDummy708 v u h), (nb090AlphaDummy709 A, nb090AlphaDummy710 v u h), (nb090AlphaDummy712 A, nb090AlphaDummy714 v u h), (nb090AlphaDummy711 A, nb090AlphaDummy713 v u h), (nb090AlphaDummy700 A, nb090AlphaDummy702 v u h), (nb090AlphaDummy699 A, nb090AlphaDummy701 v u h), (nb090AlphaDummy705 A, nb090AlphaDummy706 v u h), (nb090AlphaDummy703 A, nb090AlphaDummy704 v u h), (nb090AlphaDummy042 A, nb090AlphaDummy044 v u h), (nb090AlphaDummy041 A, nb090AlphaDummy043 v u h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy749 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy749 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy750 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy750 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)))).neg)

Checked nominal proof certificate identified upstream as nb090_split_alpha_0089.

Equations

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