Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrec0 (ph : SemanticCore.Wff) (F G I : SemanticCore.Class) (hyp_frec0_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_frec0_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns))) (hyp_frec0_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_frec0_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G)))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F Compiler.CompactSourceSyntax.synC0c) I))

Checked nominal proof certificate identified upstream as g_frec0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecsuc (ph : SemanticCore.Wff) (F G I X : SemanticCore.Class) (hyp_frecsuc_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_frecsuc_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns))) (hyp_frecsuc_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_frecsuc_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_frecsuc_5 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCnnc))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCplc X Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv F X))))

Checked nominal proof certificate identified upstream as g_frecsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcg (A B : SemanticCore.Class) (f g h : SemanticCore.Var) (V W : SemanticCore.Class) (_dv_A_V : Disjoint A.fv V.fv) (_dv_A_W : Disjoint A.fv W.fv) (dv_A_f : f ∉ A.fv) (dv_A_g : g ∉ A.fv) (dv_A_h : h ∉ A.fv) (_dv_B_V : Disjoint B.fv V.fv) (_dv_B_W : Disjoint B.fv W.fv) (dv_B_f : f ∉ B.fv) (dv_B_g : g ∉ B.fv) (dv_B_h : h ∉ B.fv) (_dv_V_W : Disjoint V.fv W.fv) (dv_f_g : f ≠ g) (dv_f_h : f ≠ h) (dv_g_h : g ≠ h) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWwpp.imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWfo (SemanticCore.Class.cv f) B A)) (Compiler.CompactSourceSyntax.synWex g (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv g) B A))).imp (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv h) A B)))))

Checked nominal proof certificate identified upstream as g_wppcg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnnzdf (y : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))

Checked nominal proof certificate identified upstream as g_nnnzdf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnnzex (y : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_nnnzex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fopprod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFoun (A B C D F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfo F A C) (Compiler.CompactSourceSyntax.synWfo G B D)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synCun F G) (Compiler.CompactSourceSyntax.synCun A B) (Compiler.CompactSourceSyntax.synCun C D)))

Checked nominal proof certificate identified upstream as g_foun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXnnex (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_xnnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPadsetex (x y v : SemanticCore.Var) (_dv_v_x : v ≠ x) (_dv_v_y : v ≠ y) (_dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_padsetex.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part007.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXnndisj (y : SemanticCore.Var) (X : SemanticCore.Class) (_dv_X_y : y ∉ X.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_xnndisj.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXnnun (y : SemanticCore.Var) (X : SemanticCore.Class) (_dv_X_y : y ∉ X.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))) (Compiler.CompactSourceSyntax.synCxp X Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_xnnun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSucnnf1o (y z : SemanticCore.Var) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCmpt z Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv z) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))

Checked nominal proof certificate identified upstream as g_sucnnf1o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPadontoex (x y v f : SemanticCore.Var) (F : SemanticCore.Class) (dv_F_f : f ∉ F.fv) (_dv_F_v : v ∉ F.fv) (_dv_F_x : x ∉ F.fv) (_dv_F_y : y ∉ F.fv) (dv_f_v : f ≠ v) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (_dv_v_x : v ≠ x) (_dv_v_y : v ≠ y) (_dv_x_y : x ≠ y) (hyp_padontoex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpprod F (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))) (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg)))) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg)))).imp (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWfo (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))))))

Checked nominal proof certificate identified upstream as g_padontoex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSucxpinjex (x y z v g : SemanticCore.Var) (dv_g_v : g ≠ v) (dv_g_x : g ≠ x) (dv_g_y : g ≠ y) (dv_g_z : g ≠ z) (_dv_v_x : v ≠ x) (_dv_v_y : v ≠ y) (_dv_v_z : v ≠ z) (_dv_x_y : x ≠ y) (_dv_x_z : x ≠ z) (_dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCmpt z Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv z) Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg)))).imp (Compiler.CompactSourceSyntax.synWex g (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))))))

Checked nominal proof certificate identified upstream as g_sucxpinjex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSucxpinj (y z : SemanticCore.Var) (V X : SemanticCore.Class) (_dv_V_X : Disjoint V.fv X.fv) (_dv_V_y : y ∉ V.fv) (_dv_V_z : z ∉ V.fv) (_dv_X_y : y ∉ X.fv) (_dv_X_z : z ∉ X.fv) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid X) (Compiler.CompactSourceSyntax.synCmpt z Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv z) Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synCxp X Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp V (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg))))

Checked nominal proof certificate identified upstream as g_sucxpinj.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppadonto (y : SemanticCore.Var) (F V X : SemanticCore.Class) (_dv_F_V : Disjoint F.fv V.fv) (_dv_F_X : Disjoint F.fv X.fv) (_dv_F_y : y ∉ F.fv) (_dv_V_X : Disjoint V.fv X.fv) (_dv_V_y : y ∉ V.fv) (dv_X_y : y ∉ X.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfo F X V).imp (Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpprod F (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))) (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg)))) (Compiler.CompactSourceSyntax.synCxp X Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp V (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp X (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg)))))

