1. FormalConjectures
  2. Mathoverflow
  3. «75792»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Mathoverflow 75792

Various questions about integer complexity, which is the minimum number of 1s needed to express a natural number using addition, multiplication, and parentheses.

Let ‖n‖ denote the integer complexity of n > 0.

    It is known that ‖3^n‖ = 3n for n > 0.

    Is it true that ‖2^n‖ = 2n for n > 0?

    The corresponding conjecture for 5 is false, because 5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

We have chosen to formalise this using an inductive type.

References:

    mathoverflow/75792 by user Harry Altman

    http://arxiv.org/abs/1203.6462 by Jānis Iraids, Kaspars Balodis, Juris Čerņenoks, Mārtiņš Opmanis, Rihards Opmanis, Kārlis Podnieks

    http://arxiv.org/abs/1207.4841 by Harry Altman, Joshua Zelinsky

    https://oeis.org/A5245 : Mahler-Popken complexity.

namespace Mathoverflow75792

The inductively defined predicate that m is reachable in n steps.

inductive Reachable : ℕ → ℕ → Prop | one : Reachable 1 1 | add {m n a b} : Reachable m a → Reachable n b → Reachable (m + n) (a + b) | mul {m n a b} : Reachable m a → Reachable n b → Reachable (m * n) (a + b) @[category test, AMS 11] theorem Reachable.self (n : ℕ) (hn : 0 < n) : Reachable n n := Nat.le_induction .one (fun _ _ ih ↦ .add ih .one) n hn @[category test, AMS 11] theorem not_reachable_zero_fst (n : ℕ) : ¬ Reachable 0 n := n:ℕ⊢ ¬Reachable 0 n n:ℕh:Reachable 0 n⊢ False; n:ℕm:ℕhm:0 = mh:Reachable m n⊢ False; induction h with n:ℕm:ℕhm:0 = 1⊢ False exact absurd hm (n:ℕm:ℕhm:0 = 1⊢ ¬0 = 1 All goals completed! 🐙) n:ℕm:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = m✝ → Falsea_ih✝:0 = n✝ → Falsehm:0 = m✝ + n✝⊢ False n:ℕm:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = m✝ → Falsea_ih✝:0 = n✝ → Falsehm:m✝ = 0 ∧ n✝ = 0⊢ False; All goals completed! 🐙 n:ℕm:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = m✝ → Falsea_ih✝:0 = n✝ → Falsehm:0 = m✝ * n✝⊢ False n:ℕm:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = m✝ → Falsea_ih✝:0 = n✝ → Falsehm:m✝ = 0 ∨ n✝ = 0⊢ False; All goals completed! 🐙 @[category test, AMS 11] theorem not_reachable_zero_snd (m : ℕ) : ¬ Reachable m 0 := m:ℕ⊢ ¬Reachable m 0 m:ℕh:Reachable m 0⊢ False; m:ℕn:ℕhn:0 = nh:Reachable m n⊢ False; induction h with m:ℕn:ℕhn:0 = 1⊢ False exact absurd hn (m:ℕn:ℕhn:0 = 1⊢ ¬0 = 1 All goals completed! 🐙) m:ℕn:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = a✝ → Falsea_ih✝:0 = b✝ → Falsehn:0 = a✝ + b✝⊢ False m:ℕn:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = a✝ → Falsea_ih✝:0 = b✝ → Falsehn:a✝ = 0 ∧ b✝ = 0⊢ False; All goals completed! 🐙 m:ℕn:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = a✝ → Falsea_ih✝:0 = b✝ → Falsehn:0 = a✝ + b✝⊢ False m:ℕn:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = a✝ → Falsea_ih✝:0 = b✝ → Falsehn:a✝ = 0 ∧ b✝ = 0⊢ False; All goals completed! 🐙 @[category test, AMS 11] theorem Reachable.dec {m n : ℕ} (h : Reachable m n) : ∃ m' n', m' + 1 = m ∧ n' + 1 = n := m:ℕn:ℕh:Reachable m n⊢ ∃ m' n', m' + 1 = m ∧ n' + 1 = n n:ℕh:Reachable 0 n⊢ ∃ m' n', m' + 1 = 0 ∧ n' + 1 = nn:ℕm:ℕh:Reachable (m + 1) n⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = n n:ℕh:Reachable 0 n⊢ ∃ m' n', m' + 1 = 0 ∧ n' + 1 = n All goals completed! 🐙 m:ℕh:Reachable (m + 1) 0⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = 0m:ℕn:ℕh:Reachable (m + 1) (n + 1)⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = n + 1 m:ℕh:Reachable (m + 1) 0⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = 0 All goals completed! 🐙 All goals completed! 🐙 @[category test, AMS 11] theorem Reachable.le {m n₁ n₂ : ℕ} (hn : n₁ ≤ n₂) (hm : Reachable m n₁) : Reachable m n₂ := m:ℕn₁:ℕn₂:ℕhn:n₁ ≤ n₂hm:Reachable m n₁⊢ Reachable m n₂ induction hn with m:ℕn₁:ℕn₂:ℕhm:Reachable m n₁⊢ Reachable m n₁ All goals completed! 🐙 m:ℕn₁:ℕn₂:ℕhm:Reachable m n₁m✝:ℕh:n₁.le m✝ih:Reachable m m✝⊢ Reachable m m✝.succ m:ℕn₁:ℕn₂:ℕhm:Reachable m n₁m✝:ℕh:n₁.le m✝ih:Reachable m m✝⊢ m = m * 1; All goals completed! 🐙 @[category test, AMS 11] theorem reachable_iff_of_two_le (m n : ℕ) (hm : 2 ≤ m) : Reachable m n ↔ ∃ m₁, ∃ _ : m₁ < m, ∃ m₂, ∃ _ : m₂ < m, ∃ n₁, ∃ _ : n₁ < n, ∃ n₂, ∃ _ : n₂ < n, n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m ∨ m₁ * m₂ = m) := m:ℕn:ℕhm:2 ≤ m⊢ Reachable m n ↔ ∃ m₁, ∃ (_ : m₁ < m), ∃ m₂, ∃ (_ : m₂ < m), ∃ n₁, ∃ (_ : n₁ < n), ∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m ∨ m₁ * m₂ = m) m:ℕn:ℕhm:2 ≤ mhmn:Reachable m n⊢ ∃ m₁, ∃ (_ : m₁ < m), ∃ m₂, ∃ (_ : m₂ < m), ∃ n₁, ∃ (_ : n₁ < n), ∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m ∨ m₁ * m₂ = m) induction hmn with m:ℕn:ℕhm:2 ≤ 1⊢ ∃ m₁, ∃ (_ : m₁ < 1), ∃ m₂, ∃ (_ : m₂ < 1), ∃ n₁, ∃ (_ : n₁ < 1), ∃ n₂, ∃ (_ : n₂ < 1), n₁ + n₂ = 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 1 ∨ m₁ * m₂ = 1) exact absurd hm (m:ℕn:ℕhm:2 ≤ 1⊢ ¬2 ≤ 1 All goals completed! 🐙) m:ℕn:ℕm₃:ℕm₄:ℕn₃:ℕn₄:ℕh₁:Reachable m₃ n₃h₂:Reachable m₄ n₄ih₁:2 ≤ m₃ → ∃ m₁, ∃ (_ : m₁ < m₃), ∃ m₂, ∃ (_ : m₂ < m₃), ∃ n₁, ∃ (_ : n₁ < n₃), ∃ n₂, ∃ (_ : n₂ < n₃), n₁ + n₂ = n₃ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ ∨ m₁ * m₂ = m₃)ih₂:2 ≤ m₄ → ∃ m₁, ∃ (_ : m₁ < m₄), ∃ m₂, ∃ (_ : m₂ < m₄), ∃ n₁, ∃ (_ : n₁ < n₄), ∃ n₂, ∃ (_ : n₂ < n₄), n₁ + n₂ = n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ ∨ m₁ * m₂ = m₄)hm:2 ≤ m₃ + m₄⊢ ∃ m₁, ∃ (_ : m₁ < m₃ + m₄), ∃ m₂, ∃ (_ : m₂ < m₃ + m₄), ∃ n₁, ∃ (_ : n₁ < n₃ + n₄), ∃ n₂, ∃ (_ : n₂ < n₃ + n₄), n₁ + n₂ = n₃ + n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + m₄ ∨ m₁ * m₂ = m₃ + m₄) m:ℕn:ℕm₄:ℕn₄:ℕh₂:Reachable m₄ n₄ih₂:2 ≤ m₄ → ∃ m₁, ∃ (_ : m₁ < m₄), ∃ m₂, ∃ (_ : m₂ < m₄), ∃ n₁, ∃ (_ : n₁ < n₄), ∃ n₂, ∃ (_ : n₂ < n₄), n₁ + n₂ = n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ ∨ m₁ * m₂ = m₄)m₃:ℕn₃:ℕhm:2 ≤ m₃ + 1 + m₄h₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + m₄), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + m₄), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + n₄), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + n₄), n₁ + n₂ = n₃ + 1 + n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + m₄ ∨ m₁ * m₂ = m₃ + 1 + m₄) m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + (m₄ + 1)), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + (m₄ + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + (m₄ + 1) ∨ m₁ * m₂ = m₃ + 1 + (m₄ + 1)) m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ m₃ + 1 < m₃ + 1 + (m₄ + 1)m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ m₄ + 1 < m₃ + 1 + (m₄ + 1)m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ n₃ + 1 < n₃ + 1 + (n₄ + 1)m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ n₄ + 1 < n₃ + 1 + (n₄ + 1) m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ m₃ + 1 < m₃ + 1 + (m₄ + 1)m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ m₄ + 1 < m₃ + 1 + (m₄ + 1)m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ n₃ + 1 < n₃ + 1 + (n₄ + 1)m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ m₃ + 1 + (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ n₄ + 1 < n₃ + 1 + (n₄ + 1) All goals completed! 🐙 m:ℕn:ℕm₃:ℕm₄:ℕn₃:ℕn₄:ℕh₁:Reachable m₃ n₃h₂:Reachable m₄ n₄ih₁:2 ≤ m₃ → ∃ m₁, ∃ (_ : m₁ < m₃), ∃ m₂, ∃ (_ : m₂ < m₃), ∃ n₁, ∃ (_ : n₁ < n₃), ∃ n₂, ∃ (_ : n₂ < n₃), n₁ + n₂ = n₃ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ ∨ m₁ * m₂ = m₃)ih₂:2 ≤ m₄ → ∃ m₁, ∃ (_ : m₁ < m₄), ∃ m₂, ∃ (_ : m₂ < m₄), ∃ n₁, ∃ (_ : n₁ < n₄), ∃ n₂, ∃ (_ : n₂ < n₄), n₁ + n₂ = n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ ∨ m₁ * m₂ = m₄)hm:2 ≤ m₃ * m₄⊢ ∃ m₁, ∃ (_ : m₁ < m₃ * m₄), ∃ m₂, ∃ (_ : m₂ < m₃ * m₄), ∃ n₁, ∃ (_ : n₁ < n₃ + n₄), ∃ n₂, ∃ (_ : n₂ < n₃ + n₄), n₁ + n₂ = n₃ + n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ * m₄ ∨ m₁ * m₂ = m₃ * m₄) m:ℕn:ℕm₄:ℕn₄:ℕh₂:Reachable m₄ n₄ih₂:2 ≤ m₄ → ∃ m₁, ∃ (_ : m₁ < m₄), ∃ m₂, ∃ (_ : m₂ < m₄), ∃ n₁, ∃ (_ : n₁ < n₄), ∃ n₂, ∃ (_ : n₂ < n₄), n₁ + n₂ = n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ ∨ m₁ * m₂ = m₄)m₃:ℕn₃:ℕhm:2 ≤ (m₃ + 1) * m₄h₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (m₃ + 1) * m₄), ∃ m₂, ∃ (_ : m₂ < (m₃ + 1) * m₄), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + n₄), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + n₄), n₁ + n₂ = n₃ + 1 + n₄ ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (m₃ + 1) * m₄ ∨ m₁ * m₂ = (m₃ + 1) * m₄) m:ℕn:ℕm₃:ℕn₃:ℕh₁:Reachable (m₃ + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 ∨ m₁ * m₂ = m₃ + 1)m₄:ℕn₄:ℕhm:2 ≤ (m₃ + 1) * (m₄ + 1)h₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (m₃ + 1) * (m₄ + 1)), ∃ m₂, ∃ (_ : m₂ < (m₃ + 1) * (m₄ + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (m₃ + 1) * (m₄ + 1) ∨ m₁ * m₂ = (m₃ + 1) * (m₄ + 1)) m:ℕn:ℕn₃:ℕm₄:ℕn₄:ℕh₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)h₁:Reachable (0 + 1) (n₃ + 1)ih₁:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (0 + 1) * (m₄ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (0 + 1) * (m₄ + 1)), ∃ m₂, ∃ (_ : m₂ < (0 + 1) * (m₄ + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (0 + 1) * (m₄ + 1) ∨ m₁ * m₂ = (0 + 1) * (m₄ + 1))m:ℕn:ℕn₃:ℕm₄:ℕn₄:ℕh₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)m₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (m₃ + 1 + 1) * (m₄ + 1)), ∃ m₂, ∃ (_ : m₂ < (m₃ + 1 + 1) * (m₄ + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (m₃ + 1 + 1) * (m₄ + 1) ∨ m₁ * m₂ = (m₃ + 1 + 1) * (m₄ + 1)) m:ℕn:ℕn₃:ℕm₄:ℕn₄:ℕh₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)h₁:Reachable (0 + 1) (n₃ + 1)ih₁:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (0 + 1) * (m₄ + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (0 + 1) * (m₄ + 1)), ∃ m₂, ∃ (_ : m₂ < (0 + 1) * (m₄ + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (0 + 1) * (m₄ + 1) ∨ m₁ * m₂ = (0 + 1) * (m₄ + 1)) obtain ⟨m₅, hm₅, m₆, hm₆, n₅, hn₅, n₆, hn₆, h₃, h₄, h₅, h₆⟩ := ih₂ (m:ℕn:ℕn₃:ℕm₄:ℕn₄:ℕh₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)h₁:Reachable (0 + 1) (n₃ + 1)ih₁:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (0 + 1) * (m₄ + 1)⊢ 2 ≤ m₄ + 1 All goals completed! 🐙) refine ⟨m₅, ?_, m₆, ?_, n₅+n₃+1, ?_, n₆, ?_, m:ℕn:ℕn₃:ℕm₄:ℕn₄:ℕh₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)h₁:Reachable (0 + 1) (n₃ + 1)ih₁:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (0 + 1) * (m₄ + 1)m₅:ℕhm₅:m₅ < m₄ + 1m₆:ℕhm₆:m₆ < m₄ + 1n₅:ℕhn₅:n₅ < n₄ + 1n₆:ℕhn₆:n₆ < n₄ + 1h₃:n₅ + n₆ = n₄ + 1h₄:Reachable m₅ n₅h₅:Reachable m₆ n₆h₆:m₅ + m₆ = m₄ + 1 ∨ m₅ * m₆ = m₄ + 1⊢ n₅ + n₃ + 1 + n₆ = n₃ + 1 + (n₄ + 1) m:ℕn:ℕn₃:ℕm₄:ℕn₄:ℕh₂:Reachable (m₄ + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 ∨ m₁ * m₂ = m₄ + 1)h₁:Reachable (0 + 1) (n₃ + 1)ih₁:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (0 + 1) * (m₄ + 1)m₅:ℕhm₅:m₅ < m₄ + 1m₆:ℕhm₆:m₆ < m₄ + 1n₅:ℕhn₅:n₅ < n₄ + 1n₆:ℕhn₆:n₆ < n₄ + 1h₃:n₅ + n₆ = n₄ + 1h₄:Reachable m₅ n₅h₅:Reachable m₆ n₆h₆:m₅ + m₆ = m₄ + 1 ∨ m₅ * m₆ = m₄ + 1⊢ n₅ + n₃ + 1 + n₆ = n₃ + 1 + (n₅ + n₆); All goals completed! 🐙, h₄.le ?_, h₅, ?_⟩ all_goals All goals completed! 🐙 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)h₂:Reachable (0 + 1) (n₄ + 1)ih₂:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (m₃ + 1 + 1) * (0 + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (m₃ + 1 + 1) * (0 + 1)), ∃ m₂, ∃ (_ : m₂ < (m₃ + 1 + 1) * (0 + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (m₃ + 1 + 1) * (0 + 1) ∨ m₁ * m₂ = (m₃ + 1 + 1) * (0 + 1))m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (m₃ + 1 + 1) * (m₄ + 1 + 1)), ∃ m₂, ∃ (_ : m₂ < (m₃ + 1 + 1) * (m₄ + 1 + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (m₃ + 1 + 1) * (m₄ + 1 + 1) ∨ m₁ * m₂ = (m₃ + 1 + 1) * (m₄ + 1 + 1)) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)h₂:Reachable (0 + 1) (n₄ + 1)ih₂:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (m₃ + 1 + 1) * (0 + 1)⊢ ∃ m₁, ∃ (_ : m₁ < (m₃ + 1 + 1) * (0 + 1)), ∃ m₂, ∃ (_ : m₂ < (m₃ + 1 + 1) * (0 + 1)), ∃ n₁, ∃ (_ : n₁ < n₃ + 1 + (n₄ + 1)), ∃ n₂, ∃ (_ : n₂ < n₃ + 1 + (n₄ + 1)), n₁ + n₂ = n₃ + 1 + (n₄ + 1) ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = (m₃ + 1 + 1) * (0 + 1) ∨ m₁ * m₂ = (m₃ + 1 + 1) * (0 + 1)) obtain ⟨m₅, hm₅, m₆, hm₆, n₅, hn₅, n₆, hn₆, h₃, h₄, h₅, h₆⟩ := ih₁ (m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)h₂:Reachable (0 + 1) (n₄ + 1)ih₂:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (m₃ + 1 + 1) * (0 + 1)⊢ 2 ≤ m₃ + 1 + 1 All goals completed! 🐙) refine ⟨m₅, ?_, m₆, ?_, n₅, ?_, n₆+n₄+1, ?_, m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)h₂:Reachable (0 + 1) (n₄ + 1)ih₂:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (m₃ + 1 + 1) * (0 + 1)m₅:ℕhm₅:m₅ < m₃ + 1 + 1m₆:ℕhm₆:m₆ < m₃ + 1 + 1n₅:ℕhn₅:n₅ < n₃ + 1n₆:ℕhn₆:n₆ < n₃ + 1h₃:n₅ + n₆ = n₃ + 1h₄:Reachable m₅ n₅h₅:Reachable m₆ n₆h₆:m₅ + m₆ = m₃ + 1 + 1 ∨ m₅ * m₆ = m₃ + 1 + 1⊢ n₅ + (n₆ + n₄ + 1) = n₃ + 1 + (n₄ + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)h₂:Reachable (0 + 1) (n₄ + 1)ih₂:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (m₃ + 1 + 1) * (0 + 1)m₅:ℕhm₅:m₅ < m₃ + 1 + 1m₆:ℕhm₆:m₆ < m₃ + 1 + 1n₅:ℕhn₅:n₅ < n₃ + 1n₆:ℕhn₆:n₆ < n₃ + 1h₃:n₅ + n₆ = n₃ + 1h₄:Reachable m₅ n₅h₅:Reachable m₆ n₆h₆:m₅ + m₆ = m₃ + 1 + 1 ∨ m₅ * m₆ = m₃ + 1 + 1⊢ n₅ + (n₆ + n₄ + 1) = n₅ + n₆ + (n₄ + 1); All goals completed! 🐙, h₄, h₅.le ?_, ?_⟩ all_goals All goals completed! 🐙 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₃ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1)m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₄ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1)m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ n₃ + 1 < n₃ + 1 + (n₄ + 1)m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ n₄ + 1 < n₃ + 1 + (n₄ + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₃ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₃ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₄ + 1 + 1 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₃ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₄ + 1 + 1 All goals completed! 🐙 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₄ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₄ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₃ + 1 + 1 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₄ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₃ + 1 + 1 All goals completed! 🐙 all_goals All goals completed! 🐙 instance Reachable.decide : ∀ m n, Decidable (Reachable m n) | 0, n => isFalse (not_reachable_zero_fst n) | 1, 0 => isFalse (not_reachable_zero_snd 1) | 1, n+1 => isTrue (Reachable.one.le (n:ℕ⊢ 1 ≤ n + 1 All goals completed! 🐙)) m:ℕn:ℕ⊢ Decidable (Reachable (m + 2) n) m:ℕn:ℕ⊢ Decidable (Reachable (m + 2) n) m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ n⊢ Decidable (Reachable (m + 2) n) refine @decidable_of_iff' _ _ (reachable_iff_of_two_le (m+2) n (m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ n⊢ 2 ≤ m + 2 All goals completed! 🐙)) ?_ m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ nm₁:ℕhm₁:m₁ < m + 2⊢ Decidable (∃ m₂, ∃ (_ : m₂ < m + 2), ∃ n₁, ∃ (_ : n₁ < n), ∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ nm₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2⊢ Decidable (∃ n₁, ∃ (_ : n₁ < n), ∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ nm₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < n⊢ Decidable (∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ nm₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < nn₂:ℕhn₂:n₂ < n⊢ Decidable (n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ nm₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < nn₂:ℕhn₂:n₂ < n⊢ Decidable (Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) m:ℕn:ℕd:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} => decide m₁ nm₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < nn₂:ℕhn₂:n₂ < n⊢ Decidable (Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) All goals completed! 🐙

The (Mahler-Popken) complexity of n: the minimum number of 1s needed to express a given number using only addition and multiplication. E.g. 2 = 1 + 1, so complexity 2 = 2.

def complexity (n : ℕ) : ℕ := if h : n = 0 then 0 else Nat.find ⟨n, Reachable.self n <| n.pos_of_ne_zero h⟩ @[category test, AMS 11] theorem Reachable.complexity_le {m n : ℕ} (h : Reachable m n) : complexity m ≤ n := m:ℕn:ℕh:Reachable m n⊢ complexity m ≤ n m:ℕn:ℕh:Reachable m n⊢ (if h : m = 0 then 0 else Nat.find ⋯) ≤ n m:ℕn:ℕh:Reachable m nh':m = 0⊢ 0 ≤ nm:ℕn:ℕh:Reachable m nh':¬m = 0⊢ Nat.find ⋯ ≤ n m:ℕn:ℕh:Reachable m nh':m = 0⊢ 0 ≤ n n:ℕh:Reachable 0 n⊢ 0 ≤ n; All goals completed! 🐙 All goals completed! 🐙 @[category test, AMS 11] theorem Reachable.complexity_eq {m n : ℕ} (h : Reachable m n) (min : ∀ n' < n, ¬ Reachable m n') : complexity m = n := m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'⊢ complexity m = n m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'⊢ n ≤ complexity m m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'⊢ n ≤ if h : m = 0 then 0 else Nat.find ⋯ m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'h':m = 0⊢ n ≤ 0m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'h':¬m = 0⊢ n ≤ Nat.find ⋯ m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'h':m = 0⊢ n ≤ 0 n:ℕh:Reachable 0 nmin:∀ n' < n, ¬Reachable 0 n'⊢ n ≤ 0; All goals completed! 🐙 All goals completed! 🐙 @[category test, AMS 11] theorem Reachable.complexity {n : ℕ} (hn : 0 < n) : Reachable n (complexity n) := n:ℕhn:0 < n⊢ Reachable n (Mathoverflow75792.complexity n) n:ℕhn:0 < n⊢ Reachable n (if h : n = 0 then 0 else Nat.find ⋯) n:ℕhn:0 < n⊢ Reachable n (Nat.find ⋯) All goals completed! 🐙 @[category test, AMS 11] theorem complexity_zero : complexity 0 = 0 := rfl @[category test, AMS 11] theorem complexity_one : complexity 1 = 1 := Reachable.one.complexity_eq fun n' hn' ↦ n':ℕhn':n' < 1⊢ ¬Reachable 1 n' have : n' = 0 := n':ℕhn':n' < 1⊢ ¬Reachable 1 n' All goals completed! 🐙 hn':0 < 1⊢ ¬Reachable 1 0; All goals completed! 🐙 @[category test, AMS 11] theorem complexity_two : complexity 2 = 2 := (Reachable.add .one .one).complexity_eq fun n' hn' ↦ n':ℕhn':n' < 1 + 1⊢ ¬Reachable (1 + 1) n' n':ℕhn':0 < 1 + 1⊢ ¬Reachable (1 + 1) 0n':ℕhn':1 < 1 + 1⊢ ¬Reachable (1 + 1) 1 n':ℕhn':0 < 1 + 1⊢ ¬Reachable (1 + 1) 0 All goals completed! 🐙 n':ℕhn':1 < 1 + 1⊢ ¬Reachable (1 + 1) 1 n':ℕhn':1 < 1 + 1⊢ ¬∃ m₁, ∃ (_ : m₁ < 2), ∃ m₂, ∃ (_ : m₂ < 2), ∃ n₁, ∃ (_ : n₁ < 1), ∃ n₂, ∃ (_ : n₂ < 1), n₁ + n₂ = 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 2 ∨ m₁ * m₂ = 2) n':ℕhn':1 < 1 + 1m₁:ℕhm₁:m₁ < 2m₂:ℕhm₂:m₂ < 2n₁:ℕhn₁:n₁ < 1n₂:ℕhn₂:n₂ < 1h₁:n₁ + n₂ = 1⊢ False All goals completed! 🐙 @[category test, AMS 11] theorem Reachable.pow (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : Reachable (m ^ n) (m * n) := m:ℕn:ℕhm:0 < mhn:0 < n⊢ Reachable (m ^ n) (m * n) induction hn with m:ℕn:ℕhm:0 < m⊢ Reachable (m ^ Nat.succ 0) (m * Nat.succ 0) m:ℕn:ℕhm:0 < m⊢ m ^ Nat.succ 0 = mm:ℕn:ℕhm:0 < m⊢ m * Nat.succ 0 = m m:ℕn:ℕhm:0 < m⊢ m ^ Nat.succ 0 = mm:ℕn:ℕhm:0 < m⊢ m * Nat.succ 0 = m All goals completed! 🐙 m:ℕn:ℕhm:0 < mm✝:ℕhn:(Nat.succ 0).le m✝ih:Reachable (m ^ m✝) (m * m✝)⊢ Reachable (m ^ m✝.succ) (m * m✝.succ) All goals completed! 🐙 @[category test, AMS 11] theorem Reachable.pow' (m n : ℕ+) : Reachable (m ^ (n : ℕ) : ℕ) (m * n) := .pow _ _ m.pos n.pos

5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

@[category test, AMS 11] theorem Reachable.five_pow_six : Reachable (5^6) 29 := have h8 : Reachable 8 6 := .pow' 2 3 have h9 : Reachable 9 6 := .pow' 3 2 have h27 : Reachable 27 9 := .pow' 3 3 .add .one <| .mul h8 <| .mul h9 <| .add .one <| .mul h8 h27

Is 5n the complexity of 5^n for 0 < n? Answer: No.

@[category research solved, AMS 11] theorem complexity_five_pow : answer(False) ↔ ∀ n : ℕ, 0 < n → complexity (5 ^ n) = 5 * n := ⊢ False ↔ ∀ (n : ℕ), 0 < n → complexity (5 ^ n) = 5 * n ⊢ False ↔ ∀ (n : ℕ), 0 < n → complexity (5 ^ n) = 5 * n ⊢ ∃ x, 0 < x ∧ ¬complexity (5 ^ x) = 5 * x exact ⟨6, ⊢ 0 < 6 All goals completed! 🐙, fun h ↦ absurd (h ▸ Reachable.five_pow_six.complexity_le) (h:complexity (5 ^ 6) = 5 * 6⊢ ¬5 * 6 ≤ 29 All goals completed! 🐙)⟩

Is 3n the complexity of 3^n for 0 < n? Answer: Yes, by John Selfridge.

Reference: https://arxiv.org/abs/1207.4841

@[category research solved, AMS 11] theorem declaration uses 'sorry'complexity_three_pow : answer(True) ↔ ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n := ⊢ True ↔ ∀ (n : ℕ), 0 < n → complexity (3 ^ n) = 3 * n All goals completed! 🐙

Is 2n the complexity of 2^n for 0 < n?

@[category research open, AMS 11] theorem declaration uses 'sorry'complexity_two_pow : answer(sorry) ↔ ∀ n : ℕ, 0 < n → complexity (2 ^ n) = 2 * n := ⊢ True ↔ ∀ (n : ℕ), 0 < n → complexity (2 ^ n) = 2 * n All goals completed! 🐙 end Mathoverflow75792