LeanPool.NFWeakPartition.Certificates.NAR4C060C001Block002

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C060C001Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0000 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0000.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0001 (x y z r a : SemanticCore.Var) (dv_a_r : a ≠ r) :

Nominal.TAlphaWff [(nb060AlphaDummy008 , nb060AlphaDummy010 r a), (nb060AlphaDummy007 , nb060AlphaDummy009 r a), (nb060AlphaDummy013 , nb060AlphaDummy014 r a), (nb060AlphaDummy011 , nb060AlphaDummy012 r a), (nb060AlphaDummy000 , a), (nb060AlphaDummy001 , r), (nb060AlphaDummy005 , nb060AlphaDummy006 x y z r a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb060AlphaDummy008) (SemanticCore.Class.cv nb060AlphaDummy001)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb060AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb060AlphaDummy008))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb060AlphaDummy010 r a)) (SemanticCore.Class.cv r)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb060AlphaDummy009 r a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb060AlphaDummy010 r a)))).neg)

Checked nominal proof certificate identified upstream as nb060_split_alpha_0001.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0002 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0002.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0003 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0003.

Equations

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

Instances For

Certificates from NAR4C060C001Part006.

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060OrderedPairBinderOccurrence (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_ordered_pair_binder_occurrence.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as nb060_split_alpha_0004.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0005 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0005.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0006 (x y z r a : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0006.

Equations

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

Instances For

Certificates from NAR4C060C001Part007.

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0007 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0007.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0008 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0008.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0009 (x y z r a : SemanticCore.Var) (dv_y_z : y ≠ z) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0009.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0010 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0010.

Equations

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

Instances For

Certificates from NAR4C060C001Part008.

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0011 (x y z r a : SemanticCore.Var) (dv_y_z : y ≠ z) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0011.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0012 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0012.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0013 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0013.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0014 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0014.

Equations

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

Instances For

Certificates from NAR4C060C001Part009.

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0015 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0015.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0016 (x y z r a : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0016.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0017 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0017.

Equations

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

Instances For

Certificates from NAR4C060C001Part010.

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0018 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0018.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb060SplitAlpha0019 (x y z r a : SemanticCore.Var) :

Checked nominal proof certificate identified upstream as nb060_split_alpha_0019.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfTrans (x y z r a : SemanticCore.Var) (dv_a_r : a ≠ r) (dv_a_x : a ≠ x) (dv_a_y : a ≠ y) (dv_a_z : a ≠ z) (dv_r_x : r ≠ x) (dv_r_y : r ≠ y) (dv_r_z : r ≠ z) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :

Checked nominal proof certificate identified upstream as nominal_df_trans.

Equations

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

Instances For