Nominal proof certificates grouped in dependency order.

Certificates from NAR4C072C001Part012.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0003 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_H_x : x ∉ H.fv) (dv_H_y : y ∉ H.fv) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb072AlphaDummy044 A B R S_cls H, nb072AlphaDummy045 x y H), (nb072AlphaDummy042 A B R S_cls H, nb072AlphaDummy043 x y H), (nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy044 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy038 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy039 A B R S_cls H) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy038 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy039 A B R S_cls H))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy044 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy038 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy039 A B R S_cls H) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy038 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy039 A B R S_cls H))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy045 x y H)) (SemanticCore.Class.cab (nb072AlphaDummy040 x y H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy041 x y H) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy040 x y H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy041 x y H))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy045 x y H)) (SemanticCore.Class.cab (nb072AlphaDummy040 x y H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy041 x y H) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy040 x y H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy041 x y H))))))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0003.

Equations

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

Certificates from NAR4C072C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0004 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) : Nominal.TAlphaWff [(nb072AlphaDummy130 A B R S_cls H, nb072AlphaDummy131 y H), (nb072AlphaDummy128 A B R S_cls H, nb072AlphaDummy129 y H), (nb072AlphaDummy116 A B R S_cls H, nb072AlphaDummy117 y H), (nb072AlphaDummy118 A B R S_cls H, nb072AlphaDummy119 y H), (nb072AlphaDummy121 A B R S_cls H, nb072AlphaDummy123 y H), (nb072AlphaDummy120 A B R S_cls H, nb072AlphaDummy122 y H), (nb072AlphaDummy039 A B R S_cls H, nb072AlphaDummy041 x y H), (nb072AlphaDummy038 A B R S_cls H, nb072AlphaDummy040 x y H), (nb072AlphaDummy114 A B R S_cls H, nb072AlphaDummy115 x y H), (nb072AlphaDummy042 A B R S_cls H, nb072AlphaDummy043 x y H), (nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy130 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy124 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy125 A B R S_cls H) (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy124 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy125 A B R S_cls H))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy130 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy124 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy125 A B R S_cls H) (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy124 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy125 A B R S_cls H))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy131 y H)) (SemanticCore.Class.cab (nb072AlphaDummy126 y H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy127 y H) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy126 y H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy127 y H))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy131 y H)) (SemanticCore.Class.cab (nb072AlphaDummy126 y H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy127 y H) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy126 y H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy127 y H))))))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0004.

Equations

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