Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012BCompact001Part015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvmpt (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (hyp_cbvmpt_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y B)) (hyp_cbvmpt_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x C)) (hyp_cbvmpt_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCmpt x A B) (Compiler.CompactSourceSyntax.synCmpt y A C))

Checked nominal proof certificate identified upstream as g_cbvmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvmptv (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (hyp_cbvmptv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCmpt x A B) (Compiler.CompactSourceSyntax.synCmpt y A C))

Checked nominal proof certificate identified upstream as g_cbvmptv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMptpreima (x : SemanticCore.Var) (A B C F : SemanticCore.Class) (dv_C_x : x ∉ C.fv) (hyp_dmmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) C) (Compiler.CompactSourceSyntax.synCrab x A (SemanticCore.Wff.classMem B C)))

Checked nominal proof certificate identified upstream as g_mptpreima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmmpt (x : SemanticCore.Var) (A B F : SemanticCore.Class) (hyp_dmmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synCrab x A (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_dmmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnmpt (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_rnmpt_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn F) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))

Checked nominal proof certificate identified upstream as g_rnmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMptfng (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_mptfng_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWfn F A))

Checked nominal proof certificate identified upstream as g_mptfng.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnmpt (x : SemanticCore.Var) (A B F V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_mptfng_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem B V)).imp (Compiler.CompactSourceSyntax.synWfn F A))

Checked nominal proof certificate identified upstream as g_fnmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnmpti (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_fnmpti_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_fnmpti_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn F A)

Checked nominal proof certificate identified upstream as g_fnmpti.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFmpt (x : SemanticCore.Var) (A B C F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_fmpt_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A C))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem C B)) (Compiler.CompactSourceSyntax.synWf F A B))

Checked nominal proof certificate identified upstream as g_fmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFmpti (x : SemanticCore.Var) (A B C F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_fmpt_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A C))) (hyp_fmpti_2 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem C B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf F A B)

Checked nominal proof certificate identified upstream as g_fmpti.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResmpt (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss B A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCmpt x A C) B) (Compiler.CompactSourceSyntax.synCmpt x B C)))

Checked nominal proof certificate identified upstream as g_resmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmptg (x : SemanticCore.Var) (A B C D R F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (hyp_fvmptg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) (hyp_fvmptg_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x D B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A D) (SemanticCore.Wff.classMem C R)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) C))

Checked nominal proof certificate identified upstream as g_fvmptg.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmpti (x : SemanticCore.Var) (A B C D F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (hyp_fvmptg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) (hyp_fvmptg_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x D B))) : Nominal.NPrf ((SemanticCore.Wff.classMem A D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCid C)))

Checked nominal proof certificate identified upstream as g_fvmpti.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmpt (x : SemanticCore.Var) (A B C D F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (hyp_fvmptg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) (hyp_fvmptg_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x D B))) (hyp_fvmpt_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem A D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) C))

Checked nominal proof certificate identified upstream as g_fvmpt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmpts (x : SemanticCore.Var) (A B C F V : SemanticCore.Class) (dv_C_x : x ∉ C.fv) (hyp_fvmpts_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x C B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsb A x B) V)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCsb A x B)))

Checked nominal proof certificate identified upstream as g_fvmpts.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmptd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B C D F V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_ph_x : x ∉ ph.fv) (hyp_fvmptd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x D B)))) (hyp_fvmptd_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classEq B C))) (hyp_fvmptd_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A D))) (hyp_fvmptd_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C V))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) C))

Checked nominal proof certificate identified upstream as g_fvmptd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmpt2i (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_fvmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCid B)))

Checked nominal proof certificate identified upstream as g_fvmpt2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvmpt2 (x : SemanticCore.Var) (A B C F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_fvmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem B C)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) B))

Checked nominal proof certificate identified upstream as g_fvmpt2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpt2mptx (x y z : SemanticCore.Var) (A B C D : SemanticCore.Class) (_dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_z : z ∉ D.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_mpt2mpt_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCmpt z (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) B)) C) (Compiler.CompactSourceSyntax.synCmpt2 x A y B D))

Checked nominal proof certificate identified upstream as g_mpt2mptx.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvmpt2ga (x y : SemanticCore.Var) (A B C D R S F 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) (hyp_ovmpt2ga_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (SemanticCore.Wff.classEq R S))) (hyp_ovmpt2ga_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x C y D R))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem S H)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A F B) S))

