leon

0熱

1答えて

溶接機での作業中に、私はその証拠に私がsitutationに直面：コンテンツ（L1）==コンテンツ（L2）及びfはべき等、連想と可換演算子次いで倍（F、Zである場合倍（F：、L1）は、私は、フォームのxのリストL1のためにあることを示したかった私の証明の1つの段階で）（F、Z、L2を折る:: XS = 、（x、xs）== fold（f、z、without（x、l2））ここで、without（

0熱

1答えて

Welderで二重誘導を実行する

Welderを使用して二重誘導によって特性を証明しようとしています。定義はhereから取られます。理論の詳細を与える関連する質問はhereで見つけることができます。とにかく私は問題を表示するためにいくつかの部分が必要です。基本的には、整数の形をとる式POP(i,p)とPOW(i,p,q)を使って作業しています。それらには通常の性質があり、それをnと呼ぶ。私はそれを証明したい場合n(x) && n

0熱

1答えて

私はイノックスソルバーインターフェースで、次のScalaの階層をモデル化するイノックス

でクラス階層のモデル化： abstract class Element() abstract class nonZero() extends Element final case class Zero() extends Element final case class One() extends nonZero() final case class notOne() extends no

0熱

1答えて

溶接機でnotIを使用する。例矛盾の証明

WelderでnotI構造を使用しているときにいくつか問題があります。私の例では、リングの構造と、リングa0 = 0 = 0aのすべての 'a'についての派生した補題（zeroDivisorLemma）について通常の補題を使用しています。 2つの要素がゼロでない場合、その積はゼロではないことを証明します。次のように。 val theorem: Theorem = forallI("a"