PVSのこと(2)
一般項が分数である数列の和です.NASA製の (grind-reals) が要です.
pvsファイル
frseq:theory begin importing reals@sigma_posnat lem01:lemma FORALL (n: posnat): sigma(1, n, (LAMBDA (k: posnat): 1 / (k * (k + 1)))) = n / (n + 1) %|- lem01 : PROOF %|- (then (induct-and-simplify "n" 1 :defs T :if-match best) (grind-reals)) %|- QED end frseq
*PVS*バッファ
pvs(1190): Installing rewrite rule sets.singleton_rew (all instances) lem01 : |------- {1} FORALL (n: posnat): sigma(1, n, (LAMBDA (k: posnat): 1 / (k * (k + 1)))) = n / (n + 1) Rule? (induct-and-simplify "n" 1 :defs T :if-match best) sigma rewrites sigma(1, 1 + j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) to sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) + 1 / (2 + j!1 * j!1 + 3 * j!1) sigma rewrites sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) to 0 By induction on n, and by repeatedly rewriting and simplifying, this simplifies to: lem01 : {-1} sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) = j!1 / (1 + j!1) {-2} 1 + j!1 > 0 |------- {1} sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) + 1 / (2 + j!1 * j!1 + 3 * j!1) = (1 + j!1) / (2 + j!1) Rule? (grind-reals) div_cancel4 rewrites sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) = j!1 / (1 + j!1) to TRUE div_cancel4 rewrites sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) + 1 / (2 + j!1 * j!1 + 3 * j!1) = (1 + j!1) / (2 + j!1) to 2 * sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) + sigma(1, j!1, (LAMBDA (k: posnat): 1 / (k + k * k))) * j!1 + (2 * (1 / (2 + j!1 * j!1 + 3 * j!1)) + (1 / (2 + j!1 * j!1 + 3 * j!1)) * j!1) = 1 + j!1 Applying grind-reals, Q.E.D.
latexでの出力