NF weak partition development: NominalAlphaRepairedBase001041CoReflected001.

Shared variable, support, and alpha-certificate components.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.splitAlpha0000 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy021 A B, alphaDummy024 x y), (alphaDummy020 A B, alphaDummy023 x y), (alphaDummy019 A B, alphaDummy022 x y), (alphaDummy017 A B, alphaDummy018 x y), (alphaDummy013 A B, alphaDummy015 x y), (alphaDummy014 A B, alphaDummy016 x y), (alphaDummy006 A B, alphaDummy008 x y), (alphaDummy005 A B, alphaDummy007 x y), (alphaDummy011 A B, alphaDummy012 x y), (alphaDummy009 A B, alphaDummy010 x y), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy020 A B)) (SemanticCore.Class.cv (alphaDummy021 A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy019 A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy020 A B)) (SemanticCore.Class.cv (alphaDummy021 A B)))).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.CompositionAlpha.splitAlpha0001 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(alphaDummy006 A B, alphaDummy008 x y), (alphaDummy005 A B, alphaDummy007 x y), (alphaDummy011 A B, alphaDummy012 x y), (alphaDummy009 A B, alphaDummy010 x y), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy006 A B)) (SemanticCore.Class.cv (alphaDummy000 A B))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy005 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy006 A B)))).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.CompositionAlpha.splitAlpha0002 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy021 A B, alphaDummy024 x y), (alphaDummy020 A B, alphaDummy023 x y), (alphaDummy019 A B, alphaDummy022 x y), (alphaDummy017 A B, alphaDummy018 x y), (alphaDummy013 A B, alphaDummy015 x y), (alphaDummy014 A B, alphaDummy016 x y), (alphaDummy039 A B, alphaDummy040 x y), (alphaDummy037 A B, alphaDummy038 x y), (alphaDummy006 A B, alphaDummy008 x y), (alphaDummy005 A B, alphaDummy007 x y), (alphaDummy035 A B, alphaDummy036 x y), (alphaDummy009 A B, alphaDummy010 x y), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy020 A B)) (SemanticCore.Class.cv (alphaDummy021 A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy019 A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy020 A B)) (SemanticCore.Class.cv (alphaDummy021 A B)))).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.CompositionAlpha.splitAlpha0003 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy039 A B, alphaDummy040 x y), (alphaDummy037 A B, alphaDummy038 x y), (alphaDummy006 A B, alphaDummy008 x y), (alphaDummy005 A B, alphaDummy007 x y), (alphaDummy035 A B, alphaDummy036 x y), (alphaDummy009 A B, alphaDummy010 x y), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy039 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy006 A B)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy039 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy006 A B)))).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.CompositionAlpha.splitAlpha0004 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy003 A B)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (alphaDummy000 A B)) (SemanticCore.Class.cv (alphaDummy001 A B)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy004 x y z A B)) (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.CompositionAlpha.splitAlpha0005 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy057 A B, alphaDummy060 x z), (alphaDummy056 A B, alphaDummy059 x z), (alphaDummy055 A B, alphaDummy058 x z), (alphaDummy053 A B, alphaDummy054 x z), (alphaDummy049 A B, alphaDummy051 x z), (alphaDummy050 A B, alphaDummy052 x z), (alphaDummy042 A B, alphaDummy044 x z), (alphaDummy041 A B, alphaDummy043 x z), (alphaDummy047 A B, alphaDummy048 x z), (alphaDummy045 A B, alphaDummy046 x z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy056 A B)) (SemanticCore.Class.cv (alphaDummy057 A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy055 A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy056 A B)) (SemanticCore.Class.cv (alphaDummy057 A B)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy059 x z)) (SemanticCore.Class.cv (alphaDummy060 x z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy058 x z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy059 x z)) (SemanticCore.Class.cv (alphaDummy060 x 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.CompositionAlpha.splitAlpha0006 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) : Nominal.TAlphaWff [(alphaDummy042 A B, alphaDummy044 x z), (alphaDummy041 A B, alphaDummy043 x z), (alphaDummy047 A B, alphaDummy048 x z), (alphaDummy045 A B, alphaDummy046 x z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy042 A B)) (SemanticCore.Class.cv (alphaDummy000 A B))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy041 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy042 A B)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy044 x z)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 x z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 x 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.CompositionAlpha.splitAlpha0007 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy057 A B, alphaDummy060 x z), (alphaDummy056 A B, alphaDummy059 x z), (alphaDummy055 A B, alphaDummy058 x z), (alphaDummy053 A B, alphaDummy054 x z), (alphaDummy049 A B, alphaDummy051 x z), (alphaDummy050 A B, alphaDummy052 x z), (alphaDummy075 A B, alphaDummy076 x z), (alphaDummy073 A B, alphaDummy074 x z), (alphaDummy042 A B, alphaDummy044 x z), (alphaDummy041 A B, alphaDummy043 x z), (alphaDummy071 A B, alphaDummy072 x z), (alphaDummy045 A B, alphaDummy046 x z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy056 A B)) (SemanticCore.Class.cv (alphaDummy057 A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy055 A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy056 A B)) (SemanticCore.Class.cv (alphaDummy057 A B)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy059 x z)) (SemanticCore.Class.cv (alphaDummy060 x z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy058 x z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy059 x z)) (SemanticCore.Class.cv (alphaDummy060 x 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.CompositionAlpha.splitAlpha0008 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy075 A B, alphaDummy076 x z), (alphaDummy073 A B, alphaDummy074 x z), (alphaDummy042 A B, alphaDummy044 x z), (alphaDummy041 A B, alphaDummy043 x z), (alphaDummy071 A B, alphaDummy072 x z), (alphaDummy045 A B, alphaDummy046 x z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy075 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy042 A B)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy076 x z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 x 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.CompositionAlpha.wppRefl0014 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) : Nominal.TReflOn [(alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] B.fv

Proof-translation construction identified upstream as wpp_refl_0014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.splitAlpha0009 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) : Nominal.TAlphaWff [(alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (alphaDummy000 A B)) (SemanticCore.Class.cv (alphaDummy002 A B))) B) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv z)) B)

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.CompositionAlpha.splitAlpha0010 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy093 A B, alphaDummy096 y z), (alphaDummy092 A B, alphaDummy095 y z), (alphaDummy091 A B, alphaDummy094 y z), (alphaDummy089 A B, alphaDummy090 y z), (alphaDummy085 A B, alphaDummy087 y z), (alphaDummy086 A B, alphaDummy088 y z), (alphaDummy078 A B, alphaDummy080 y z), (alphaDummy077 A B, alphaDummy079 y z), (alphaDummy083 A B, alphaDummy084 y z), (alphaDummy081 A B, alphaDummy082 y z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy092 A B)) (SemanticCore.Class.cv (alphaDummy093 A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy091 A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy092 A B)) (SemanticCore.Class.cv (alphaDummy093 A B)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy095 y z)) (SemanticCore.Class.cv (alphaDummy096 y z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy094 y z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy095 y z)) (SemanticCore.Class.cv (alphaDummy096 y z)))).neg)

