2011-11-16から1日間の記事一覧
今回は の帰納法による証明です.まず,左辺の和を # NSUM_CLAUSES_NUMSEG;; val it : thm = |- (!m. nsum (m..0) f = (if m = 0 then f 0 else 0)) /\ (!m n. nsum (m..SUC n) f = (if m という性質を持つnsumで表すと,goalは # g(`!n. nsum(0..n)(\k.2*k)…
今回は の帰納法による証明です.まず,左辺の和を # NSUM_CLAUSES_NUMSEG;; val it : thm = |- (!m. nsum (m..0) f = (if m = 0 then f 0 else 0)) /\ (!m n. nsum (m..SUC n) f = (if m という性質を持つnsumで表すと,goalは # g(`!n. nsum(0..n)(\k.2*k)…