Дан ряд не более чем из 30 камней, которые могут быть как черными, так и белыми. В начале игры не допускаются пробелы, но камней может быть меньше 30. Цель состоит в том, чтобы удалить все камни. Убрать можно только черные камни, если убрать...

Только начинаю изучать большой и асимптотический анализ, и я застрял на этом конкретном доказательстве: Как мы можем доказать, что 2^n равно O(n!)? Спасибо

У меня возникли проблемы с доказательством свойств бинарного дерева с помощью индукции: Property 1 - A tree with N internal nodes has a maximum height of N+1 base case - 0 internal nodes has a height of 0 assume - a tree with k internal...

Иногда, когда я пишу доказательства в стиле применения, мне нужен способ изменить метод доказательства foo , чтобы Попробуйте foo на первой цели. Если это решает цель, хорошо; если это не решает ее, вернуться в исходное состояние и...

Я решаю задачу от codeforces . Наша задача состоит в том, чтобы найти минимальную стоимость, чтобы данная целочисленная последовательность была неубывающей. Мы можем увеличивать/уменьшать любое число последовательности на 1 на каждом шаге и это...

У меня есть следующее доказательство для оператора if p then q (p --> q) наоборот: p --> q == ~q --> ~p противоречие: ~q --> p покажите контрпример противоречия от противного ~q --> ~p == True противопоставлением p --> q == true Это...

Я хочу доказать это: 1 subgoals x : nat y : nat z : nat ______________________________________(1/1) x + y - z = x + (y - z) Это выглядит тривиально, но меня это сильно смущает, и мне это нужно для еще одного доказательства. Спасибо.

Я новичок в coq и пытаюсь это доказать ... Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> (b = c). Вот мое доказательство, но я застреваю, когда добираюсь до цели (false = true -> false = true). Proof. intros b...

Докажите, что пересечение двух языков, разрешимых по Тьюрингу, является разрешимым по Тьюрингу. (Зная алгоритмы для определения каждого языка, опишите алгоритм для определения того, принадлежит ли строка пересечению.) Я знаю, что язык разрешим по...

Я следую официальному руководству по Liquid Haskell и наткнулся на то, что кажется "баг" в нем. Следующий код присутствует в руководстве , а Liquid Haskell был должен проверить, что это безопасно. {-@ type TRUE = {v:Bool | v } @-} {-@...

Я пытаюсь доказать следующую лемму: forall (A B : Type) (f : A -> B) (l : list A) (y : B), In y (map f l) <-> exists x, f x = y /\ In x l. Я начинаю с расщепления, чтобы обработать первое направление, затем провожу индукцию...

Предположим, у меня есть лемма L , в которой говорится forall x, x + 1 + 1 = x + 2. Если моя цель имеет вид a + 1 + 1 = b Я могу написать команду rewrite L , чтобы получить цель вида a + 2 = b Однако, если моя цель имеет форму a...

Я должен доказать тривиальность, используя классы типов: class order = fixes lesseq :: " 'a ⇒ 'a ⇒ bool" (infix "≼" 50) assumes refl: "x ≼ x" and trans: "x ≼ y ⟹ y ≼ z ⟹ x ≼ z" and...

Я пытаюсь реализовать версию Isabelle / JEdit для командной строки, чтобы Запустите сервер Isabelle на другом докере / машине Разрешить интеграцию большего количества редакторов, таких как Vim или Emacs Разрешить автоматизированным агентам...

Я пытаюсь доказать следующую теорему после формализации лямбда-исчисления с индексами Дебройна и заменой в Coq. Theorem atom_equality : forall e : expression , forall x : nat, (beta_reduction (Var x) e) -> (e = Var x). и это определения...