NF weak partition development: NominalWPPReplayChunk008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnisng (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCsn A)) A))

Checked nominal proof certificate identified upstream as g_unisng.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUniun (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCun A B)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCuni A) (Compiler.CompactSourceSyntax.synCuni B)))

Checked nominal proof certificate identified upstream as g_uniun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUniss (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCuni A) (Compiler.CompactSourceSyntax.synCuni B)))

Checked nominal proof certificate identified upstream as g_uniss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsuni (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.classMem B C)).imp (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCuni C)))

Checked nominal proof certificate identified upstream as g_ssuni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUni0b (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni A) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)))

Checked nominal proof certificate identified upstream as g_uni0b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUni0 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_uni0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElssuni (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCuni B)))

Checked nominal proof certificate identified upstream as g_elssuni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfint2 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCint A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWral y A (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dfint2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInteq (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCint A) (Compiler.CompactSourceSyntax.synCint B)))

Checked nominal proof certificate identified upstream as g_inteq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInteqi (A B : SemanticCore.Class) (hyp_inteqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCint A) (Compiler.CompactSourceSyntax.synCint B))

Checked nominal proof certificate identified upstream as g_inteqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gInteqi A B hyp_inteqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_inteqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gInteq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElint (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_elint_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCint B)) (SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_elint.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElint2 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_elint2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCint B)) (Compiler.CompactSourceSyntax.synWral x B (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_elint2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElintab (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_inteqab_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCint (SemanticCore.Class.cab x ph))) (SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_elintab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIntss1 (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCint B) A))

Checked nominal proof certificate identified upstream as g_intss1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsint (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCint B)) (Compiler.CompactSourceSyntax.synWral x B (Compiler.CompactSourceSyntax.synWss A (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_ssint.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsintab (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCint (SemanticCore.Class.cab x ph))) (SemanticCore.Wff.all x (ph.imp (Compiler.CompactSourceSyntax.synWss A (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_ssintab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsmin (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCint (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A (SemanticCore.Class.cv x)) ph))))

Checked nominal proof certificate identified upstream as g_ssmin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEliun (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCiun x B C)) (Compiler.CompactSourceSyntax.synWrex x B (SemanticCore.Wff.classMem A C)))

Checked nominal proof certificate identified upstream as g_eliun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSs2iun (x : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWss B C)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCiun x A B) (Compiler.CompactSourceSyntax.synCiun x A C)))

Checked nominal proof certificate identified upstream as g_ss2iun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIuneq2 (x : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classEq B C)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A B) (Compiler.CompactSourceSyntax.synCiun x A C)))

Checked nominal proof certificate identified upstream as g_iuneq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIuneq2i (x : SemanticCore.Var) (A B C : SemanticCore.Class) (hyp_iuneq2i_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A B) (Compiler.CompactSourceSyntax.synCiun x A C))

Checked nominal proof certificate identified upstream as g_iuneq2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfiun (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfiun_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_nfiun_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y (Compiler.CompactSourceSyntax.synCiun x A B))

Checked nominal proof certificate identified upstream as g_nfiun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfiu1 (x : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCiun x A B))

Checked nominal proof certificate identified upstream as g_nfiu1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfiun2g (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem B C)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A B) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))))

Checked nominal proof certificate identified upstream as g_dfiun2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfiun2 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_dfiun2_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A B) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)))))

Checked nominal proof certificate identified upstream as g_dfiun2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbviun (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (hyp_cbviun_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y B)) (hyp_cbviun_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x C)) (hyp_cbviun_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A B) (Compiler.CompactSourceSyntax.synCiun y A C))

Checked nominal proof certificate identified upstream as g_cbviun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIunss (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_C_x : x ∉ C.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCiun x A B) C) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWss B C)))

Checked nominal proof certificate identified upstream as g_iunss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIunab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A (SemanticCore.Class.cab y ph)) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A ph)))

Checked nominal proof certificate identified upstream as g_iunab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIunid (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) A)

Checked nominal proof certificate identified upstream as g_iunid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq1 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk A C) (Compiler.CompactSourceSyntax.synCopk B C)))

Checked nominal proof certificate identified upstream as g_opkeq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq2 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk C A) (Compiler.CompactSourceSyntax.synCopk C B)))

Checked nominal proof certificate identified upstream as g_opkeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq12 (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A C) (SemanticCore.Wff.classEq B D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCopk C D)))

Checked nominal proof certificate identified upstream as g_opkeq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq2i (A B C : SemanticCore.Class) (hyp_opkeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk C A) (Compiler.CompactSourceSyntax.synCopk C B))

