NF weak partition development: NominalAlphaRepairedBase001038Leaf1stReflected001.

Shared variable, support, and alpha-certificate components.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0000 (x y z : SemanticCore.Var) : Nominal.TAlphaWff [(alphaDummy021, alphaDummy024 x y), (alphaDummy020, alphaDummy023 x y), (alphaDummy019, alphaDummy022 x y), (alphaDummy017, alphaDummy018 x y), (alphaDummy013, alphaDummy015 x y), (alphaDummy014, alphaDummy016 x y), (alphaDummy006, alphaDummy008 x y), (alphaDummy005, alphaDummy007 x y), (alphaDummy011, alphaDummy012 x y), (alphaDummy009, alphaDummy010 x y), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy019) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy022 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y)))).neg)

Proof-translation construction identified upstream as split_alpha_0000.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0001 (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(alphaDummy006, alphaDummy008 x y), (alphaDummy005, alphaDummy007 x y), (alphaDummy011, alphaDummy012 x y), (alphaDummy009, alphaDummy010 x y), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy006) (SemanticCore.Class.cv alphaDummy000)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy008 x y)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y)))).neg)

Proof-translation construction identified upstream as split_alpha_0001.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0002 (x y z : SemanticCore.Var) : Nominal.TAlphaWff [(alphaDummy021, alphaDummy024 x y), (alphaDummy020, alphaDummy023 x y), (alphaDummy019, alphaDummy022 x y), (alphaDummy017, alphaDummy018 x y), (alphaDummy013, alphaDummy015 x y), (alphaDummy014, alphaDummy016 x y), (alphaDummy039, alphaDummy040 x y), (alphaDummy037, alphaDummy038 x y), (alphaDummy006, alphaDummy008 x y), (alphaDummy005, alphaDummy007 x y), (alphaDummy035, alphaDummy036 x y), (alphaDummy009, alphaDummy010 x y), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy019) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy022 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y)))).neg)

Proof-translation construction identified upstream as split_alpha_0002.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0003 (x y z : SemanticCore.Var) : Nominal.TAlphaWff [(alphaDummy039, alphaDummy040 x y), (alphaDummy037, alphaDummy038 x y), (alphaDummy006, alphaDummy008 x y), (alphaDummy005, alphaDummy007 x y), (alphaDummy035, alphaDummy036 x y), (alphaDummy009, alphaDummy010 x y), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy039) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy039) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy040 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy040 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y)))).neg)

Proof-translation construction identified upstream as split_alpha_0003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0004 (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy003) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Class.cv alphaDummy001))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy004 x y z)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))

Proof-translation construction identified upstream as split_alpha_0004.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0005 (x y z : SemanticCore.Var) : Nominal.TAlphaWff [(alphaDummy057, alphaDummy060 y z), (alphaDummy056, alphaDummy059 y z), (alphaDummy055, alphaDummy058 y z), (alphaDummy053, alphaDummy054 y z), (alphaDummy049, alphaDummy051 y z), (alphaDummy050, alphaDummy052 y z), (alphaDummy042, alphaDummy044 y z), (alphaDummy041, alphaDummy043 y z), (alphaDummy047, alphaDummy048 y z), (alphaDummy045, alphaDummy046 y z), (alphaDummy002, z), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy055) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy058 y z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z)))).neg)

Proof-translation construction identified upstream as split_alpha_0005.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0006 (x y z : SemanticCore.Var) (dv_y_z : y ≠ z) : Nominal.TAlphaWff [(alphaDummy042, alphaDummy044 y z), (alphaDummy041, alphaDummy043 y z), (alphaDummy047, alphaDummy048 y z), (alphaDummy045, alphaDummy046 y z), (alphaDummy002, z), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy042) (SemanticCore.Class.cv alphaDummy001)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy044 y z)) (SemanticCore.Class.cv y)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z)))).neg)

Proof-translation construction identified upstream as split_alpha_0006.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0007 (x y z : SemanticCore.Var) : Nominal.TAlphaWff [(alphaDummy057, alphaDummy060 y z), (alphaDummy056, alphaDummy059 y z), (alphaDummy055, alphaDummy058 y z), (alphaDummy053, alphaDummy054 y z), (alphaDummy049, alphaDummy051 y z), (alphaDummy050, alphaDummy052 y z), (alphaDummy075, alphaDummy076 y z), (alphaDummy073, alphaDummy074 y z), (alphaDummy042, alphaDummy044 y z), (alphaDummy041, alphaDummy043 y z), (alphaDummy071, alphaDummy072 y z), (alphaDummy045, alphaDummy046 y z), (alphaDummy002, z), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy055) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy058 y z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z)))).neg)

Proof-translation construction identified upstream as split_alpha_0007.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0008 (x y z : SemanticCore.Var) : Nominal.TAlphaWff [(alphaDummy075, alphaDummy076 y z), (alphaDummy073, alphaDummy074 y z), (alphaDummy042, alphaDummy044 y z), (alphaDummy041, alphaDummy043 y z), (alphaDummy071, alphaDummy072 y z), (alphaDummy045, alphaDummy046 y z), (alphaDummy002, z), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy075) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy076 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))))

Proof-translation construction identified upstream as split_alpha_0008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FirstProjectionAlpha.splitAlpha0009 (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.TAlphaWff [(alphaDummy002, z), (alphaDummy001, y), (alphaDummy000, x), (alphaDummy003, alphaDummy004 x y z)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy000) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Class.cv alphaDummy002))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv z)))

Proof-translation construction identified upstream as split_alpha_0009.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDf1st (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWex z (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))))))

Checked nominal proof certificate identified upstream as nominal_df_1st.

Equations

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