各システムにおける実数の扱いが平明に記されています． http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf

以前 Isar で書いた自然数の分解 http://d.hatena.ne.jp/ehito/20130514/1368492752 の PVS 版です． lem_odd_even:lemma forall(n:nat):(n=0 or exists(x:posint,y:nat):odd?(x) & n=x*2^y) %|- lem_odd_even : PROOF %|- (then (induct "n" 1 "NAT_inducti…