Checked nominal proof certificate identified upstream as g_opkeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOpkeq2i A B C hyp_opkeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_opkeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gOpkeq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_opkeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk A C) (Compiler.CompactSourceSyntax.synCopk B C)))

Checked nominal proof certificate identified upstream as g_opkeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_opkeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk C A) (Compiler.CompactSourceSyntax.synCopk C B)))

Checked nominal proof certificate identified upstream as g_opkeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkeq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_opkeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_opkeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk A C) (Compiler.CompactSourceSyntax.synCopk B D)))

Checked nominal proof certificate identified upstream as g_opkeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCompldif (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv A))

Checked nominal proof certificate identified upstream as g_compldif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gComplV : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_complV.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNincompl (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnin A (Compiler.CompactSourceSyntax.synCcompl A)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_nincompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIncompl (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCcompl A)) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_incompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUncompl (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCcompl A)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_uncompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInindif (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCdif A B)) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_inindif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsofss (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A C).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWral x C ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)))))

Checked nominal proof certificate identified upstream as g_ssofss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsofeq (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A C) (Compiler.CompactSourceSyntax.synWss B C)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (Compiler.CompactSourceSyntax.synWral x C (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)))))

Checked nominal proof certificate identified upstream as g_ssofeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAxprimlem1 (B : SemanticCore.Class) (a c : SemanticCore.Var) (dv_B_c : c ∉ B.fv) (dv_a_c : a ≠ c) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.all c (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.objMem c a) (SemanticCore.Wff.classEq (SemanticCore.Class.cv c) B))))

Checked nominal proof certificate identified upstream as g_axprimlem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNinexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnin A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_ninexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gComplexg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcompl A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_complexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_inexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_unexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCdif A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_difexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSymdifexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsymdif A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_symdifexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gComplex (A : SemanticCore.Class) (hyp_boolex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcompl A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_complex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInex (A B : SemanticCore.Class) (hyp_boolex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_boolex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_inex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnex (A B : SemanticCore.Class) (hyp_boolex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_boolex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_unex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifex (A B : SemanticCore.Class) (hyp_boolex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_boolex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCdif A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_difex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSymdifex (A B : SemanticCore.Class) (hyp_boolex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_boolex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsymdif A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_symdifex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVvex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_vvex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0ex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_n_0ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnex (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_snex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPrex (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpr A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_prex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkex (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_opkex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnelpwg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCpw B)) (SemanticCore.Wff.classMem A B)))

Checked nominal proof certificate identified upstream as g_snelpwg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnelpw (A B : SemanticCore.Class) (hyp_snelpw_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCpw B)) (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_snelpw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnelpwi (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCpw B)))

Checked nominal proof certificate identified upstream as g_snelpwi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnipw (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCpw A)) A)

Checked nominal proof certificate identified upstream as g_unipw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSspwb (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCpw A) (Compiler.CompactSourceSyntax.synCpw B)))

Checked nominal proof certificate identified upstream as g_sspwb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwadjoin (A X : SemanticCore.Class) (a b : SemanticCore.Var) (dv_A_a : a ∉ A.fv) (dv_A_b : b ∉ A.fv) (dv_X_a : a ∉ X.fv) (dv_X_b : b ∉ X.fv) (dv_a_b : a ≠ b) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn X))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw A) (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex b (Compiler.CompactSourceSyntax.synCpw A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsn X)))))))

Checked nominal proof certificate identified upstream as g_pwadjoin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreqr1 (A B C : SemanticCore.Class) (hyp_preqr1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_preqr1_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpr A C) (Compiler.CompactSourceSyntax.synCpr B C)).imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_preqr1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreqr2 (A B C : SemanticCore.Class) (hyp_preqr2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_preqr2_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpr C A) (Compiler.CompactSourceSyntax.synCpr C B)).imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_preqr2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreqr2g (A B C V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpr C A) (Compiler.CompactSourceSyntax.synCpr C B)).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_preqr2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElopk (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCopk B C)) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpr B C))))

Checked nominal proof certificate identified upstream as g_elopk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkth1g (A B C D V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCopk C D))).imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_opkth1g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkthg (A B C D T V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem D T)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A C) (SemanticCore.Wff.classEq B D))))

Checked nominal proof certificate identified upstream as g_opkthg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEl1c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_el1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnel1c (A : SemanticCore.Class) (hyp_snel1c_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_snel1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnel1cg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synC1c))

Checked nominal proof certificate identified upstream as g_snel1cg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1cex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_n_1cex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1eq (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCpw1 B)))

Checked nominal proof certificate identified upstream as g_pw1eq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw1 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw1 B)) (Compiler.CompactSourceSyntax.synWrex x B (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_elpw1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw12 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 B))) (Compiler.CompactSourceSyntax.synWrex x B (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_elpw12.

Equations

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