2011-12-25から1日間の記事一覧
今回は,虚数と整数とが混在する証明です.変数はintとし,&,real_of_int,num_of_intを介して各ドメインの性質を適用します.なお,SOS系の利用はできるだけ控えました. needs "Complex/make.ml";;let lemma04 = prove (`!a b:real. (?x. ~( x = Cx(&1) )…
今回は,虚数と整数とが混在する証明です.変数はintとし,&,real_of_int,num_of_intを介して各ドメインの性質を適用します.なお,SOS系の利用はできるだけ控えました. needs "Complex/make.ml";;let lemma04 = prove (`!a b:real. (?x. ~( x = Cx(&1) )…