Example (16-2)

最終的に

# let thm20120104_4=MESON[thm20120104]`!d:num. !c:num->int. (!n:num. ?p:num. isum (0..d) (\i. c i * &n pow i) = &p /\ prime p) ==> (?p:num. !n:num. isum (0..d) (\i. c i * &n pow i) = &p /\ prime p)`;;
0..0..0..1..3..7..13..26..41..70..102..188..289..511..768..1251..1794..2831..419
9..6606..9520..14315..20148..solved at 22495
val thm20120104_4 : thm =
|- !d c.
(!n. ?p. isum (0..d) (\i. c i * &n pow i) = &p /\ prime p)
==> (?p. !n. isum (0..d) (\i. c i * &n pow i) = &p /\ prime p)

のようにまとめました．