Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk011Compact001Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmcoss (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom A B)) (Compiler.CompactSourceSyntax.synCdm B))

Checked nominal proof certificate identified upstream as g_dmcoss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRncoss (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcom A B)) (Compiler.CompactSourceSyntax.synCrn A))

Checked nominal proof certificate identified upstream as g_rncoss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmcosseq (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn B) (Compiler.CompactSourceSyntax.synCdm A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom A B)) (Compiler.CompactSourceSyntax.synCdm B)))

Checked nominal proof certificate identified upstream as g_dmcosseq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmcoeq (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCrn B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom A B)) (Compiler.CompactSourceSyntax.synCdm B)))

Checked nominal proof certificate identified upstream as g_dmcoeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRncoeq (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCrn B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcom A B)) (Compiler.CompactSourceSyntax.synCrn A)))

Checked nominal proof certificate identified upstream as g_rncoeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRes0 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres A Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_res0.

Equations

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

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

Checked nominal proof certificate identified upstream as g_resundi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_resundir.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dmres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsdmres (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCdm B)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCres B A)) A))

Checked nominal proof certificate identified upstream as g_ssdmres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResss (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCres A B) A)

Checked nominal proof certificate identified upstream as g_resss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsres2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCres C A) (Compiler.CompactSourceSyntax.synCres C B)))

Checked nominal proof certificate identified upstream as g_ssres2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsreseq (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm A) B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres A B) A))

Checked nominal proof certificate identified upstream as g_ssreseq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResopab (ph : SemanticCore.Wff) (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.synCres (Compiler.CompactSourceSyntax.synCopab x y ph) A) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)))

Checked nominal proof certificate identified upstream as g_resopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIss (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synCid) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid (Compiler.CompactSourceSyntax.synCdm A))))

Checked nominal proof certificate identified upstream as g_iss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResopab2 (ph : SemanticCore.Wff) (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 B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) ph)) A) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph))))

Checked nominal proof certificate identified upstream as g_resopab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmresi (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A)) A)

Checked nominal proof certificate identified upstream as g_dmresi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResid (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres A Compiler.CompactSourceSyntax.synCvv) A)

Checked nominal proof certificate identified upstream as g_resid.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImadmrn (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima A (Compiler.CompactSourceSyntax.synCdm A)) (Compiler.CompactSourceSyntax.synCrn A))

Checked nominal proof certificate identified upstream as g_imadmrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImassrn (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima A B) (Compiler.CompactSourceSyntax.synCrn A))

Checked nominal proof certificate identified upstream as g_imassrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImai (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCid A) A)

Checked nominal proof certificate identified upstream as g_imai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIma0 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima A Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_ima0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvimass (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv A) B) (Compiler.CompactSourceSyntax.synCdm A))

Checked nominal proof certificate identified upstream as g_cnvimass.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImasn (y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_R_y : y ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima R (Compiler.CompactSourceSyntax.synCsn A)) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWbr A R (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_imasn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimasn (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCima A (Compiler.CompactSourceSyntax.synCsn B))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B C) A))

Checked nominal proof certificate identified upstream as g_elimasn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEliniseg (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv A) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synWbr C A B))

Checked nominal proof certificate identified upstream as g_eliniseg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIniseg (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv A) (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A B)))

Checked nominal proof certificate identified upstream as g_iniseg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImass2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima C A) (Compiler.CompactSourceSyntax.synCima C B)))

Checked nominal proof certificate identified upstream as g_imass2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNdmima (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm B)).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima B (Compiler.CompactSourceSyntax.synCsn A)) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ndmima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvopab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCopab x y ph)) (Compiler.CompactSourceSyntax.synCopab y x ph))

Checked nominal proof certificate identified upstream as g_cnvopab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnv0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvi : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCid) Compiler.CompactSourceSyntax.synCid)

Checked nominal proof certificate identified upstream as g_cnvi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvdif.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvin.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rnun.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part007.

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

Checked nominal proof certificate identified upstream as g_rnuni.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imaundi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imaundir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvxp (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCxp A B)) (Compiler.CompactSourceSyntax.synCxp B A))

Checked nominal proof certificate identified upstream as g_cnvxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXp0 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp A Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_xp0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpdisj2 (A B C D : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxp C A) (Compiler.CompactSourceSyntax.synCxp D B)) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_xpdisj2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmxpss (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCxp A B)) A)

Checked nominal proof certificate identified upstream as g_dmxpss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnxpss (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCxp A B)) B)

Checked nominal proof certificate identified upstream as g_rnxpss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvcnv (R : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv R)) R)

Checked nominal proof certificate identified upstream as g_cnvcnv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnveqb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmsnopg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B V).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))) (Compiler.CompactSourceSyntax.synCsn A)))

Checked nominal proof certificate identified upstream as g_dmsnopg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmsnop (A B : SemanticCore.Class) (hyp_dmsnop_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))) (Compiler.CompactSourceSyntax.synCsn A))

Checked nominal proof certificate identified upstream as g_dmsnop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvsn (A B : SemanticCore.Class) (_hyp_cnvsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (_hyp_cnvsn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop B A)))

Checked nominal proof certificate identified upstream as g_cnvsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnsnop (A B : SemanticCore.Class) (hyp_rnsnop_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))) (Compiler.CompactSourceSyntax.synCsn B))

Checked nominal proof certificate identified upstream as g_rnsnop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvresima (A B F : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres F A)) B) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) B) A))

Checked nominal proof certificate identified upstream as g_cnvresima.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResco (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcom A B) C) (Compiler.CompactSourceSyntax.synCcom A (Compiler.CompactSourceSyntax.synCres B C)))

Checked nominal proof certificate identified upstream as g_resco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImaco (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcom A B) C) (Compiler.CompactSourceSyntax.synCima A (Compiler.CompactSourceSyntax.synCima B C)))

Checked nominal proof certificate identified upstream as g_imaco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCo01 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synC0 A) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_co01.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoi1 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A Compiler.CompactSourceSyntax.synCid) A)

Checked nominal proof certificate identified upstream as g_coi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoi2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synCid A) A)

Checked nominal proof certificate identified upstream as g_coi2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_coass.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsdmrn (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCrn A)))

Checked nominal proof certificate identified upstream as g_ssdmrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfcnv2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv A) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCswap A))

Checked nominal proof certificate identified upstream as g_dfcnv2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvex (A : SemanticCore.Class) (hyp_cnvex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcnv A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_cnvex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rnexg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dmexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmex (A : SemanticCore.Class) (hyp_dmex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCdm A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_dmex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnex (A : SemanticCore.Class) (hyp_dmex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCrn A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_rnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDf2nd2 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synC1st Compiler.CompactSourceSyntax.synCswap))

Checked nominal proof certificate identified upstream as g_df2nd2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_2ndex.

Equations

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