Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012BCompact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1st2nd2 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCxp B C)).imp (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st A) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd A))))

Checked nominal proof certificate identified upstream as g_n_1st2nd2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFununiq (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWbr A F B) (Compiler.CompactSourceSyntax.synWbr A F C)).imp (SemanticCore.Wff.classEq B C))

Checked nominal proof certificate identified upstream as g_fununiq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvsi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmsi (R : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCsi R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCdm R)))

Checked nominal proof certificate identified upstream as g_dmsi.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part011.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunsi (F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCsi F)))

Checked nominal proof certificate identified upstream as g_funsi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnsi (R : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCsi R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCrn R)))

Checked nominal proof certificate identified upstream as g_rnsi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOp1std (A B C : SemanticCore.Class) (hyp_op1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_op1st_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCop A B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st C) A))

Checked nominal proof certificate identified upstream as g_op1std.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOp2ndd (A B C : SemanticCore.Class) (hyp_op1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_op1st_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCop A B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C) B))

Checked nominal proof certificate identified upstream as g_op2ndd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_oveq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_oveq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOveq12 (A B C D F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq C D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A F C) (Compiler.CompactSourceSyntax.synCo B F D)))

Checked nominal proof certificate identified upstream as g_oveq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOveq2d (ph : SemanticCore.Wff) (A B C F : SemanticCore.Class) (hyp_oveq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo C F A) (Compiler.CompactSourceSyntax.synCo C F B)))

Checked nominal proof certificate identified upstream as g_oveq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvex (A B F : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCo A F B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ovex.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfoprab2 (ph : SemanticCore.Wff) (x y z w : SemanticCore.Var) (dv_ph_w : w ∉ ph.fv) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCoprab x y z ph) (Compiler.CompactSourceSyntax.synCopab w z (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv w) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) ph)))))

Checked nominal proof certificate identified upstream as g_dfoprab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOprabbid (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (_dv_x_z : x ≠ z) (_dv_y_z : y ≠ z) (hyp_oprabbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_oprabbid_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_oprabbid_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) (hyp_oprabbid_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCoprab x y z ps) (Compiler.CompactSourceSyntax.synCoprab x y z ch)))

Checked nominal proof certificate identified upstream as g_oprabbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOprabbidv (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_oprabbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCoprab x y z ps) (Compiler.CompactSourceSyntax.synCoprab x y z ch)))

Checked nominal proof certificate identified upstream as g_oprabbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOprabbii (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_oprabbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCoprab x y z ph) (Compiler.CompactSourceSyntax.synCoprab x y z ps))

Checked nominal proof certificate identified upstream as g_oprabbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvoprab12 (ph ps : SemanticCore.Wff) (x y z w v : SemanticCore.Var) (dv_v_w : v ≠ w) (dv_v_x : v ≠ x) (dv_v_y : v ≠ y) (dv_v_z : v ≠ z) (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) (hyp_cbvoprab12_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf w ph)) (hyp_cbvoprab12_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf v ph)) (hyp_cbvoprab12_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvoprab12_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ps)) (hyp_cbvoprab12_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x w) (SemanticCore.Wff.objEq y v)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCoprab x y z ph) (Compiler.CompactSourceSyntax.synCoprab w v z ps))

Checked nominal proof certificate identified upstream as g_cbvoprab12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmoprab (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCoprab x y z ph)) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWex z ph)))

Checked nominal proof certificate identified upstream as g_dmoprab.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEloprabga (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C V W X : SemanticCore.Class) (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_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_eloprabga_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C X)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop A B) C) (Compiler.CompactSourceSyntax.synCoprab x y z ph)) ps))

Checked nominal proof certificate identified upstream as g_eloprabga.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEloprabg (ph ps ch th : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C V W X : SemanticCore.Class) (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_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_th_x : x ∉ th.fv) (dv_th_y : y ∉ th.fv) (dv_th_z : z ∉ th.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_eloprabg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_eloprabg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_eloprabg_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C).imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C X)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop A B) C) (Compiler.CompactSourceSyntax.synCoprab x y z ph)) th))

Checked nominal proof certificate identified upstream as g_eloprabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunoprabg (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWmo z ph))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCoprab x y z ph)))

Checked nominal proof certificate identified upstream as g_funoprabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunoprab (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_funoprab_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWmo z ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCoprab x y z ph))

Checked nominal proof certificate identified upstream as g_funoprab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnoprabg (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_z : z ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y (ph.imp (Compiler.CompactSourceSyntax.synWeu z ps)))).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCoprab x y z (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synCopab x y ph)))

Checked nominal proof certificate identified upstream as g_fnoprabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnoprab (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_z : z ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_fnoprab_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWeu z ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCoprab x y z (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synCopab x y ph))

Checked nominal proof certificate identified upstream as g_fnoprab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvigg (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C F V W X : SemanticCore.Class) (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_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_ovigg_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_ovigg_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWmo z ph)) (hyp_ovigg_5 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCoprab x y z ph))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C X)).imp (ps.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A F B) C)))

Checked nominal proof certificate identified upstream as g_ovigg.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOvig (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C D R S F : SemanticCore.Class) (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_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_S_z : z ∉ S.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_ovig_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_ovig_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) R) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) S)).imp (Compiler.CompactSourceSyntax.synWmo z ph))) (hyp_ovig_3 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCoprab x y z (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) R) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) S)) ph)))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A R) (SemanticCore.Wff.classMem B S) (SemanticCore.Wff.classMem C D)).imp (ps.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A F B) C)))

Checked nominal proof certificate identified upstream as g_ovig.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOv2ag (x y z : 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_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.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_C_z : z ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_R_z : z ∉ R.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_S_z : z ∉ S.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_ov2ag_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_ov2ag_3 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCoprab x y z (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) 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_ov2ag.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOprabid2 (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCoprab x y z (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) A)) A)

Checked nominal proof certificate identified upstream as g_oprabid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOprabbi2i (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_oprabbi2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) A) ph)) : Nominal.NPrf (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCoprab x y z ph))

Checked nominal proof certificate identified upstream as g_oprabbi2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElovex12 (A B C F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCo B F C)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_elovex12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElovex1 (A B C F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCo B F C)).imp (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_elovex1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElovex2 (A B C F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCo B F C)).imp (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_elovex2.

Equations

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