Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart001.

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

Checked nominal proof certificate identified upstream as g_elpw1101c.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elpw1111c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1ss1c (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCpw1 A) Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_pw1ss1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0nel1c : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC1c).neg

Checked nominal proof certificate identified upstream as g_n_0nel1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw0 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_pw0.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw10.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqpw1 (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.classEq A (Compiler.CompactSourceSyntax.synCpw1 B)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)))))

Checked nominal proof certificate identified upstream as g_eqpw1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw1un.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw1in.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw1sn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw10b (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw1 A) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_pw10b.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDf1c2 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC1c (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_df1c2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw1ss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw111.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eluni1g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEluni1 (A B : SemanticCore.Class) (hyp_eluni1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCuni1 B)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) B))

Checked nominal proof certificate identified upstream as g_eluni1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElxpk (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCxpk B C)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) C))))))

Checked nominal proof certificate identified upstream as g_elxpk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElxpk2 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCxpk B C)) (Compiler.CompactSourceSyntax.synWrex x B (Compiler.CompactSourceSyntax.synWrex y C (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_elxpk2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpkeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpkeq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpkeq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpkeq12i (A B C D : SemanticCore.Class) (hyp_xpkeq12i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_xpkeq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxpk A C) (Compiler.CompactSourceSyntax.synCxpk B D))

Checked nominal proof certificate identified upstream as g_xpkeq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpkeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_xpkeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxpk C A) (Compiler.CompactSourceSyntax.synCxpk C B)))

Checked nominal proof certificate identified upstream as g_xpkeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElvvk (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 (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_elvvk.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkabssvvk (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) ph)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_opkabssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkabssvvki (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (hyp_opkabssvvki_1 : Nominal.NPrf (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) ph)))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_opkabssvvki.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpkssvvk (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCxpk A B) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_xpkssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsrelk (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B))))))

Checked nominal proof certificate identified upstream as g_ssrelk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqrelk (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWss B (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B))))))

Checked nominal proof certificate identified upstream as g_eqrelk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqrelkriiv (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_eqrelkriiv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))) (hyp_eqrelkriiv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))) (hyp_eqrelkriiv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B))) : Nominal.NPrf (SemanticCore.Wff.classEq A B)

Checked nominal proof certificate identified upstream as g_eqrelkriiv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvkeq.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart004.

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

Checked nominal proof certificate identified upstream as g_ins2keq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ins3keq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imakeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imakeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImakeq1i (A B C : SemanticCore.Class) (hyp_imakeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimak A C) (Compiler.CompactSourceSyntax.synCimak B C))

Checked nominal proof certificate identified upstream as g_imakeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImakeq1i A B C hyp_imakeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_imakeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gImakeq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImakeq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_imakeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimak A C) (Compiler.CompactSourceSyntax.synCimak B C)))

Checked nominal proof certificate identified upstream as g_imakeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImakeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_imakeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimak C A) (Compiler.CompactSourceSyntax.synCimak C B)))

Checked nominal proof certificate identified upstream as g_imakeq2d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_p6eq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sikeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelopkabg (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C V W : SemanticCore.Class) (_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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_ch_z : z ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_opkelopkabg_1 : Nominal.NPrf (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) ph)))))) (hyp_opkelopkabg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_opkelopkabg_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B V) (SemanticCore.Wff.classMem C W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) A) ch))

Checked nominal proof certificate identified upstream as g_opkelopkabg.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelopkab (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_ch_z : z ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_opkelopkab_1 : Nominal.NPrf (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) ph)))))) (hyp_opkelopkab_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_opkelopkab_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_opkelopkab_4 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_opkelopkab_5 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) A) ch)

Checked nominal proof certificate identified upstream as g_opkelopkab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_opkelxpkg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelxpk (A B C D : SemanticCore.Class) (hyp_opkelxpk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opkelxpk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCxpk C D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)))

Checked nominal proof certificate identified upstream as g_opkelxpk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelcnvkg (A B C V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCcnvk C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) C)))

Checked nominal proof certificate identified upstream as g_opkelcnvkg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelcnvk (A B C : SemanticCore.Class) (hyp_opkelcnvk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opkelcnvk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCcnvk C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) C))

Checked nominal proof certificate identified upstream as g_opkelcnvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelins2kg (x y z : SemanticCore.Var) (A B C V W : 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCins2k C)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv z)) C)))))))

Checked nominal proof certificate identified upstream as g_opkelins2kg.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelins3kg (x y z : SemanticCore.Var) (A B C V W : 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCins3k C)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) C)))))))

Checked nominal proof certificate identified upstream as g_opkelins3kg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtkelins2kg (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 C T)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCopk B C)) (Compiler.CompactSourceSyntax.synCins2k D)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A C) D)))

Checked nominal proof certificate identified upstream as g_otkelins2kg.

Equations

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