Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part043.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandleastreundv (ph : SemanticCore.Wff) (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (dv_C_m : m ∉ C.fv) (dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_k_m : k ≠ m) (_dv_k_ph : k ∉ ph.fv) (_dv_m_ph : m ∉ ph.fv) (hyp_wppcandleastreundv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex m (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWreu m (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))

Checked nominal proof certificate identified upstream as g_wppcandleastreundv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammaminpackndv (ph : SemanticCore.Wff) (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (dv_C_m : m ∉ C.fv) (dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_k_m : k ≠ m) (dv_k_ph : k ∉ ph.fv) (dv_m_ph : m ∉ ph.fv) (hyp_wppgammaminpackndv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex m (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma F C) (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCwppgamma F C) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))

Checked nominal proof certificate identified upstream as g_wppgammaminpackndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammaminhwndv (C : SemanticCore.Class) (k : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (dv_F_k : k ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma F C) (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCwppgamma F C) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))

Checked nominal proof certificate identified upstream as g_wppgammaminhwndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppcardtfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardtfnvalndv (q : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppcardtfn (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_wppcardtfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardtfnmapndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf Compiler.CompactSourceSyntax.synCwppcardtfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppcardtfnmapndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part044.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardtfnf1ndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 Compiler.CompactSourceSyntax.synCwppcardtfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppcardtfnf1ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardtfnvalsingndv (D : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCncs).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppcardtfn (Compiler.CompactSourceSyntax.synCsn D)) (Compiler.CompactSourceSyntax.synCtc D)))

Checked nominal proof certificate identified upstream as g_wppcardtfnvalsingndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachorbitextcbidv (x : SemanticCore.Var) (C D F G : SemanticCore.Class) (r p a : SemanticCore.Var) (dv_C_a : a ∉ C.fv) (dv_C_p : p ∉ C.fv) (dv_D_a : a ∉ D.fv) (dv_D_p : p ∉ D.fv) (dv_D_r : r ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_F_a : a ∉ F.fv) (dv_F_p : p ∉ F.fv) (dv_F_r : r ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_G_a : a ∉ G.fv) (dv_G_p : p ∉ G.fv) (dv_G_x : x ∉ G.fv) (dv_a_p : a ≠ p) (dv_a_r : a ≠ r) (hyp_wppreachorbitextcbidv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachorbitextcbidv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachorbitextcbidv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachorbitextcbidv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachorbitextcbidv_5 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc D) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachorbitextcbidv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachorbitextcbidv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) (hyp_wppreachorbitextcbidv_8 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)) (hyp_wppreachorbitextcbidv_9 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral r Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCncs))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex a Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv a)))) (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCtc D)) (SemanticCore.Class.cv p)))))

Checked nominal proof certificate identified upstream as g_wppreachorbitextcbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachorbitfnvndv (C F : SemanticCore.Class) (hyp_wppreachorbitfnvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_wppreachorbitfnvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwppreachvndv (C D : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_D_n : n ∉ D.fv) (dv_F_n : n ∉ F.fv) (hyp_elwppreachvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach F C)) (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_elwppreachvndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part045.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppnnstageextcbidv (D H : SemanticCore.Class) (p a : SemanticCore.Var) (dv_D_a : a ∉ D.fv) (dv_D_p : p ∉ D.fv) (dv_H_a : a ∉ H.fv) (dv_H_p : p ∉ H.fv) (dv_a_p : a ≠ p) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex a Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv a)))) (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv H (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p))))))

Checked nominal proof certificate identified upstream as g_wppnnstageextcbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachtcrexvndv (C D : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_D_n : n ∉ D.fv) (dv_F_n : n ∉ F.fv) (hyp_wppreachtcrexvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach F C)) (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_wppreachtcrexvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachlayerorbvndv (C D F N : SemanticCore.Class) (hyp_wppreachlayerorbvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachlayerorbvndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachlayerorbvndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachlayerorbvndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc N))) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) N))))

