PVSのこと（４）

　(grind) は中々です．

pvsファイル

nnseq:theory begin
importing reals@sigma_nat
a:[nat->nnreal]
n:nat
lem01:lemma sigma(0,n,a)>=0
lem02:lemma sigma(0,n,a)=0 => a(n)=0
%|- lem0* : PROOF
%|- (grind)
%|- QED
end nnseq

＊PVS＊バッファ

pvs(1160): 
Installing rewrite rule sets.singleton_rew (all instances)
Installing rewrite rule reals@sigma_nat.sigma_0_neg


lem01 :  

  |-------
{1}   sigma(0, n, a) >= 0

Rule? (grind)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.




Run time  = 0.04 secs.
Real time = 2.10 secs.

nil
pvs(1167): 
Installing rewrite rule sets.singleton_rew (all instances)
Installing rewrite rule reals@sigma_nat.sigma_0_neg


lem02 :  

  |-------
{1}   (sigma(0, n, a) = 0 => a(n) = 0)

Rule? (grind)
sigma rewrites sigma(0, n, a)
  to a(n) + sigma(0, n - 1, a)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.




Run time  = 0.06 secs.
Real time = 1.58 secs.

nil