Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012BCompact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oiso (x y z w : SemanticCore.Var) (A B R S H : 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_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_H_w : w ∉ H.fv) (dv_H_x : x ∉ H.fv) (dv_H_y : y ∉ H.fv) (dv_H_z : z ∉ H.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_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.synWa (Compiler.CompactSourceSyntax.synWf1o H A B) (SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCopab z w (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv w) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)))))))).imp (Compiler.CompactSourceSyntax.synWiso H R S A B))

Checked nominal proof certificate identified upstream as g_f1oiso.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part007.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oiso2 (x y : SemanticCore.Var) (A B R S H : 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_H_x : x ∉ H.fv) (dv_H_y : y ∉ H.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) (hyp_f1oiso2_1 : Nominal.NPrf (SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv H) (SemanticCore.Class.cv x)) R (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv H) (SemanticCore.Class.cv y))))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o H A B).imp (Compiler.CompactSourceSyntax.synWiso H R S A B))

Checked nominal proof certificate identified upstream as g_f1oiso2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpbr1st (A B C : SemanticCore.Class) (hyp_opbr1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opbr1st_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.synC1st C) (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_opbr1st.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpbr2nd (A B C : SemanticCore.Class) (hyp_opbr1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opbr1st_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.synC2nd C) (SemanticCore.Wff.classEq B C))

Checked nominal proof certificate identified upstream as g_opbr2nd.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part008.

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

Checked nominal proof certificate identified upstream as g_dfid4.

Equations

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

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

Checked nominal proof certificate identified upstream as g_idex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1stfo : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfo Compiler.CompactSourceSyntax.synC1st Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_n_1stfo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2ndfo : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfo Compiler.CompactSourceSyntax.synC2nd Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_n_2ndfo.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dfdm4.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part009.

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

Checked nominal proof certificate identified upstream as g_dfrn5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrswap (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.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCswap B) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (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 y) (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_brswap.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvswap.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSwapf1o : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o Compiler.CompactSourceSyntax.synCswap Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_swapf1o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSwapres (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCswap A) A (Compiler.CompactSourceSyntax.synCcnv A))

Checked nominal proof certificate identified upstream as g_swapres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpnedisj (A B C D : SemanticCore.Class) (hyp_xpnedisj_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) (hyp_xpnedisj_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn C)) (Compiler.CompactSourceSyntax.synCxp B (Compiler.CompactSourceSyntax.synCsn D))) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_xpnedisj.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpfv1st (A B : SemanticCore.Class) (hyp_opfv1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opfv1st_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCop A B)) A)

Checked nominal proof certificate identified upstream as g_opfv1st.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpfv2nd (A B : SemanticCore.Class) (hyp_opfv1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opfv1st_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCop A B)) B)

Checked nominal proof certificate identified upstream as g_opfv2nd.

Equations

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