Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrpprod (x y z w : SemanticCore.Var) (A B R S : SemanticCore.Class) (dv_A_w : w ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_w : w ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_R_w : w ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_S_w : w ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_S_z : z ∉ S.fv) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCpprod R S) B) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv z) (SemanticCore.Class.cv w))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv z)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) S (SemanticCore.Class.cv w)))))))))

Checked nominal proof certificate identified upstream as g_brpprod.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part007.

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

Checked nominal proof certificate identified upstream as g_dmpprod.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part008.

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

Checked nominal proof certificate identified upstream as g_cnvpprod.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rnpprod.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnpprod (A B F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G B)).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCpprod F G) (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_fnpprod.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1opprod (A B C D F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F A C) (Compiler.CompactSourceSyntax.synWf1o G B D)).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCpprod F G) (Compiler.CompactSourceSyntax.synCxp A B) (Compiler.CompactSourceSyntax.synCxp C D)))

Checked nominal proof certificate identified upstream as g_f1opprod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvcross (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.synCcross B) (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_ovcross.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFncross : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCcross Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fncross.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcrossg (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.synCcross C) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCxp A B))))

Checked nominal proof certificate identified upstream as g_brcrossg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcross (A B C : SemanticCore.Class) (hyp_brcross_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brcross_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.synCcross C) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_brcross.

Equations

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

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

Checked nominal proof certificate identified upstream as g_crossex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1fnval (A : SemanticCore.Class) (hyp_pw1fnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCpw1fn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCpw1 A))

Checked nominal proof certificate identified upstream as g_pw1fnval.

Equations

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