Proof-translation construction identified upstream as split_alpha_0010.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.splitAlpha0011 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy078 A B, alphaDummy080 y z), (alphaDummy077 A B, alphaDummy079 y z), (alphaDummy083 A B, alphaDummy084 y z), (alphaDummy081 A B, alphaDummy082 y z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy078 A B)) (SemanticCore.Class.cv (alphaDummy002 A B))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy077 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy078 A B)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy080 y z)) (SemanticCore.Class.cv z)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy079 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy080 y z)))).neg)

Proof-translation construction identified upstream as split_alpha_0011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.splitAlpha0012 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy093 A B, alphaDummy096 y z), (alphaDummy092 A B, alphaDummy095 y z), (alphaDummy091 A B, alphaDummy094 y z), (alphaDummy089 A B, alphaDummy090 y z), (alphaDummy085 A B, alphaDummy087 y z), (alphaDummy086 A B, alphaDummy088 y z), (alphaDummy111 A B, alphaDummy112 y z), (alphaDummy109 A B, alphaDummy110 y z), (alphaDummy078 A B, alphaDummy080 y z), (alphaDummy077 A B, alphaDummy079 y z), (alphaDummy107 A B, alphaDummy108 y z), (alphaDummy081 A B, alphaDummy082 y z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy092 A B)) (SemanticCore.Class.cv (alphaDummy093 A B))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy091 A B)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy092 A B)) (SemanticCore.Class.cv (alphaDummy093 A B)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (alphaDummy095 y z)) (SemanticCore.Class.cv (alphaDummy096 y z))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy094 y z)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (alphaDummy095 y z)) (SemanticCore.Class.cv (alphaDummy096 y z)))).neg)

Proof-translation construction identified upstream as split_alpha_0012.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.splitAlpha0013 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.TAlphaWff [(alphaDummy111 A B, alphaDummy112 y z), (alphaDummy109 A B, alphaDummy110 y z), (alphaDummy078 A B, alphaDummy080 y z), (alphaDummy077 A B, alphaDummy079 y z), (alphaDummy107 A B, alphaDummy108 y z), (alphaDummy081 A B, alphaDummy082 y z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy111 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy078 A B)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy112 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy080 y z))))

Proof-translation construction identified upstream as split_alpha_0013.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.splitAlpha0014 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_y_z : y ≠ z) : Nominal.TAlphaWff [(alphaDummy081 A B, alphaDummy082 y z), (alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy081 A B)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy077 A B) (Compiler.CompactSourceSyntax.synWrex (alphaDummy078 A B) (SemanticCore.Class.cv (alphaDummy002 A B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy077 A B)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy078 A B)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy081 A B)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy077 A B) (Compiler.CompactSourceSyntax.synWrex (alphaDummy078 A B) (SemanticCore.Class.cv (alphaDummy001 A B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy077 A B)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy078 A B))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy082 y z)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy079 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy080 y z) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy079 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy080 y z)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy082 y z)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy079 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy080 y z) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy079 y z)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy080 y z))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

Proof-translation construction identified upstream as split_alpha_0014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.CompositionAlpha.wppRefl0022 (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) : Nominal.TReflOn [(alphaDummy002 A B, z), (alphaDummy001 A B, y), (alphaDummy000 A B, x), (alphaDummy003 A B, alphaDummy004 x y z A B)] A.fv

Proof-translation construction identified upstream as wpp_refl_0022.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfCo (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A B) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) B (SemanticCore.Class.cv z)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) A (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as nominal_df_co.

Equations

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