Checked nominal proof certificate identified upstream as g_ovmpt2ga.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvmpt2g (x y : SemanticCore.Var) (A B C D R S F G 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (_dv_G_x : x ∉ G.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) (hyp_ovmpt2g_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq R G))) (hyp_ovmpt2g_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (SemanticCore.Wff.classEq G S))) (hyp_ovmpt2g_3 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x C y D R))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem S H)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A F B) S))

Checked nominal proof certificate identified upstream as g_ovmpt2g.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part017.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvmpt2 (x y : SemanticCore.Var) (A B C D R S F G : 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_G_x : x ∉ G.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) (hyp_ovmpt2g_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq R G))) (hyp_ovmpt2g_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (SemanticCore.Wff.classEq G S))) (hyp_ovmpt2g_3 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x C y D R))) (hyp_ovmpt2_4 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A F B) S))

Checked nominal proof certificate identified upstream as g_ovmpt2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMptv (x y : SemanticCore.Var) (B : SemanticCore.Class) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv B) (Compiler.CompactSourceSyntax.synCopab x y (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)))

Checked nominal proof certificate identified upstream as g_mptv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1od (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D F W X : 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_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_f1od_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A C))) (hyp_f1od_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classMem C W))) (hyp_f1od_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp (SemanticCore.Wff.classMem D X))) (hyp_f1od_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) C)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) D))))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWf1o F A B))

Checked nominal proof certificate identified upstream as g_f1od.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1o2d (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D F : 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_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_f1od_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt x A C))) (hyp_f1o2d_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classMem C B))) (hyp_f1o2d_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp (SemanticCore.Wff.classMem D A))) (hyp_f1o2d_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) C)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWf1o F A B))

Checked nominal proof certificate identified upstream as g_f1o2d.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFmpt2x (x y : SemanticCore.Var) (A B C D F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_x_y : x ≠ y) (hyp_fmpt2x_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x A y B C))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B (SemanticCore.Wff.classMem C D))) (Compiler.CompactSourceSyntax.synWf F (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) B)) D))

Checked nominal proof certificate identified upstream as g_fmpt2x.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFmpt2 (x y : SemanticCore.Var) (A B C D F : 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_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_x_y : x ≠ y) (hyp_fmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x A y B C))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B (SemanticCore.Wff.classMem C D))) (Compiler.CompactSourceSyntax.synWf F (Compiler.CompactSourceSyntax.synCxp A B) D))

Checked nominal proof certificate identified upstream as g_fmpt2.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnmpt2 (x y : SemanticCore.Var) (A B C F 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_x_y : x ≠ y) (hyp_fmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x A y B C))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B (SemanticCore.Wff.classMem C V))).imp (Compiler.CompactSourceSyntax.synWfn F (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_fnmpt2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnmpt2i (x y : SemanticCore.Var) (A B C F : 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) (hyp_fmpt2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCmpt2 x A y B C))) (hyp_fnmpt2i_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn F (Compiler.CompactSourceSyntax.synCxp A B))

Checked nominal proof certificate identified upstream as g_fnmpt2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrsnsi (A B R : SemanticCore.Class) (hyp_brsnsi_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brsnsi_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synWbr A R B))

Checked nominal proof certificate identified upstream as g_brsnsi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpsnelsi (A B R : SemanticCore.Class) (hyp_brsnsi_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brsnsi_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCsi R)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) R))

Checked nominal proof certificate identified upstream as g_opsnelsi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrsnsi1 (x : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) (hyp_brsnsi1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsi R) B) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWbr A R (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_brsnsi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrsnsi2 (x : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) (hyp_brsnsi1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R A))))

Checked nominal proof certificate identified upstream as g_brsnsi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrco1st (A B C R : SemanticCore.Class) (hyp_brco1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brco1st_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.synCcom R Compiler.CompactSourceSyntax.synC1st) C) (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_brco1st.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrco2nd (A B C R : SemanticCore.Class) (hyp_brco1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brco1st_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.synCcom R Compiler.CompactSourceSyntax.synC2nd) C) (Compiler.CompactSourceSyntax.synWbr B R C))

Checked nominal proof certificate identified upstream as g_brco2nd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_txpeq2.

Equations

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