PVSのこと（２）

　一般項が分数である数列の和です．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での出力