Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012BCompact001Part026.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtsnelsi3 (A B C R : SemanticCore.Class) (hyp_otsnelsi3_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_otsnelsi3_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_otsnelsi3_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn B) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCsi3 R)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCop B C)) R))

Checked nominal proof certificate identified upstream as g_otsnelsi3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSi3ex (A : SemanticCore.Class) (hyp_si3ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsi3 A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_si3ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReleqel (x y : SemanticCore.Var) (A R T : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_R_y : y ∉ R.fv) (dv_T_y : y ∉ T.fv) (dv_x_y : x ≠ y) (hyp_releqel_1 : Nominal.NPrf (SemanticCore.Wff.classMem T Compiler.CompactSourceSyntax.synCvv)) (hyp_releqel_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)) T) R) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) T) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins2 R)) Compiler.CompactSourceSyntax.synC1c))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A))

Checked nominal proof certificate identified upstream as g_releqel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReleqmpt (x y : SemanticCore.Var) (A R V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_V_y : y ∉ V.fv) (dv_x_y : x ≠ y) (hyp_releqmpt_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)) (SemanticCore.Class.cv x)) R) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) V))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxp A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins2 R)) Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCmpt x A V))

Checked nominal proof certificate identified upstream as g_releqmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReleqmpt2 (x y z : SemanticCore.Var) (A B R V : 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_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_V_z : z ∉ V.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_releqmpt2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) R) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) V))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxp A B) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 R)) Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCmpt2 x A y B V))

Checked nominal proof certificate identified upstream as g_releqmpt2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMptexlem (A R : SemanticCore.Class) (hyp_mptexlem_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_mptexlem_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxp A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins2 R)) Compiler.CompactSourceSyntax.synC1c)))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_mptexlem.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpt2exlem (A B R : SemanticCore.Class) (hyp_mpt2exlem_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_mpt2exlem_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_mpt2exlem_3 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxp A B) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2 Compiler.CompactSourceSyntax.synCsset) (Compiler.CompactSourceSyntax.synCins3 R)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_mpt2exlem.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCupvalg (A B 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.synCo A Compiler.CompactSourceSyntax.synCcup B) (Compiler.CompactSourceSyntax.synCun A B)))

Checked nominal proof certificate identified upstream as g_cupvalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFncup : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCcup Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fncup.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcupg (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 (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCop A B) Compiler.CompactSourceSyntax.synCcup C) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCun A B))))

Checked nominal proof certificate identified upstream as g_brcupg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcup (A B C : SemanticCore.Class) (hyp_brcup_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brcup_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCop A B) Compiler.CompactSourceSyntax.synCcup C) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCun A B)))

Checked nominal proof certificate identified upstream as g_brcup.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cupex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gComposevalg (A B 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.synCo A Compiler.CompactSourceSyntax.synCcompose B) (Compiler.CompactSourceSyntax.synCcom A B)))

Checked nominal proof certificate identified upstream as g_composevalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gComposefn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCcompose Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_composefn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcomposeg (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 (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCop A B) Compiler.CompactSourceSyntax.synCcompose C) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A B) C)))

Checked nominal proof certificate identified upstream as g_brcomposeg.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part028.

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

Checked nominal proof certificate identified upstream as g_composeex.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrdisjg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCdisj B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0)))

Checked nominal proof certificate identified upstream as g_brdisjg.

Equations

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