2014-06-27から1日間の記事一覧
http://d.hatena.ne.jp/ehito/20111119/1321692292 のPVS版です. lem00:lemma FORALL (p: pred [nat]): (FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)) IMPLIES (FORALL (n: nat): p(n)) %|- lem00 : PROOF %|- (then (skeep*) (c…