Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part044.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvmuc (g : SemanticCore.Var) (M N : SemanticCore.Class) (a b : SemanticCore.Var) (dv_M_a : a ∉ M.fv) (dv_M_b : b ∉ M.fv) (dv_N_a : a ∉ N.fv) (dv_N_b : b ∉ N.fv) (dv_N_g : g ∉ N.fv) (dv_a_b : a ≠ b) (dv_a_g : a ≠ g) (dv_b_g : b ≠ g) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo M Compiler.CompactSourceSyntax.synCmuc N) (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex b M (Compiler.CompactSourceSyntax.synWrex g N (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv a) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv b) (SemanticCore.Class.cv g))))))))

Checked nominal proof certificate identified upstream as g_ovmuc.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part045.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMucnc (A B : SemanticCore.Class) (hyp_mucnc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_mucnc_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synCmuc (Compiler.CompactSourceSyntax.synCnc B)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_mucnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMuccl (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc B) Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_muccl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMuccom (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc B) (Compiler.CompactSourceSyntax.synCo B Compiler.CompactSourceSyntax.synCmuc A)))

Checked nominal proof certificate identified upstream as g_muccom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcdisjun (A B : SemanticCore.Class) (hyp_ncdisjun_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ncdisjun_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCun A B)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCnc A) (Compiler.CompactSourceSyntax.synCnc B))))

Checked nominal proof certificate identified upstream as g_ncdisjun.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part046.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDf0c2 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC0c (Compiler.CompactSourceSyntax.synCnc Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_df0c2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0cnc : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_n_0cnc.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_1cnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDf1c3 (A : SemanticCore.Class) (hyp_df1c3_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC1c (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCsn A)))

Checked nominal proof certificate identified upstream as g_df1c3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcaddccl (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_ncaddccl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPeano2nc (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_peano2nc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnnc (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_nnnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcdisjeq (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_ncdisjeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNceleq (A B X : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X A) (SemanticCore.Wff.classMem X B))).imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_nceleq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcpw1 (A B : SemanticCore.Class) (hyp_ncpw1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc A) (Compiler.CompactSourceSyntax.synCnc B)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 B))))

Checked nominal proof certificate identified upstream as g_ncpw1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcpwpw1 (A : SemanticCore.Class) (hyp_ncpwpw1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw A))))

Checked nominal proof certificate identified upstream as g_ncpwpw1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcpw1c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCnc Compiler.CompactSourceSyntax.synC1c))

Checked nominal proof certificate identified upstream as g_ncpw1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1p1e2c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC2c)

Checked nominal proof certificate identified upstream as g_n_1p1e2c.

Equations

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

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

Checked nominal proof certificate identified upstream as g_tcex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part047.

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

Checked nominal proof certificate identified upstream as g_tceq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcspw1eu (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.classMem A Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWreu x Compiler.CompactSourceSyntax.synCncs (Compiler.CompactSourceSyntax.synWrex y A (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_ncspw1eu.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTccl (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc A) Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_tccl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqtc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1eltc (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B A)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 B) (Compiler.CompactSourceSyntax.synCtc A)))

Checked nominal proof certificate identified upstream as g_pw1eltc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc0c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc Compiler.CompactSourceSyntax.synC0c) Compiler.CompactSourceSyntax.synC0c)

Checked nominal proof certificate identified upstream as g_tc0c.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part048.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcdi (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCplc A B)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCtc A) (Compiler.CompactSourceSyntax.synCtc B))))

Checked nominal proof certificate identified upstream as g_tcdi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc1c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_tc1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2nnc : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC2c Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_n_2nnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1fin (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 A) Compiler.CompactSourceSyntax.synCfin))

Checked nominal proof certificate identified upstream as g_pw1fin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNntccl (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc A) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_nntccl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNclec (A B : SemanticCore.Class) (hyp_nclec_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_nclec_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc B)))

Checked nominal proof certificate identified upstream as g_nclec.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLecidg (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec A))

Checked nominal proof certificate identified upstream as g_lecidg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNclecid (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec A))

Checked nominal proof certificate identified upstream as g_nclecid.

Equations

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