Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part047.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpstrictminndv (y u : SemanticCore.Var) (A : SemanticCore.Class) (q : SemanticCore.Var) (_dv_A_q : q ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_q_u : q ≠ u) (dv_q_y : q ≠ y) (dv_u_y : u ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv q) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWrex u (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synWral y (SemanticCore.Class.cv q) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) (SemanticCore.Class.cv u)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_hncodecmpstrictminndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpstrictfrndv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) Compiler.CompactSourceSyntax.synCfound (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hncodecmpstrictfrndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part048.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmplnpwcndv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synClnpwc (Compiler.CompactSourceSyntax.synChwcn A))))

Checked nominal proof certificate identified upstream as g_hncodecmplnpwcndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordlnquoeqimndv (A : SemanticCore.Class) (r : SemanticCore.Var) (_dv_A_r : r ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnker (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synChwniso A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnquo (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synChnord A)))

Checked nominal proof certificate identified upstream as g_hnordlnquoeqimndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordwendv (A : SemanticCore.Class) (s : SemanticCore.Var) (dv_A_s : s ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWex s (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv s) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synChnord A))))

Checked nominal proof certificate identified upstream as g_hnordwendv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part049.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardhwcardsndv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncard A) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_hncardhwcardsndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6canonicaltchomndv (X : SemanticCore.Class) (hyp_wppconcrete6canonicaltchomndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc X))))))))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc X))))))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6canonicaltchomndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtc6oneeqndv : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))))

Checked nominal proof certificate identified upstream as g_hncardtc6oneeqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtc7oneeqndv : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))))

Checked nominal proof certificate identified upstream as g_hncardtc7oneeqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6thresholdtclecndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6thresholdtclecndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwpw1argclcndv (C D : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCpw1 D)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni C) D) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni C)))))

Checked nominal proof certificate identified upstream as g_hnwpw1argclcndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppsifnndv (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn F A).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_wppsifnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpptxpfnvalndv (x : SemanticCore.Var) (A F G : SemanticCore.Class) (_dv_A_x : x ∉ A.fv) (_dv_F_x : x ∉ F.fv) (_dv_G_x : x ∉ G.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCtxp F G) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv G (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_wpptxpfnvalndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part050.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1xpshiftsetndv (A B : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_B_p : p ∉ B.fv) (hyp_pw1xpshiftsetndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_pw1xpshiftsetndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCmpt p (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_pw1xpshiftsetndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part051.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1xpshiftenndv (A B : SemanticCore.Class) (hyp_pw1xpshiftenndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_pw1xpshiftenndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCpw1 B)))

Checked nominal proof certificate identified upstream as g_pw1xpshiftenndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelpw1shiftenndv (X : SemanticCore.Class) (hyp_wppqkrelpw1shiftenndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxpk X X)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 X) (Compiler.CompactSourceSyntax.synCpw1 X)))

Checked nominal proof certificate identified upstream as g_wppqkrelpw1shiftenndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitshiftenndv (X : SemanticCore.Class) (hyp_wpplitshiftenndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 X) (Compiler.CompactSourceSyntax.synCpw1 X)) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_wpplitshiftenndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part052.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6dmrepdndv (x z : SemanticCore.Var) (dv_x_z : x ≠ z) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn)).imp (Compiler.CompactSourceSyntax.synWex z (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv z)))))))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6dmrepdndv.

Equations

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