2013-06-29から1日間の記事一覧
HOL系と異なり,PVS の number system は数学と同じく,サブセットからなっていますので numsys1:lemma forall(a:nat): exists(x:real): x=a numsys2:lemma forall(a:nat): exists(x:rat): x=a numsys3:lemma forall(a:nat): exists(x:int): x=a numsys4:lem…
HOL系と異なり,PVS の number system は数学と同じく,サブセットからなっていますので numsys1:lemma forall(a:nat): exists(x:real): x=a numsys2:lemma forall(a:nat): exists(x:rat): x=a numsys3:lemma forall(a:nat): exists(x:int): x=a numsys4:lem…