Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part068.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopgammacontrgrowthstagedndv (x y : SemanticCore.Var) (C F : SemanticCore.Class) (p : SemanticCore.Var) (dv_C_p : p ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_F_p : p ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_p_x : p ≠ x) (dv_p_y : p ≠ y) (dv_x_y : x ≠ y) (hyp_wppstopgammacontrgrowthstagedndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopgammacontrgrowthstagedndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopgammacontrgrowthstagedndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopgammacontrgrowthstagedndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec C)) (hyp_wppstopgammacontrgrowthstagedndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F))))) (hyp_wppstopgammacontrgrowthstagedndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) (hyp_wppstopgammacontrgrowthstagedndv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv y)))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C)) ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) (SemanticCore.Class.cv y))))).imp (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synC0c).neg)

Checked nominal proof certificate identified upstream as g_wppstopgammacontrgrowthstagedndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part069.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6globalnonfixedfromhnshiftndv (y : SemanticCore.Var) (hyp_wppconcrete6globalnonfixedfromhnshiftndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))))).neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (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 (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6globalnonfixedfromhnshiftndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6rnhwcardsndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn Compiler.CompactSourceSyntax.synCwppconcrete6fn) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wppconcrete6rnhwcardsndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6thresholdhwcardsndv : Nominal.NPrf (SemanticCore.Wff.classMem (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.synChwcards Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wppconcrete6thresholdhwcardsndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6stoppedtchomfullndv (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep 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.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6stoppedtchomfullndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part070.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6stoppedgammacontrgrowthstagedndv (y : SemanticCore.Var) (hyp_wppconcrete6stoppedgammacontrgrowthstagedndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))))).neg) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (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.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 (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWbr (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.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) (SemanticCore.Class.cv y))))).imp (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synC0c).neg)

Checked nominal proof certificate identified upstream as g_wppconcrete6stoppedgammacontrgrowthstagedndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodeselfnoisoclndv (x : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B))).imp (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) (SemanticCore.Class.cv x))).neg)

Checked nominal proof certificate identified upstream as g_hnwcutcodeselfnoisoclndv.

Equations

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