Checked nominal proof certificate identified upstream as g_wpppadonto.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1exco (t : SemanticCore.Var) (A B C : SemanticCore.Class) (h k : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_A_k : k ∉ A.fv) (dv_A_t : t ∉ A.fv) (dv_B_h : h ∉ B.fv) (_dv_B_k : k ∉ B.fv) (dv_B_t : t ∉ B.fv) (dv_C_h : h ∉ C.fv) (dv_C_k : k ∉ C.fv) (dv_C_t : t ∉ C.fv) (dv_h_k : h ≠ k) (dv_h_t : h ≠ t) (dv_k_t : k ≠ t) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv h) B C)) (Compiler.CompactSourceSyntax.synWex t (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv t) A B))).imp (Compiler.CompactSourceSyntax.synWex k (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) A C)))

Checked nominal proof certificate identified upstream as g_f1exco.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTaginjex (x y v t : SemanticCore.Var) (dv_t_v : t ≠ v) (_dv_t_x : t ≠ x) (_dv_t_y : t ≠ y) (_dv_v_x : v ≠ x) (_dv_v_y : v ≠ y) (_dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex t (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv t) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrab y Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC0c).neg)))))

Checked nominal proof certificate identified upstream as g_taginjex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQkrelbr (A B C : SemanticCore.Class) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (_dv_B_C : Disjoint B.fv C.fv) (hyp_qkrelbr_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_qkrelbr_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) (Compiler.CompactSourceSyntax.synCqkrel A)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B C) A))

Checked nominal proof certificate identified upstream as g_qkrelbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdmemval (C : SemanticCore.Class) (e : SemanticCore.Var) (_dv_C_e : e ∉ C.fv) (hyp_fdmemval_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synCfdmem) (SemanticCore.Wff.classMem C (SemanticCore.Class.cv e)))

Checked nominal proof certificate identified upstream as g_fdmemval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQkrelex (A : SemanticCore.Class) (hyp_qkrelex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCqkrel A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_qkrelex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fdmemex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fdprj0ex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fdprj1ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFddomex (A B : SemanticCore.Class) (hyp_fddomex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fddomex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfddom A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fddomex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFde0ex (A B : SemanticCore.Class) (hyp_fddomex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fddomex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfde0 A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fde0ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFde1ex (A B : SemanticCore.Class) (hyp_fddomex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fddomex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfde1 A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fde1ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdsepex (A B : SemanticCore.Class) (hyp_fddomex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fddomex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdsep A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdsepex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdliftex (R : SemanticCore.Class) (hyp_fdliftex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdlift R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdliftex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdnonminex (A B R : SemanticCore.Class) (hyp_fdnonminex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdnonminex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdnonminex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdnonmin R A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdnonminex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminsepex (A B R : SemanticCore.Class) (hyp_fdnonminex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdnonminex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdnonminex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdminsep R A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdminsepex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdliftval2 (x : SemanticCore.Var) (R : SemanticCore.Class) (e c d : SemanticCore.Var) (dv_R_c : c ∉ R.fv) (dv_R_d : d ∉ R.fv) (_dv_R_e : e ∉ R.fv) (_dv_R_x : x ∉ R.fv) (dv_c_d : c ≠ d) (dv_c_e : c ≠ e) (dv_c_x : c ≠ x) (dv_d_e : d ≠ e) (dv_d_x : d ≠ x) (_dv_e_x : e ≠ x) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e))) (Compiler.CompactSourceSyntax.synCfdlift R)) (Compiler.CompactSourceSyntax.synWex c (Compiler.CompactSourceSyntax.synWex d (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv c))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) R (SemanticCore.Class.cv d))))))

Checked nominal proof certificate identified upstream as g_fdliftval2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdliftval1 (x : SemanticCore.Var) (R : SemanticCore.Class) (e c : SemanticCore.Var) (dv_R_c : c ∉ R.fv) (dv_R_e : e ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_c_e : c ≠ e) (dv_c_x : c ≠ x) (dv_e_x : e ≠ x) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e))) (Compiler.CompactSourceSyntax.synCfdlift R)) (Compiler.CompactSourceSyntax.synWex c (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv c))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) R (SemanticCore.Class.cv e)))))

Checked nominal proof certificate identified upstream as g_fdliftval1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdmemvalC (B C : SemanticCore.Class) (e : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.classMem C B).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synCfdmem) (SemanticCore.Wff.classMem C (SemanticCore.Class.cv e))))

Checked nominal proof certificate identified upstream as g_fdmemvalC.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdprj0valV (x : SemanticCore.Var) (C D : SemanticCore.Class) (_dv_C_D : Disjoint C.fv D.fv) (_dv_C_x : x ∉ C.fv) (_dv_D_x : x ∉ D.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk C D)) Compiler.CompactSourceSyntax.synCfdprj0) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn C)))))

Checked nominal proof certificate identified upstream as g_fdprj0valV.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFde0valJp (A B C D : SemanticCore.Class) (e : SemanticCore.Var) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (_dv_A_D : Disjoint A.fv D.fv) (_dv_A_e : e ∉ A.fv) (_dv_B_C : Disjoint B.fv C.fv) (_dv_B_D : Disjoint B.fv D.fv) (_dv_B_e : e ∉ B.fv) (dv_C_D : Disjoint C.fv D.fv) (_dv_C_e : e ∉ C.fv) (_dv_D_e : e ∉ D.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synCfde0 A B)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A) (SemanticCore.Wff.classMem C (SemanticCore.Class.cv e)))))

Checked nominal proof certificate identified upstream as g_fde0valJp.

Equations

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