proof

1熱

1答えて

2n^2 - 2n -7 = O（n^2）、nが1または2のとき、f（n）の負の値を持つことを証明する必要があります。私はBig-Oが正しいことを証明する方法はわかりません。あなたの助けと助言は高く評価されます。 f(n) = 2n^2 - 2n -7 = O(n^2) if c=2; n=1->2(1)^2 - 2(1) -7 = -7 <= 2*(1)^2

0熱

1答えて

`replace`を使ってこの可換性の証拠を完成させるには？

thisのドキュメントには、replaceを使用して証明を完成させる方法が記載されていますが、rewriteが使用されています。これはreplaceという文章砂糖のようです。私はそれを明示的に使用する方法を理解することに興味があります。私が正しく理解していれば、反射性によって証明可能となり、k = plus k 0という証拠与えられ、S (plus k 0) = S (plus k 0)としてS

0熱

2答えて

平面内で最も近い複数のペアの決定

以下に概略を示す掃引アルゴリズムを使用して平面内の最も近い頂点のペアを決定する場合、追加の実行を行わずに複数のペアを決定できますか？ x座標に応じてポイントをソートします。ポイントのセットを垂直線x = xmidで2つの等しいサイズのサブセットに分割します。問題を再帰的に左右のサブセットで解決します。これにより、それぞれ左側および右側の最小距離dLminおよびdRminが得られる。 1組のポイ

0熱

1答えて

SPARK.Text_IO手順の前提条件は、私が2017年</p> <p>私の問題SPARKの発見にspark_io例からSPARK.Text_IOを使用してい

を開催することを証明する方法はSPARK.Text_IO手順の多くは、前提条件を持っていることであるIどのようにして証明しようとするのかわからない、すなわち標準入力が読み込み可能であり、ファイルの終わりではないということです。私の試みは、以下のコードに示されているように、SPARK.Text_IOプロシージャ（この場合はGet_Immediate）の前提条件を呼び出し側プロシージャの前提条件に追加

0熱

2答えて

ビッグオメガ機能

私は（nはない）、nの大きなオメガサイズと機能のN0を見つけようとしているの証明^ 3ここで、c = 2.25（）= 3^3から39^2 + （）がΩ（^ 3）であることを証明するためには、0≥0となるような0> 0の定数が必要である。もしc = 2.25ならば、 n0を満たす最小の整数？最初の考えは、n> 0なのでn = 1であり、不等式が働いていればn = 1は最小のn（したがってn0）に

0熱

1答えて

Prooving N-1と呼ば回

これは問題から擬似コードである： Procedure Foo(A,f,L)、前提条件： A [f..L]の配列であります整数 f、Lはf < = Lの2つの自然数> = 1です。コード procedure Foo(A,f,L if (f=L) then return A[f] else m <-- [(f+L)/2] return

0熱

2答えて

Agdaで偶数のn倍の偶数が得られることを証明する

Agda で1.nn∈sumをn *（n + 1）/ 2として定義しようとしており、n * （n + 1）はそのためである。証明はかなりシンプルですが、私はAgdaを初めて使っているので（理解もしていない概念もあるようです）、http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf からもっと学んでいます。）。 open import

2熱

1答えて

Coq on Coinduction、タイプミスマッチ

私はコインシデンスタイプを試していましたし、自然数とベクトル（型のサイズがリスト）のコインシデンスバージョンを定義することに決めました。私は彼らとように無限の数に定義： CoInductive conat : Set := | cozero : conat | cosuc : conat -> conat. CoInductive covec (A : Set) : conat -> Se

-1熱

1答えて

複雑な小文字の証拠

以下の質問は宿題として与えられます。私はそれを解決しようとどんなに困難になったとしても、私は解決策に達することができませんでした。問題は、与えられた関数aが、set-little（b）の要素であるかどうかを調べる。 show that n^(ln(ln(ln(n)))) is o(ceiling(ln(n))!) 興味深いのは、階乗演算子!がnの隣が、ceiling(ln(x))にだけではなく