Checked nominal proof certificate identified upstream as g_wppreachlayerorbvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachlayerorbrexvndv (C D : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (_dv_C_n : n ∉ C.fv) (_dv_D_n : n ∉ D.fv) (_dv_F_n : n ∉ F.fv) (hyp_wppreachlayerorbrexvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachlayerorbrexvndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachlayerorbrexvndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachlayerorbrexvndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv n))))) (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_wppreachlayerorbrexvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachfwdrexvndv (C D : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_D_n : n ∉ D.fv) (dv_F_n : n ∉ F.fv) (hyp_wppreachfwdrexvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachfwdrexvndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachfwdrexvndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachfwdrexvndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach F C)) (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_wppreachfwdrexvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachtcbidv (x : SemanticCore.Var) (C D F G : SemanticCore.Class) (r : SemanticCore.Var) (dv_D_r : r ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_F_r : r ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_G_x : x ∉ G.fv) (hyp_wppreachtcbidv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachtcbidv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachtcbidv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachtcbidv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachtcbidv_5 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc D) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachtcbidv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachtcbidv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) (hyp_wppreachtcbidv_8 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)) (hyp_wppreachtcbidv_9 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral r Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCncs))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach F C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc D) (Compiler.CompactSourceSyntax.synCwppreach G (Compiler.CompactSourceSyntax.synCtc C))))

Checked nominal proof certificate identified upstream as g_wppreachtcbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwcardsweclndv (K : SemanticCore.Class) (s d : SemanticCore.Var) (dv_K_d : d ∉ K.fv) (dv_K_s : s ∉ K.fv) (dv_d_s : d ≠ s) : Nominal.NPrf ((SemanticCore.Wff.classMem K Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem K (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWex d (Compiler.CompactSourceSyntax.synWex s (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv s) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv d)) (SemanticCore.Wff.classEq K (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv d))))))))

Checked nominal proof certificate identified upstream as g_elhwcardsweclndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part046.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcardstcclndv (K : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem K (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc K) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_hwcardstcclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcardsdownltcndv (C : SemanticCore.Class) (d : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv d) Compiler.CompactSourceSyntax.synClec C)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_hwcardsdownltcndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part047.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammaimagetceqndv (C : SemanticCore.Class) (k : SemanticCore.Var) (F G : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_d : d ∉ C.fv) (dv_C_k : k ∉ C.fv) (dv_F_d : d ∉ F.fv) (dv_F_k : k ∉ F.fv) (_dv_G_d : d ∉ G.fv) (dv_G_k : k ∉ G.fv) (dv_d_k : d ≠ k) (hyp_wppgammaimagetceqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppgammaimagetceqndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppgammaimagetceqndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)) (hyp_wppgammaimagetceqndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc C) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppgammaimagetceqndv_5 : Nominal.NPrf (SemanticCore.Wff.all k (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwppcand G (Compiler.CompactSourceSyntax.synCtc C))) (Compiler.CompactSourceSyntax.synWrex d (Compiler.CompactSourceSyntax.synCwppcand F C) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv d))))))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma F C)) (Compiler.CompactSourceSyntax.synCwppgamma G (Compiler.CompactSourceSyntax.synCtc C)))

Checked nominal proof certificate identified upstream as g_wppgammaimagetceqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammareachndv (C F : SemanticCore.Class) (hyp_wppgammareachndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppgammareachndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma F C) (Compiler.CompactSourceSyntax.synCwppreach F C))

Checked nominal proof certificate identified upstream as g_wppgammareachndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitexvndv (C F I : SemanticCore.Class) (hyp_wpphitexvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpphit F I C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpphitexvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwpphitvndv (C F I N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwpphit F I C)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N)))))

Checked nominal proof certificate identified upstream as g_elwpphitvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitminexvndv (x : SemanticCore.Var) (C S : SemanticCore.Class) (m n : SemanticCore.Var) (F I : SemanticCore.Class) (dv_C_m : m ∉ C.fv) (dv_C_n : n ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_I_m : m ∉ I.fv) (dv_I_n : n ∉ I.fv) (dv_I_x : x ∉ I.fv) (dv_S_m : m ∉ S.fv) (dv_S_n : n ∉ S.fv) (_dv_S_x : x ∉ S.fv) (dv_m_n : m ≠ n) (dv_m_x : m ≠ x) (dv_n_x : n ≠ x) (hyp_wpphitminexvndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCwpphit F I C)))).imp (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwpphit F I C)) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F I C)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) S (SemanticCore.Class.cv n)))))))

Checked nominal proof certificate identified upstream as g_wpphitminexvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwpphitsucvndv (C F I N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCwpphit F I C)) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N)))))

Checked nominal proof certificate identified upstream as g_elwpphitsucvndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitnestptndv (F H I L N : SemanticCore.Class) (_dv_F_N : Disjoint F.fv N.fv) (_dv_I_N : Disjoint I.fv N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem L Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem H Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N) Compiler.CompactSourceSyntax.synCncs)) (Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec H))).imp ((SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwpphit F I H)).imp (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwpphit F I L))))

Checked nominal proof certificate identified upstream as g_wpphitnestptndv.

Equations

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