1. FormalConjectures
  2. ErdosProblems
  3. «44»
/- 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

Erdős Problem 44: Extending Sidon Sets

Reference: erdosproblems.com/44

open Function Set Finset namespace Erdos44

The maximum size of a Sidon set in {1, ..., N} is less than or equal to 2 * √N.

@[category textbook, AMS 5 11] theorem declaration uses 'sorry'maxSidonSubsetCard_icc_bound (N : ℕ) (hN : 1 ≤ N) : maxSidonSubsetCard (Icc 1 N) ≤ 2 * Real.sqrt N := N:ℕhN:1 ≤ N⊢ ↑(Finset.Icc 1 N).maxSidonSubsetCard ≤ 2 * √↑N All goals completed! 🐙

Erdős Problem 44: Let N ≥ 1 and A ⊆ {1,…,N} be a Sidon set. Is it true that, for any ε > 0, there exist M = M(ε) and B ⊆ {N+1,…,M} such that A ∪ B ⊆ {1,…,M} is a Sidon set of size at least (1−ε)M^{1/2}?

This problem asks whether any Sidon set can be extended to achieve a density arbitrarily close to the optimal density for Sidon sets.

@[category research open, AMS 5 11] theorem declaration uses 'sorry'erdos_44 : answer(sorry) ↔ ∀ᵉ (N ≥ (1 : ℕ)) (A ⊆ Finset.Icc 1 N), IsSidon (A : Set ℕ) → ∀ᵉ (ε > (0 : ℝ)), ∃ᵉ (M > N) (B ⊆ Finset.Icc (N + 1) M), IsSidon (A ∪ B : Set ℕ) ∧ (1 - ε) * Real.sqrt M ≤ (A ∪ B).card := ⊢ True ↔ ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon ↑A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (↑A ∪ ↑B) ∧ (1 - ε) * √↑M ≤ ↑(#(A ∪ B)) All goals completed! 🐙

The case where we start with an empty set (constructing large Sidon sets).

@[category research open, AMS 5 11] theorem declaration uses 'sorry'erdos_44.variants.empty_start : answer(sorry) ↔ ∀ᵉ (ε > (0 : ℝ)), ∀ᶠ (M : ℕ) in Filter.atTop, ∃ᵉ (A ⊆ Finset.Icc 1 M), IsSidon (A : Set ℕ) ∧ (1 - ε) * Real.sqrt M ≤ A.card := ⊢ True ↔ ∀ ε > 0, ∀ᶠ (M : ℕ) in Filter.atTop, ∃ A ⊆ Finset.Icc 1 M, IsSidon ↑A ∧ (1 - ε) * √↑M ≤ ↑(#A) All goals completed! 🐙

The set {1, 2, 4, 8, 13} is a Sidon set in {1, ..., 13}.

@[category textbook, AMS 5 11] theorem example_sidon_set : IsSidon ({1, 2, 4, 8, 13} : Set ℕ) := ⊢ IsSidon {1, 2, 4, 8, 13} intro i₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}⊢ ∀ j₁ ∈ {1, 2, 4, 8, 13}, ∀ i₂ ∈ {1, 2, 4, 8, 13}, ∀ j₂ ∈ {1, 2, 4, 8, 13}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕ⊢ j₁ ∈ {1, 2, 4, 8, 13} → ∀ i₂ ∈ {1, 2, 4, 8, 13}, ∀ j₂ ∈ {1, 2, 4, 8, 13}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕhj₁:j₁ ∈ {1, 2, 4, 8, 13}⊢ ∀ i₂ ∈ {1, 2, 4, 8, 13}, ∀ j₂ ∈ {1, 2, 4, 8, 13}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕhj₁:j₁ ∈ {1, 2, 4, 8, 13}i₂:ℕ⊢ i₂ ∈ {1, 2, 4, 8, 13} → ∀ j₂ ∈ {1, 2, 4, 8, 13}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕhj₁:j₁ ∈ {1, 2, 4, 8, 13}i₂:ℕhi₂:i₂ ∈ {1, 2, 4, 8, 13}⊢ ∀ j₂ ∈ {1, 2, 4, 8, 13}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕhj₁:j₁ ∈ {1, 2, 4, 8, 13}i₂:ℕhi₂:i₂ ∈ {1, 2, 4, 8, 13}j₂:ℕ⊢ j₂ ∈ {1, 2, 4, 8, 13} → i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕhj₁:j₁ ∈ {1, 2, 4, 8, 13}i₂:ℕhi₂:i₂ ∈ {1, 2, 4, 8, 13}j₂:ℕhj₂:j₂ ∈ {1, 2, 4, 8, 13}⊢ i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕhi₁:i₁ ∈ {1, 2, 4, 8, 13}j₁:ℕhj₁:j₁ ∈ {1, 2, 4, 8, 13}i₂:ℕhi₂:i₂ ∈ {1, 2, 4, 8, 13}j₂:ℕhj₂:j₂ ∈ {1, 2, 4, 8, 13}hsum:i₁ + i₂ = j₁ + j₂⊢ i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ i₁:ℕj₁:ℕi₂:ℕj₂:ℕhsum:i₁ + i₂ = j₁ + j₂hi₁:i₁ = 1 ∨ i₁ = 2 ∨ i₁ = 4 ∨ i₁ = 8 ∨ i₁ = 13hj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13⊢ i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = j₁ + j₂⊢ 1 = j₁ ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = j₁ + j₂⊢ 2 = j₁ ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = j₁ + j₂⊢ 4 = j₁ ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = j₁ + j₂⊢ 8 = j₁ ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = j₁ + j₂⊢ 13 = j₁ ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = j₁ j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = j₁ + j₂⊢ 1 = j₁ ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = j₁ + j₂⊢ 2 = j₁ ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = j₁ + j₂⊢ 4 = j₁ ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = j₁ + j₂⊢ 8 = j₁ ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = j₁j₁:ℕi₂:ℕj₂:ℕhj₁:j₁ = 1 ∨ j₁ = 2 ∨ j₁ = 4 ∨ j₁ = 8 ∨ j₁ = 13hi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = j₁ + j₂⊢ 13 = j₁ ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = j₁ i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 1 + j₂⊢ 13 = 1 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 1i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 2 + j₂⊢ 13 = 2 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 2i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 4 + j₂⊢ 13 = 4 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 4i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 8 + j₂⊢ 13 = 8 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 8i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 13 + j₂⊢ 13 = 13 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 13 i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = 1 + j₂⊢ 1 = 1 ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = 1i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = 2 + j₂⊢ 1 = 2 ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = 2i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = 4 + j₂⊢ 1 = 4 ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = 4i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = 8 + j₂⊢ 1 = 8 ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = 8i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + i₂ = 13 + j₂⊢ 1 = 13 ∧ i₂ = j₂ ∨ 1 = j₂ ∧ i₂ = 13i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = 1 + j₂⊢ 2 = 1 ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = 1i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = 2 + j₂⊢ 2 = 2 ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = 2i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = 4 + j₂⊢ 2 = 4 ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = 4i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = 8 + j₂⊢ 2 = 8 ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = 8i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + i₂ = 13 + j₂⊢ 2 = 13 ∧ i₂ = j₂ ∨ 2 = j₂ ∧ i₂ = 13i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = 1 + j₂⊢ 4 = 1 ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = 1i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = 2 + j₂⊢ 4 = 2 ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = 2i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = 4 + j₂⊢ 4 = 4 ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = 4i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = 8 + j₂⊢ 4 = 8 ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = 8i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + i₂ = 13 + j₂⊢ 4 = 13 ∧ i₂ = j₂ ∨ 4 = j₂ ∧ i₂ = 13i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = 1 + j₂⊢ 8 = 1 ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = 1i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = 2 + j₂⊢ 8 = 2 ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = 2i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = 4 + j₂⊢ 8 = 4 ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = 4i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = 8 + j₂⊢ 8 = 8 ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = 8i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + i₂ = 13 + j₂⊢ 8 = 13 ∧ i₂ = j₂ ∨ 8 = j₂ ∧ i₂ = 13i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 1 + j₂⊢ 13 = 1 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 1i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 2 + j₂⊢ 13 = 2 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 2i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 4 + j₂⊢ 13 = 4 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 4i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 8 + j₂⊢ 13 = 8 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 8i₂:ℕj₂:ℕhi₂:i₂ = 1 ∨ i₂ = 2 ∨ i₂ = 4 ∨ i₂ = 8 ∨ i₂ = 13hj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + i₂ = 13 + j₂⊢ 13 = 13 ∧ i₂ = j₂ ∨ 13 = j₂ ∧ i₂ = 13 j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 1 = 13 + j₂⊢ 13 = 13 ∧ 1 = j₂ ∨ 13 = j₂ ∧ 1 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 2 = 13 + j₂⊢ 13 = 13 ∧ 2 = j₂ ∨ 13 = j₂ ∧ 2 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 4 = 13 + j₂⊢ 13 = 13 ∧ 4 = j₂ ∨ 13 = j₂ ∧ 4 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 8 = 13 + j₂⊢ 13 = 13 ∧ 8 = j₂ ∨ 13 = j₂ ∧ 8 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 13 = 13 + j₂⊢ 13 = 13 ∧ 13 = j₂ ∨ 13 = j₂ ∧ 13 = 13 j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 1 = 1 + j₂⊢ 1 = 1 ∧ 1 = j₂ ∨ 1 = j₂ ∧ 1 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 2 = 1 + j₂⊢ 1 = 1 ∧ 2 = j₂ ∨ 1 = j₂ ∧ 2 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 4 = 1 + j₂⊢ 1 = 1 ∧ 4 = j₂ ∨ 1 = j₂ ∧ 4 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 8 = 1 + j₂⊢ 1 = 1 ∧ 8 = j₂ ∨ 1 = j₂ ∧ 8 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 13 = 1 + j₂⊢ 1 = 1 ∧ 13 = j₂ ∨ 1 = j₂ ∧ 13 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 1 = 2 + j₂⊢ 1 = 2 ∧ 1 = j₂ ∨ 1 = j₂ ∧ 1 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 2 = 2 + j₂⊢ 1 = 2 ∧ 2 = j₂ ∨ 1 = j₂ ∧ 2 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 4 = 2 + j₂⊢ 1 = 2 ∧ 4 = j₂ ∨ 1 = j₂ ∧ 4 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 8 = 2 + j₂⊢ 1 = 2 ∧ 8 = j₂ ∨ 1 = j₂ ∧ 8 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 13 = 2 + j₂⊢ 1 = 2 ∧ 13 = j₂ ∨ 1 = j₂ ∧ 13 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 1 = 4 + j₂⊢ 1 = 4 ∧ 1 = j₂ ∨ 1 = j₂ ∧ 1 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 2 = 4 + j₂⊢ 1 = 4 ∧ 2 = j₂ ∨ 1 = j₂ ∧ 2 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 4 = 4 + j₂⊢ 1 = 4 ∧ 4 = j₂ ∨ 1 = j₂ ∧ 4 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 8 = 4 + j₂⊢ 1 = 4 ∧ 8 = j₂ ∨ 1 = j₂ ∧ 8 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 13 = 4 + j₂⊢ 1 = 4 ∧ 13 = j₂ ∨ 1 = j₂ ∧ 13 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 1 = 8 + j₂⊢ 1 = 8 ∧ 1 = j₂ ∨ 1 = j₂ ∧ 1 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 2 = 8 + j₂⊢ 1 = 8 ∧ 2 = j₂ ∨ 1 = j₂ ∧ 2 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 4 = 8 + j₂⊢ 1 = 8 ∧ 4 = j₂ ∨ 1 = j₂ ∧ 4 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 8 = 8 + j₂⊢ 1 = 8 ∧ 8 = j₂ ∨ 1 = j₂ ∧ 8 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 13 = 8 + j₂⊢ 1 = 8 ∧ 13 = j₂ ∨ 1 = j₂ ∧ 13 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 1 = 13 + j₂⊢ 1 = 13 ∧ 1 = j₂ ∨ 1 = j₂ ∧ 1 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 2 = 13 + j₂⊢ 1 = 13 ∧ 2 = j₂ ∨ 1 = j₂ ∧ 2 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 4 = 13 + j₂⊢ 1 = 13 ∧ 4 = j₂ ∨ 1 = j₂ ∧ 4 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 8 = 13 + j₂⊢ 1 = 13 ∧ 8 = j₂ ∨ 1 = j₂ ∧ 8 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:1 + 13 = 13 + j₂⊢ 1 = 13 ∧ 13 = j₂ ∨ 1 = j₂ ∧ 13 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 1 = 1 + j₂⊢ 2 = 1 ∧ 1 = j₂ ∨ 2 = j₂ ∧ 1 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 2 = 1 + j₂⊢ 2 = 1 ∧ 2 = j₂ ∨ 2 = j₂ ∧ 2 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 4 = 1 + j₂⊢ 2 = 1 ∧ 4 = j₂ ∨ 2 = j₂ ∧ 4 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 8 = 1 + j₂⊢ 2 = 1 ∧ 8 = j₂ ∨ 2 = j₂ ∧ 8 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 13 = 1 + j₂⊢ 2 = 1 ∧ 13 = j₂ ∨ 2 = j₂ ∧ 13 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 1 = 2 + j₂⊢ 2 = 2 ∧ 1 = j₂ ∨ 2 = j₂ ∧ 1 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 2 = 2 + j₂⊢ 2 = 2 ∧ 2 = j₂ ∨ 2 = j₂ ∧ 2 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 4 = 2 + j₂⊢ 2 = 2 ∧ 4 = j₂ ∨ 2 = j₂ ∧ 4 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 8 = 2 + j₂⊢ 2 = 2 ∧ 8 = j₂ ∨ 2 = j₂ ∧ 8 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 13 = 2 + j₂⊢ 2 = 2 ∧ 13 = j₂ ∨ 2 = j₂ ∧ 13 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 1 = 4 + j₂⊢ 2 = 4 ∧ 1 = j₂ ∨ 2 = j₂ ∧ 1 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 2 = 4 + j₂⊢ 2 = 4 ∧ 2 = j₂ ∨ 2 = j₂ ∧ 2 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 4 = 4 + j₂⊢ 2 = 4 ∧ 4 = j₂ ∨ 2 = j₂ ∧ 4 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 8 = 4 + j₂⊢ 2 = 4 ∧ 8 = j₂ ∨ 2 = j₂ ∧ 8 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 13 = 4 + j₂⊢ 2 = 4 ∧ 13 = j₂ ∨ 2 = j₂ ∧ 13 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 1 = 8 + j₂⊢ 2 = 8 ∧ 1 = j₂ ∨ 2 = j₂ ∧ 1 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 2 = 8 + j₂⊢ 2 = 8 ∧ 2 = j₂ ∨ 2 = j₂ ∧ 2 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 4 = 8 + j₂⊢ 2 = 8 ∧ 4 = j₂ ∨ 2 = j₂ ∧ 4 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 8 = 8 + j₂⊢ 2 = 8 ∧ 8 = j₂ ∨ 2 = j₂ ∧ 8 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 13 = 8 + j₂⊢ 2 = 8 ∧ 13 = j₂ ∨ 2 = j₂ ∧ 13 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 1 = 13 + j₂⊢ 2 = 13 ∧ 1 = j₂ ∨ 2 = j₂ ∧ 1 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 2 = 13 + j₂⊢ 2 = 13 ∧ 2 = j₂ ∨ 2 = j₂ ∧ 2 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 4 = 13 + j₂⊢ 2 = 13 ∧ 4 = j₂ ∨ 2 = j₂ ∧ 4 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 8 = 13 + j₂⊢ 2 = 13 ∧ 8 = j₂ ∨ 2 = j₂ ∧ 8 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:2 + 13 = 13 + j₂⊢ 2 = 13 ∧ 13 = j₂ ∨ 2 = j₂ ∧ 13 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 1 = 1 + j₂⊢ 4 = 1 ∧ 1 = j₂ ∨ 4 = j₂ ∧ 1 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 2 = 1 + j₂⊢ 4 = 1 ∧ 2 = j₂ ∨ 4 = j₂ ∧ 2 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 4 = 1 + j₂⊢ 4 = 1 ∧ 4 = j₂ ∨ 4 = j₂ ∧ 4 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 8 = 1 + j₂⊢ 4 = 1 ∧ 8 = j₂ ∨ 4 = j₂ ∧ 8 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 13 = 1 + j₂⊢ 4 = 1 ∧ 13 = j₂ ∨ 4 = j₂ ∧ 13 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 1 = 2 + j₂⊢ 4 = 2 ∧ 1 = j₂ ∨ 4 = j₂ ∧ 1 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 2 = 2 + j₂⊢ 4 = 2 ∧ 2 = j₂ ∨ 4 = j₂ ∧ 2 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 4 = 2 + j₂⊢ 4 = 2 ∧ 4 = j₂ ∨ 4 = j₂ ∧ 4 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 8 = 2 + j₂⊢ 4 = 2 ∧ 8 = j₂ ∨ 4 = j₂ ∧ 8 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 13 = 2 + j₂⊢ 4 = 2 ∧ 13 = j₂ ∨ 4 = j₂ ∧ 13 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 1 = 4 + j₂⊢ 4 = 4 ∧ 1 = j₂ ∨ 4 = j₂ ∧ 1 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 2 = 4 + j₂⊢ 4 = 4 ∧ 2 = j₂ ∨ 4 = j₂ ∧ 2 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 4 = 4 + j₂⊢ 4 = 4 ∧ 4 = j₂ ∨ 4 = j₂ ∧ 4 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 8 = 4 + j₂⊢ 4 = 4 ∧ 8 = j₂ ∨ 4 = j₂ ∧ 8 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 13 = 4 + j₂⊢ 4 = 4 ∧ 13 = j₂ ∨ 4 = j₂ ∧ 13 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 1 = 8 + j₂⊢ 4 = 8 ∧ 1 = j₂ ∨ 4 = j₂ ∧ 1 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 2 = 8 + j₂⊢ 4 = 8 ∧ 2 = j₂ ∨ 4 = j₂ ∧ 2 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 4 = 8 + j₂⊢ 4 = 8 ∧ 4 = j₂ ∨ 4 = j₂ ∧ 4 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 8 = 8 + j₂⊢ 4 = 8 ∧ 8 = j₂ ∨ 4 = j₂ ∧ 8 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 13 = 8 + j₂⊢ 4 = 8 ∧ 13 = j₂ ∨ 4 = j₂ ∧ 13 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 1 = 13 + j₂⊢ 4 = 13 ∧ 1 = j₂ ∨ 4 = j₂ ∧ 1 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 2 = 13 + j₂⊢ 4 = 13 ∧ 2 = j₂ ∨ 4 = j₂ ∧ 2 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 4 = 13 + j₂⊢ 4 = 13 ∧ 4 = j₂ ∨ 4 = j₂ ∧ 4 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 8 = 13 + j₂⊢ 4 = 13 ∧ 8 = j₂ ∨ 4 = j₂ ∧ 8 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:4 + 13 = 13 + j₂⊢ 4 = 13 ∧ 13 = j₂ ∨ 4 = j₂ ∧ 13 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 1 = 1 + j₂⊢ 8 = 1 ∧ 1 = j₂ ∨ 8 = j₂ ∧ 1 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 2 = 1 + j₂⊢ 8 = 1 ∧ 2 = j₂ ∨ 8 = j₂ ∧ 2 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 4 = 1 + j₂⊢ 8 = 1 ∧ 4 = j₂ ∨ 8 = j₂ ∧ 4 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 8 = 1 + j₂⊢ 8 = 1 ∧ 8 = j₂ ∨ 8 = j₂ ∧ 8 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 13 = 1 + j₂⊢ 8 = 1 ∧ 13 = j₂ ∨ 8 = j₂ ∧ 13 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 1 = 2 + j₂⊢ 8 = 2 ∧ 1 = j₂ ∨ 8 = j₂ ∧ 1 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 2 = 2 + j₂⊢ 8 = 2 ∧ 2 = j₂ ∨ 8 = j₂ ∧ 2 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 4 = 2 + j₂⊢ 8 = 2 ∧ 4 = j₂ ∨ 8 = j₂ ∧ 4 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 8 = 2 + j₂⊢ 8 = 2 ∧ 8 = j₂ ∨ 8 = j₂ ∧ 8 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 13 = 2 + j₂⊢ 8 = 2 ∧ 13 = j₂ ∨ 8 = j₂ ∧ 13 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 1 = 4 + j₂⊢ 8 = 4 ∧ 1 = j₂ ∨ 8 = j₂ ∧ 1 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 2 = 4 + j₂⊢ 8 = 4 ∧ 2 = j₂ ∨ 8 = j₂ ∧ 2 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 4 = 4 + j₂⊢ 8 = 4 ∧ 4 = j₂ ∨ 8 = j₂ ∧ 4 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 8 = 4 + j₂⊢ 8 = 4 ∧ 8 = j₂ ∨ 8 = j₂ ∧ 8 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 13 = 4 + j₂⊢ 8 = 4 ∧ 13 = j₂ ∨ 8 = j₂ ∧ 13 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 1 = 8 + j₂⊢ 8 = 8 ∧ 1 = j₂ ∨ 8 = j₂ ∧ 1 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 2 = 8 + j₂⊢ 8 = 8 ∧ 2 = j₂ ∨ 8 = j₂ ∧ 2 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 4 = 8 + j₂⊢ 8 = 8 ∧ 4 = j₂ ∨ 8 = j₂ ∧ 4 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 8 = 8 + j₂⊢ 8 = 8 ∧ 8 = j₂ ∨ 8 = j₂ ∧ 8 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 13 = 8 + j₂⊢ 8 = 8 ∧ 13 = j₂ ∨ 8 = j₂ ∧ 13 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 1 = 13 + j₂⊢ 8 = 13 ∧ 1 = j₂ ∨ 8 = j₂ ∧ 1 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 2 = 13 + j₂⊢ 8 = 13 ∧ 2 = j₂ ∨ 8 = j₂ ∧ 2 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 4 = 13 + j₂⊢ 8 = 13 ∧ 4 = j₂ ∨ 8 = j₂ ∧ 4 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 8 = 13 + j₂⊢ 8 = 13 ∧ 8 = j₂ ∨ 8 = j₂ ∧ 8 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:8 + 13 = 13 + j₂⊢ 8 = 13 ∧ 13 = j₂ ∨ 8 = j₂ ∧ 13 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 1 = 1 + j₂⊢ 13 = 1 ∧ 1 = j₂ ∨ 13 = j₂ ∧ 1 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 2 = 1 + j₂⊢ 13 = 1 ∧ 2 = j₂ ∨ 13 = j₂ ∧ 2 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 4 = 1 + j₂⊢ 13 = 1 ∧ 4 = j₂ ∨ 13 = j₂ ∧ 4 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 8 = 1 + j₂⊢ 13 = 1 ∧ 8 = j₂ ∨ 13 = j₂ ∧ 8 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 13 = 1 + j₂⊢ 13 = 1 ∧ 13 = j₂ ∨ 13 = j₂ ∧ 13 = 1j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 1 = 2 + j₂⊢ 13 = 2 ∧ 1 = j₂ ∨ 13 = j₂ ∧ 1 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 2 = 2 + j₂⊢ 13 = 2 ∧ 2 = j₂ ∨ 13 = j₂ ∧ 2 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 4 = 2 + j₂⊢ 13 = 2 ∧ 4 = j₂ ∨ 13 = j₂ ∧ 4 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 8 = 2 + j₂⊢ 13 = 2 ∧ 8 = j₂ ∨ 13 = j₂ ∧ 8 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 13 = 2 + j₂⊢ 13 = 2 ∧ 13 = j₂ ∨ 13 = j₂ ∧ 13 = 2j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 1 = 4 + j₂⊢ 13 = 4 ∧ 1 = j₂ ∨ 13 = j₂ ∧ 1 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 2 = 4 + j₂⊢ 13 = 4 ∧ 2 = j₂ ∨ 13 = j₂ ∧ 2 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 4 = 4 + j₂⊢ 13 = 4 ∧ 4 = j₂ ∨ 13 = j₂ ∧ 4 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 8 = 4 + j₂⊢ 13 = 4 ∧ 8 = j₂ ∨ 13 = j₂ ∧ 8 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 13 = 4 + j₂⊢ 13 = 4 ∧ 13 = j₂ ∨ 13 = j₂ ∧ 13 = 4j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 1 = 8 + j₂⊢ 13 = 8 ∧ 1 = j₂ ∨ 13 = j₂ ∧ 1 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 2 = 8 + j₂⊢ 13 = 8 ∧ 2 = j₂ ∨ 13 = j₂ ∧ 2 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 4 = 8 + j₂⊢ 13 = 8 ∧ 4 = j₂ ∨ 13 = j₂ ∧ 4 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 8 = 8 + j₂⊢ 13 = 8 ∧ 8 = j₂ ∨ 13 = j₂ ∧ 8 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 13 = 8 + j₂⊢ 13 = 8 ∧ 13 = j₂ ∨ 13 = j₂ ∧ 13 = 8j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 1 = 13 + j₂⊢ 13 = 13 ∧ 1 = j₂ ∨ 13 = j₂ ∧ 1 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 2 = 13 + j₂⊢ 13 = 13 ∧ 2 = j₂ ∨ 13 = j₂ ∧ 2 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 4 = 13 + j₂⊢ 13 = 13 ∧ 4 = j₂ ∨ 13 = j₂ ∧ 4 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 8 = 13 + j₂⊢ 13 = 13 ∧ 8 = j₂ ∨ 13 = j₂ ∧ 8 = 13j₂:ℕhj₂:j₂ = 1 ∨ j₂ = 2 ∨ j₂ = 4 ∨ j₂ = 8 ∨ j₂ = 13hsum:13 + 13 = 13 + j₂⊢ 13 = 13 ∧ 13 = j₂ ∨ 13 = j₂ ∧ 13 = 13 hsum:13 + 13 = 13 + 1⊢ 13 = 13 ∧ 13 = 1 ∨ 13 = 1 ∧ 13 = 13hsum:13 + 13 = 13 + 2⊢ 13 = 13 ∧ 13 = 2 ∨ 13 = 2 ∧ 13 = 13hsum:13 + 13 = 13 + 4⊢ 13 = 13 ∧ 13 = 4 ∨ 13 = 4 ∧ 13 = 13hsum:13 + 13 = 13 + 8⊢ 13 = 13 ∧ 13 = 8 ∨ 13 = 8 ∧ 13 = 13hsum:13 + 13 = 13 + 13⊢ 13 = 13 ∧ 13 = 13 ∨ 13 = 13 ∧ 13 = 13 hsum:1 + 1 = 1 + 1⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 1hsum:1 + 1 = 1 + 2⊢ 1 = 1 ∧ 1 = 2 ∨ 1 = 2 ∧ 1 = 1hsum:1 + 1 = 1 + 4⊢ 1 = 1 ∧ 1 = 4 ∨ 1 = 4 ∧ 1 = 1hsum:1 + 1 = 1 + 8⊢ 1 = 1 ∧ 1 = 8 ∨ 1 = 8 ∧ 1 = 1hsum:1 + 1 = 1 + 13⊢ 1 = 1 ∧ 1 = 13 ∨ 1 = 13 ∧ 1 = 1hsum:1 + 2 = 1 + 1⊢ 1 = 1 ∧ 2 = 1 ∨ 1 = 1 ∧ 2 = 1hsum:1 + 2 = 1 + 2⊢ 1 = 1 ∧ 2 = 2 ∨ 1 = 2 ∧ 2 = 1hsum:1 + 2 = 1 + 4⊢ 1 = 1 ∧ 2 = 4 ∨ 1 = 4 ∧ 2 = 1hsum:1 + 2 = 1 + 8⊢ 1 = 1 ∧ 2 = 8 ∨ 1 = 8 ∧ 2 = 1hsum:1 + 2 = 1 + 13⊢ 1 = 1 ∧ 2 = 13 ∨ 1 = 13 ∧ 2 = 1hsum:1 + 4 = 1 + 1⊢ 1 = 1 ∧ 4 = 1 ∨ 1 = 1 ∧ 4 = 1hsum:1 + 4 = 1 + 2⊢ 1 = 1 ∧ 4 = 2 ∨ 1 = 2 ∧ 4 = 1hsum:1 + 4 = 1 + 4⊢ 1 = 1 ∧ 4 = 4 ∨ 1 = 4 ∧ 4 = 1hsum:1 + 4 = 1 + 8⊢ 1 = 1 ∧ 4 = 8 ∨ 1 = 8 ∧ 4 = 1hsum:1 + 4 = 1 + 13⊢ 1 = 1 ∧ 4 = 13 ∨ 1 = 13 ∧ 4 = 1hsum:1 + 8 = 1 + 1⊢ 1 = 1 ∧ 8 = 1 ∨ 1 = 1 ∧ 8 = 1hsum:1 + 8 = 1 + 2⊢ 1 = 1 ∧ 8 = 2 ∨ 1 = 2 ∧ 8 = 1hsum:1 + 8 = 1 + 4⊢ 1 = 1 ∧ 8 = 4 ∨ 1 = 4 ∧ 8 = 1hsum:1 + 8 = 1 + 8⊢ 1 = 1 ∧ 8 = 8 ∨ 1 = 8 ∧ 8 = 1hsum:1 + 8 = 1 + 13⊢ 1 = 1 ∧ 8 = 13 ∨ 1 = 13 ∧ 8 = 1hsum:1 + 13 = 1 + 1⊢ 1 = 1 ∧ 13 = 1 ∨ 1 = 1 ∧ 13 = 1hsum:1 + 13 = 1 + 2⊢ 1 = 1 ∧ 13 = 2 ∨ 1 = 2 ∧ 13 = 1hsum:1 + 13 = 1 + 4⊢ 1 = 1 ∧ 13 = 4 ∨ 1 = 4 ∧ 13 = 1hsum:1 + 13 = 1 + 8⊢ 1 = 1 ∧ 13 = 8 ∨ 1 = 8 ∧ 13 = 1hsum:1 + 13 = 1 + 13⊢ 1 = 1 ∧ 13 = 13 ∨ 1 = 13 ∧ 13 = 1hsum:1 + 1 = 2 + 1⊢ 1 = 2 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 2hsum:1 + 1 = 2 + 2⊢ 1 = 2 ∧ 1 = 2 ∨ 1 = 2 ∧ 1 = 2hsum:1 + 1 = 2 + 4⊢ 1 = 2 ∧ 1 = 4 ∨ 1 = 4 ∧ 1 = 2hsum:1 + 1 = 2 + 8⊢ 1 = 2 ∧ 1 = 8 ∨ 1 = 8 ∧ 1 = 2hsum:1 + 1 = 2 + 13⊢ 1 = 2 ∧ 1 = 13 ∨ 1 = 13 ∧ 1 = 2hsum:1 + 2 = 2 + 1⊢ 1 = 2 ∧ 2 = 1 ∨ 1 = 1 ∧ 2 = 2hsum:1 + 2 = 2 + 2⊢ 1 = 2 ∧ 2 = 2 ∨ 1 = 2 ∧ 2 = 2hsum:1 + 2 = 2 + 4⊢ 1 = 2 ∧ 2 = 4 ∨ 1 = 4 ∧ 2 = 2hsum:1 + 2 = 2 + 8⊢ 1 = 2 ∧ 2 = 8 ∨ 1 = 8 ∧ 2 = 2hsum:1 + 2 = 2 + 13⊢ 1 = 2 ∧ 2 = 13 ∨ 1 = 13 ∧ 2 = 2hsum:1 + 4 = 2 + 1⊢ 1 = 2 ∧ 4 = 1 ∨ 1 = 1 ∧ 4 = 2hsum:1 + 4 = 2 + 2⊢ 1 = 2 ∧ 4 = 2 ∨ 1 = 2 ∧ 4 = 2hsum:1 + 4 = 2 + 4⊢ 1 = 2 ∧ 4 = 4 ∨ 1 = 4 ∧ 4 = 2hsum:1 + 4 = 2 + 8⊢ 1 = 2 ∧ 4 = 8 ∨ 1 = 8 ∧ 4 = 2hsum:1 + 4 = 2 + 13⊢ 1 = 2 ∧ 4 = 13 ∨ 1 = 13 ∧ 4 = 2hsum:1 + 8 = 2 + 1⊢ 1 = 2 ∧ 8 = 1 ∨ 1 = 1 ∧ 8 = 2hsum:1 + 8 = 2 + 2⊢ 1 = 2 ∧ 8 = 2 ∨ 1 = 2 ∧ 8 = 2hsum:1 + 8 = 2 + 4⊢ 1 = 2 ∧ 8 = 4 ∨ 1 = 4 ∧ 8 = 2hsum:1 + 8 = 2 + 8⊢ 1 = 2 ∧ 8 = 8 ∨ 1 = 8 ∧ 8 = 2hsum:1 + 8 = 2 + 13⊢ 1 = 2 ∧ 8 = 13 ∨ 1 = 13 ∧ 8 = 2hsum:1 + 13 = 2 + 1⊢ 1 = 2 ∧ 13 = 1 ∨ 1 = 1 ∧ 13 = 2hsum:1 + 13 = 2 + 2⊢ 1 = 2 ∧ 13 = 2 ∨ 1 = 2 ∧ 13 = 2hsum:1 + 13 = 2 + 4⊢ 1 = 2 ∧ 13 = 4 ∨ 1 = 4 ∧ 13 = 2hsum:1 + 13 = 2 + 8⊢ 1 = 2 ∧ 13 = 8 ∨ 1 = 8 ∧ 13 = 2hsum:1 + 13 = 2 + 13⊢ 1 = 2 ∧ 13 = 13 ∨ 1 = 13 ∧ 13 = 2hsum:1 + 1 = 4 + 1⊢ 1 = 4 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 4hsum:1 + 1 = 4 + 2⊢ 1 = 4 ∧ 1 = 2 ∨ 1 = 2 ∧ 1 = 4hsum:1 + 1 = 4 + 4⊢ 1 = 4 ∧ 1 = 4 ∨ 1 = 4 ∧ 1 = 4hsum:1 + 1 = 4 + 8⊢ 1 = 4 ∧ 1 = 8 ∨ 1 = 8 ∧ 1 = 4hsum:1 + 1 = 4 + 13⊢ 1 = 4 ∧ 1 = 13 ∨ 1 = 13 ∧ 1 = 4hsum:1 + 2 = 4 + 1⊢ 1 = 4 ∧ 2 = 1 ∨ 1 = 1 ∧ 2 = 4hsum:1 + 2 = 4 + 2⊢ 1 = 4 ∧ 2 = 2 ∨ 1 = 2 ∧ 2 = 4hsum:1 + 2 = 4 + 4⊢ 1 = 4 ∧ 2 = 4 ∨ 1 = 4 ∧ 2 = 4hsum:1 + 2 = 4 + 8⊢ 1 = 4 ∧ 2 = 8 ∨ 1 = 8 ∧ 2 = 4hsum:1 + 2 = 4 + 13⊢ 1 = 4 ∧ 2 = 13 ∨ 1 = 13 ∧ 2 = 4hsum:1 + 4 = 4 + 1⊢ 1 = 4 ∧ 4 = 1 ∨ 1 = 1 ∧ 4 = 4hsum:1 + 4 = 4 + 2⊢ 1 = 4 ∧ 4 = 2 ∨ 1 = 2 ∧ 4 = 4hsum:1 + 4 = 4 + 4⊢ 1 = 4 ∧ 4 = 4 ∨ 1 = 4 ∧ 4 = 4hsum:1 + 4 = 4 + 8⊢ 1 = 4 ∧ 4 = 8 ∨ 1 = 8 ∧ 4 = 4hsum:1 + 4 = 4 + 13⊢ 1 = 4 ∧ 4 = 13 ∨ 1 = 13 ∧ 4 = 4hsum:1 + 8 = 4 + 1⊢ 1 = 4 ∧ 8 = 1 ∨ 1 = 1 ∧ 8 = 4hsum:1 + 8 = 4 + 2⊢ 1 = 4 ∧ 8 = 2 ∨ 1 = 2 ∧ 8 = 4hsum:1 + 8 = 4 + 4⊢ 1 = 4 ∧ 8 = 4 ∨ 1 = 4 ∧ 8 = 4hsum:1 + 8 = 4 + 8⊢ 1 = 4 ∧ 8 = 8 ∨ 1 = 8 ∧ 8 = 4hsum:1 + 8 = 4 + 13⊢ 1 = 4 ∧ 8 = 13 ∨ 1 = 13 ∧ 8 = 4hsum:1 + 13 = 4 + 1⊢ 1 = 4 ∧ 13 = 1 ∨ 1 = 1 ∧ 13 = 4hsum:1 + 13 = 4 + 2⊢ 1 = 4 ∧ 13 = 2 ∨ 1 = 2 ∧ 13 = 4hsum:1 + 13 = 4 + 4⊢ 1 = 4 ∧ 13 = 4 ∨ 1 = 4 ∧ 13 = 4hsum:1 + 13 = 4 + 8⊢ 1 = 4 ∧ 13 = 8 ∨ 1 = 8 ∧ 13 = 4hsum:1 + 13 = 4 + 13⊢ 1 = 4 ∧ 13 = 13 ∨ 1 = 13 ∧ 13 = 4hsum:1 + 1 = 8 + 1⊢ 1 = 8 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 8hsum:1 + 1 = 8 + 2⊢ 1 = 8 ∧ 1 = 2 ∨ 1 = 2 ∧ 1 = 8hsum:1 + 1 = 8 + 4⊢ 1 = 8 ∧ 1 = 4 ∨ 1 = 4 ∧ 1 = 8hsum:1 + 1 = 8 + 8⊢ 1 = 8 ∧ 1 = 8 ∨ 1 = 8 ∧ 1 = 8hsum:1 + 1 = 8 + 13⊢ 1 = 8 ∧ 1 = 13 ∨ 1 = 13 ∧ 1 = 8hsum:1 + 2 = 8 + 1⊢ 1 = 8 ∧ 2 = 1 ∨ 1 = 1 ∧ 2 = 8hsum:1 + 2 = 8 + 2⊢ 1 = 8 ∧ 2 = 2 ∨ 1 = 2 ∧ 2 = 8hsum:1 + 2 = 8 + 4⊢ 1 = 8 ∧ 2 = 4 ∨ 1 = 4 ∧ 2 = 8hsum:1 + 2 = 8 + 8⊢ 1 = 8 ∧ 2 = 8 ∨ 1 = 8 ∧ 2 = 8hsum:1 + 2 = 8 + 13⊢ 1 = 8 ∧ 2 = 13 ∨ 1 = 13 ∧ 2 = 8hsum:1 + 4 = 8 + 1⊢ 1 = 8 ∧ 4 = 1 ∨ 1 = 1 ∧ 4 = 8hsum:1 + 4 = 8 + 2⊢ 1 = 8 ∧ 4 = 2 ∨ 1 = 2 ∧ 4 = 8hsum:1 + 4 = 8 + 4⊢ 1 = 8 ∧ 4 = 4 ∨ 1 = 4 ∧ 4 = 8hsum:1 + 4 = 8 + 8⊢ 1 = 8 ∧ 4 = 8 ∨ 1 = 8 ∧ 4 = 8hsum:1 + 4 = 8 + 13⊢ 1 = 8 ∧ 4 = 13 ∨ 1 = 13 ∧ 4 = 8hsum:1 + 8 = 8 + 1⊢ 1 = 8 ∧ 8 = 1 ∨ 1 = 1 ∧ 8 = 8hsum:1 + 8 = 8 + 2⊢ 1 = 8 ∧ 8 = 2 ∨ 1 = 2 ∧ 8 = 8hsum:1 + 8 = 8 + 4⊢ 1 = 8 ∧ 8 = 4 ∨ 1 = 4 ∧ 8 = 8hsum:1 + 8 = 8 + 8⊢ 1 = 8 ∧ 8 = 8 ∨ 1 = 8 ∧ 8 = 8hsum:1 + 8 = 8 + 13⊢ 1 = 8 ∧ 8 = 13 ∨ 1 = 13 ∧ 8 = 8hsum:1 + 13 = 8 + 1⊢ 1 = 8 ∧ 13 = 1 ∨ 1 = 1 ∧ 13 = 8hsum:1 + 13 = 8 + 2⊢ 1 = 8 ∧ 13 = 2 ∨ 1 = 2 ∧ 13 = 8hsum:1 + 13 = 8 + 4⊢ 1 = 8 ∧ 13 = 4 ∨ 1 = 4 ∧ 13 = 8hsum:1 + 13 = 8 + 8⊢ 1 = 8 ∧ 13 = 8 ∨ 1 = 8 ∧ 13 = 8hsum:1 + 13 = 8 + 13⊢ 1 = 8 ∧ 13 = 13 ∨ 1 = 13 ∧ 13 = 8hsum:1 + 1 = 13 + 1⊢ 1 = 13 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 13hsum:1 + 1 = 13 + 2⊢ 1 = 13 ∧ 1 = 2 ∨ 1 = 2 ∧ 1 = 13hsum:1 + 1 = 13 + 4⊢ 1 = 13 ∧ 1 = 4 ∨ 1 = 4 ∧ 1 = 13hsum:1 + 1 = 13 + 8⊢ 1 = 13 ∧ 1 = 8 ∨ 1 = 8 ∧ 1 = 13hsum:1 + 1 = 13 + 13⊢ 1 = 13 ∧ 1 = 13 ∨ 1 = 13 ∧ 1 = 13hsum:1 + 2 = 13 + 1⊢ 1 = 13 ∧ 2 = 1 ∨ 1 = 1 ∧ 2 = 13hsum:1 + 2 = 13 + 2⊢ 1 = 13 ∧ 2 = 2 ∨ 1 = 2 ∧ 2 = 13hsum:1 + 2 = 13 + 4⊢ 1 = 13 ∧ 2 = 4 ∨ 1 = 4 ∧ 2 = 13hsum:1 + 2 = 13 + 8⊢ 1 = 13 ∧ 2 = 8 ∨ 1 = 8 ∧ 2 = 13hsum:1 + 2 = 13 + 13⊢ 1 = 13 ∧ 2 = 13 ∨ 1 = 13 ∧ 2 = 13hsum:1 + 4 = 13 + 1⊢ 1 = 13 ∧ 4 = 1 ∨ 1 = 1 ∧ 4 = 13hsum:1 + 4 = 13 + 2⊢ 1 = 13 ∧ 4 = 2 ∨ 1 = 2 ∧ 4 = 13hsum:1 + 4 = 13 + 4⊢ 1 = 13 ∧ 4 = 4 ∨ 1 = 4 ∧ 4 = 13hsum:1 + 4 = 13 + 8⊢ 1 = 13 ∧ 4 = 8 ∨ 1 = 8 ∧ 4 = 13hsum:1 + 4 = 13 + 13⊢ 1 = 13 ∧ 4 = 13 ∨ 1 = 13 ∧ 4 = 13hsum:1 + 8 = 13 + 1⊢ 1 = 13 ∧ 8 = 1 ∨ 1 = 1 ∧ 8 = 13hsum:1 + 8 = 13 + 2⊢ 1 = 13 ∧ 8 = 2 ∨ 1 = 2 ∧ 8 = 13hsum:1 + 8 = 13 + 4⊢ 1 = 13 ∧ 8 = 4 ∨ 1 = 4 ∧ 8 = 13hsum:1 + 8 = 13 + 8⊢ 1 = 13 ∧ 8 = 8 ∨ 1 = 8 ∧ 8 = 13hsum:1 + 8 = 13 + 13⊢ 1 = 13 ∧ 8 = 13 ∨ 1 = 13 ∧ 8 = 13hsum:1 + 13 = 13 + 1⊢ 1 = 13 ∧ 13 = 1 ∨ 1 = 1 ∧ 13 = 13hsum:1 + 13 = 13 + 2⊢ 1 = 13 ∧ 13 = 2 ∨ 1 = 2 ∧ 13 = 13hsum:1 + 13 = 13 + 4⊢ 1 = 13 ∧ 13 = 4 ∨ 1 = 4 ∧ 13 = 13hsum:1 + 13 = 13 + 8⊢ 1 = 13 ∧ 13 = 8 ∨ 1 = 8 ∧ 13 = 13hsum:1 + 13 = 13 + 13⊢ 1 = 13 ∧ 13 = 13 ∨ 1 = 13 ∧ 13 = 13hsum:2 + 1 = 1 + 1⊢ 2 = 1 ∧ 1 = 1 ∨ 2 = 1 ∧ 1 = 1hsum:2 + 1 = 1 + 2⊢ 2 = 1 ∧ 1 = 2 ∨ 2 = 2 ∧ 1 = 1hsum:2 + 1 = 1 + 4⊢ 2 = 1 ∧ 1 = 4 ∨ 2 = 4 ∧ 1 = 1hsum:2 + 1 = 1 + 8⊢ 2 = 1 ∧ 1 = 8 ∨ 2 = 8 ∧ 1 = 1hsum:2 + 1 = 1 + 13⊢ 2 = 1 ∧ 1 = 13 ∨ 2 = 13 ∧ 1 = 1hsum:2 + 2 = 1 + 1⊢ 2 = 1 ∧ 2 = 1 ∨ 2 = 1 ∧ 2 = 1hsum:2 + 2 = 1 + 2⊢ 2 = 1 ∧ 2 = 2 ∨ 2 = 2 ∧ 2 = 1hsum:2 + 2 = 1 + 4⊢ 2 = 1 ∧ 2 = 4 ∨ 2 = 4 ∧ 2 = 1hsum:2 + 2 = 1 + 8⊢ 2 = 1 ∧ 2 = 8 ∨ 2 = 8 ∧ 2 = 1hsum:2 + 2 = 1 + 13⊢ 2 = 1 ∧ 2 = 13 ∨ 2 = 13 ∧ 2 = 1hsum:2 + 4 = 1 + 1⊢ 2 = 1 ∧ 4 = 1 ∨ 2 = 1 ∧ 4 = 1hsum:2 + 4 = 1 + 2⊢ 2 = 1 ∧ 4 = 2 ∨ 2 = 2 ∧ 4 = 1hsum:2 + 4 = 1 + 4⊢ 2 = 1 ∧ 4 = 4 ∨ 2 = 4 ∧ 4 = 1hsum:2 + 4 = 1 + 8⊢ 2 = 1 ∧ 4 = 8 ∨ 2 = 8 ∧ 4 = 1hsum:2 + 4 = 1 + 13⊢ 2 = 1 ∧ 4 = 13 ∨ 2 = 13 ∧ 4 = 1hsum:2 + 8 = 1 + 1⊢ 2 = 1 ∧ 8 = 1 ∨ 2 = 1 ∧ 8 = 1hsum:2 + 8 = 1 + 2⊢ 2 = 1 ∧ 8 = 2 ∨ 2 = 2 ∧ 8 = 1hsum:2 + 8 = 1 + 4⊢ 2 = 1 ∧ 8 = 4 ∨ 2 = 4 ∧ 8 = 1hsum:2 + 8 = 1 + 8⊢ 2 = 1 ∧ 8 = 8 ∨ 2 = 8 ∧ 8 = 1hsum:2 + 8 = 1 + 13⊢ 2 = 1 ∧ 8 = 13 ∨ 2 = 13 ∧ 8 = 1hsum:2 + 13 = 1 + 1⊢ 2 = 1 ∧ 13 = 1 ∨ 2 = 1 ∧ 13 = 1hsum:2 + 13 = 1 + 2⊢ 2 = 1 ∧ 13 = 2 ∨ 2 = 2 ∧ 13 = 1hsum:2 + 13 = 1 + 4⊢ 2 = 1 ∧ 13 = 4 ∨ 2 = 4 ∧ 13 = 1hsum:2 + 13 = 1 + 8⊢ 2 = 1 ∧ 13 = 8 ∨ 2 = 8 ∧ 13 = 1hsum:2 + 13 = 1 + 13⊢ 2 = 1 ∧ 13 = 13 ∨ 2 = 13 ∧ 13 = 1hsum:2 + 1 = 2 + 1⊢ 2 = 2 ∧ 1 = 1 ∨ 2 = 1 ∧ 1 = 2hsum:2 + 1 = 2 + 2⊢ 2 = 2 ∧ 1 = 2 ∨ 2 = 2 ∧ 1 = 2hsum:2 + 1 = 2 + 4⊢ 2 = 2 ∧ 1 = 4 ∨ 2 = 4 ∧ 1 = 2hsum:2 + 1 = 2 + 8⊢ 2 = 2 ∧ 1 = 8 ∨ 2 = 8 ∧ 1 = 2hsum:2 + 1 = 2 + 13⊢ 2 = 2 ∧ 1 = 13 ∨ 2 = 13 ∧ 1 = 2hsum:2 + 2 = 2 + 1⊢ 2 = 2 ∧ 2 = 1 ∨ 2 = 1 ∧ 2 = 2hsum:2 + 2 = 2 + 2⊢ 2 = 2 ∧ 2 = 2 ∨ 2 = 2 ∧ 2 = 2hsum:2 + 2 = 2 + 4⊢ 2 = 2 ∧ 2 = 4 ∨ 2 = 4 ∧ 2 = 2hsum:2 + 2 = 2 + 8⊢ 2 = 2 ∧ 2 = 8 ∨ 2 = 8 ∧ 2 = 2hsum:2 + 2 = 2 + 13⊢ 2 = 2 ∧ 2 = 13 ∨ 2 = 13 ∧ 2 = 2hsum:2 + 4 = 2 + 1⊢ 2 = 2 ∧ 4 = 1 ∨ 2 = 1 ∧ 4 = 2hsum:2 + 4 = 2 + 2⊢ 2 = 2 ∧ 4 = 2 ∨ 2 = 2 ∧ 4 = 2hsum:2 + 4 = 2 + 4⊢ 2 = 2 ∧ 4 = 4 ∨ 2 = 4 ∧ 4 = 2hsum:2 + 4 = 2 + 8⊢ 2 = 2 ∧ 4 = 8 ∨ 2 = 8 ∧ 4 = 2hsum:2 + 4 = 2 + 13⊢ 2 = 2 ∧ 4 = 13 ∨ 2 = 13 ∧ 4 = 2hsum:2 + 8 = 2 + 1⊢ 2 = 2 ∧ 8 = 1 ∨ 2 = 1 ∧ 8 = 2hsum:2 + 8 = 2 + 2⊢ 2 = 2 ∧ 8 = 2 ∨ 2 = 2 ∧ 8 = 2hsum:2 + 8 = 2 + 4⊢ 2 = 2 ∧ 8 = 4 ∨ 2 = 4 ∧ 8 = 2hsum:2 + 8 = 2 + 8⊢ 2 = 2 ∧ 8 = 8 ∨ 2 = 8 ∧ 8 = 2hsum:2 + 8 = 2 + 13⊢ 2 = 2 ∧ 8 = 13 ∨ 2 = 13 ∧ 8 = 2hsum:2 + 13 = 2 + 1⊢ 2 = 2 ∧ 13 = 1 ∨ 2 = 1 ∧ 13 = 2hsum:2 + 13 = 2 + 2⊢ 2 = 2 ∧ 13 = 2 ∨ 2 = 2 ∧ 13 = 2hsum:2 + 13 = 2 + 4⊢ 2 = 2 ∧ 13 = 4 ∨ 2 = 4 ∧ 13 = 2hsum:2 + 13 = 2 + 8⊢ 2 = 2 ∧ 13 = 8 ∨ 2 = 8 ∧ 13 = 2hsum:2 + 13 = 2 + 13⊢ 2 = 2 ∧ 13 = 13 ∨ 2 = 13 ∧ 13 = 2hsum:2 + 1 = 4 + 1⊢ 2 = 4 ∧ 1 = 1 ∨ 2 = 1 ∧ 1 = 4hsum:2 + 1 = 4 + 2⊢ 2 = 4 ∧ 1 = 2 ∨ 2 = 2 ∧ 1 = 4hsum:2 + 1 = 4 + 4⊢ 2 = 4 ∧ 1 = 4 ∨ 2 = 4 ∧ 1 = 4hsum:2 + 1 = 4 + 8⊢ 2 = 4 ∧ 1 = 8 ∨ 2 = 8 ∧ 1 = 4hsum:2 + 1 = 4 + 13⊢ 2 = 4 ∧ 1 = 13 ∨ 2 = 13 ∧ 1 = 4hsum:2 + 2 = 4 + 1⊢ 2 = 4 ∧ 2 = 1 ∨ 2 = 1 ∧ 2 = 4hsum:2 + 2 = 4 + 2⊢ 2 = 4 ∧ 2 = 2 ∨ 2 = 2 ∧ 2 = 4hsum:2 + 2 = 4 + 4⊢ 2 = 4 ∧ 2 = 4 ∨ 2 = 4 ∧ 2 = 4hsum:2 + 2 = 4 + 8⊢ 2 = 4 ∧ 2 = 8 ∨ 2 = 8 ∧ 2 = 4hsum:2 + 2 = 4 + 13⊢ 2 = 4 ∧ 2 = 13 ∨ 2 = 13 ∧ 2 = 4hsum:2 + 4 = 4 + 1⊢ 2 = 4 ∧ 4 = 1 ∨ 2 = 1 ∧ 4 = 4hsum:2 + 4 = 4 + 2⊢ 2 = 4 ∧ 4 = 2 ∨ 2 = 2 ∧ 4 = 4hsum:2 + 4 = 4 + 4⊢ 2 = 4 ∧ 4 = 4 ∨ 2 = 4 ∧ 4 = 4hsum:2 + 4 = 4 + 8⊢ 2 = 4 ∧ 4 = 8 ∨ 2 = 8 ∧ 4 = 4hsum:2 + 4 = 4 + 13⊢ 2 = 4 ∧ 4 = 13 ∨ 2 = 13 ∧ 4 = 4hsum:2 + 8 = 4 + 1⊢ 2 = 4 ∧ 8 = 1 ∨ 2 = 1 ∧ 8 = 4hsum:2 + 8 = 4 + 2⊢ 2 = 4 ∧ 8 = 2 ∨ 2 = 2 ∧ 8 = 4hsum:2 + 8 = 4 + 4⊢ 2 = 4 ∧ 8 = 4 ∨ 2 = 4 ∧ 8 = 4hsum:2 + 8 = 4 + 8⊢ 2 = 4 ∧ 8 = 8 ∨ 2 = 8 ∧ 8 = 4hsum:2 + 8 = 4 + 13⊢ 2 = 4 ∧ 8 = 13 ∨ 2 = 13 ∧ 8 = 4hsum:2 + 13 = 4 + 1⊢ 2 = 4 ∧ 13 = 1 ∨ 2 = 1 ∧ 13 = 4hsum:2 + 13 = 4 + 2⊢ 2 = 4 ∧ 13 = 2 ∨ 2 = 2 ∧ 13 = 4hsum:2 + 13 = 4 + 4⊢ 2 = 4 ∧ 13 = 4 ∨ 2 = 4 ∧ 13 = 4hsum:2 + 13 = 4 + 8⊢ 2 = 4 ∧ 13 = 8 ∨ 2 = 8 ∧ 13 = 4hsum:2 + 13 = 4 + 13⊢ 2 = 4 ∧ 13 = 13 ∨ 2 = 13 ∧ 13 = 4hsum:2 + 1 = 8 + 1⊢ 2 = 8 ∧ 1 = 1 ∨ 2 = 1 ∧ 1 = 8hsum:2 + 1 = 8 + 2⊢ 2 = 8 ∧ 1 = 2 ∨ 2 = 2 ∧ 1 = 8hsum:2 + 1 = 8 + 4⊢ 2 = 8 ∧ 1 = 4 ∨ 2 = 4 ∧ 1 = 8hsum:2 + 1 = 8 + 8⊢ 2 = 8 ∧ 1 = 8 ∨ 2 = 8 ∧ 1 = 8hsum:2 + 1 = 8 + 13⊢ 2 = 8 ∧ 1 = 13 ∨ 2 = 13 ∧ 1 = 8hsum:2 + 2 = 8 + 1⊢ 2 = 8 ∧ 2 = 1 ∨ 2 = 1 ∧ 2 = 8hsum:2 + 2 = 8 + 2⊢ 2 = 8 ∧ 2 = 2 ∨ 2 = 2 ∧ 2 = 8hsum:2 + 2 = 8 + 4⊢ 2 = 8 ∧ 2 = 4 ∨ 2 = 4 ∧ 2 = 8hsum:2 + 2 = 8 + 8⊢ 2 = 8 ∧ 2 = 8 ∨ 2 = 8 ∧ 2 = 8hsum:2 + 2 = 8 + 13⊢ 2 = 8 ∧ 2 = 13 ∨ 2 = 13 ∧ 2 = 8hsum:2 + 4 = 8 + 1⊢ 2 = 8 ∧ 4 = 1 ∨ 2 = 1 ∧ 4 = 8hsum:2 + 4 = 8 + 2⊢ 2 = 8 ∧ 4 = 2 ∨ 2 = 2 ∧ 4 = 8hsum:2 + 4 = 8 + 4⊢ 2 = 8 ∧ 4 = 4 ∨ 2 = 4 ∧ 4 = 8hsum:2 + 4 = 8 + 8⊢ 2 = 8 ∧ 4 = 8 ∨ 2 = 8 ∧ 4 = 8hsum:2 + 4 = 8 + 13⊢ 2 = 8 ∧ 4 = 13 ∨ 2 = 13 ∧ 4 = 8hsum:2 + 8 = 8 + 1⊢ 2 = 8 ∧ 8 = 1 ∨ 2 = 1 ∧ 8 = 8hsum:2 + 8 = 8 + 2⊢ 2 = 8 ∧ 8 = 2 ∨ 2 = 2 ∧ 8 = 8hsum:2 + 8 = 8 + 4⊢ 2 = 8 ∧ 8 = 4 ∨ 2 = 4 ∧ 8 = 8hsum:2 + 8 = 8 + 8⊢ 2 = 8 ∧ 8 = 8 ∨ 2 = 8 ∧ 8 = 8hsum:2 + 8 = 8 + 13⊢ 2 = 8 ∧ 8 = 13 ∨ 2 = 13 ∧ 8 = 8hsum:2 + 13 = 8 + 1⊢ 2 = 8 ∧ 13 = 1 ∨ 2 = 1 ∧ 13 = 8hsum:2 + 13 = 8 + 2⊢ 2 = 8 ∧ 13 = 2 ∨ 2 = 2 ∧ 13 = 8hsum:2 + 13 = 8 + 4⊢ 2 = 8 ∧ 13 = 4 ∨ 2 = 4 ∧ 13 = 8hsum:2 + 13 = 8 + 8⊢ 2 = 8 ∧ 13 = 8 ∨ 2 = 8 ∧ 13 = 8hsum:2 + 13 = 8 + 13⊢ 2 = 8 ∧ 13 = 13 ∨ 2 = 13 ∧ 13 = 8hsum:2 + 1 = 13 + 1⊢ 2 = 13 ∧ 1 = 1 ∨ 2 = 1 ∧ 1 = 13hsum:2 + 1 = 13 + 2⊢ 2 = 13 ∧ 1 = 2 ∨ 2 = 2 ∧ 1 = 13hsum:2 + 1 = 13 + 4⊢ 2 = 13 ∧ 1 = 4 ∨ 2 = 4 ∧ 1 = 13hsum:2 + 1 = 13 + 8⊢ 2 = 13 ∧ 1 = 8 ∨ 2 = 8 ∧ 1 = 13hsum:2 + 1 = 13 + 13⊢ 2 = 13 ∧ 1 = 13 ∨ 2 = 13 ∧ 1 = 13hsum:2 + 2 = 13 + 1⊢ 2 = 13 ∧ 2 = 1 ∨ 2 = 1 ∧ 2 = 13hsum:2 + 2 = 13 + 2⊢ 2 = 13 ∧ 2 = 2 ∨ 2 = 2 ∧ 2 = 13hsum:2 + 2 = 13 + 4⊢ 2 = 13 ∧ 2 = 4 ∨ 2 = 4 ∧ 2 = 13hsum:2 + 2 = 13 + 8⊢ 2 = 13 ∧ 2 = 8 ∨ 2 = 8 ∧ 2 = 13hsum:2 + 2 = 13 + 13⊢ 2 = 13 ∧ 2 = 13 ∨ 2 = 13 ∧ 2 = 13hsum:2 + 4 = 13 + 1⊢ 2 = 13 ∧ 4 = 1 ∨ 2 = 1 ∧ 4 = 13hsum:2 + 4 = 13 + 2⊢ 2 = 13 ∧ 4 = 2 ∨ 2 = 2 ∧ 4 = 13hsum:2 + 4 = 13 + 4⊢ 2 = 13 ∧ 4 = 4 ∨ 2 = 4 ∧ 4 = 13hsum:2 + 4 = 13 + 8⊢ 2 = 13 ∧ 4 = 8 ∨ 2 = 8 ∧ 4 = 13hsum:2 + 4 = 13 + 13⊢ 2 = 13 ∧ 4 = 13 ∨ 2 = 13 ∧ 4 = 13hsum:2 + 8 = 13 + 1⊢ 2 = 13 ∧ 8 = 1 ∨ 2 = 1 ∧ 8 = 13hsum:2 + 8 = 13 + 2⊢ 2 = 13 ∧ 8 = 2 ∨ 2 = 2 ∧ 8 = 13hsum:2 + 8 = 13 + 4⊢ 2 = 13 ∧ 8 = 4 ∨ 2 = 4 ∧ 8 = 13hsum:2 + 8 = 13 + 8⊢ 2 = 13 ∧ 8 = 8 ∨ 2 = 8 ∧ 8 = 13hsum:2 + 8 = 13 + 13⊢ 2 = 13 ∧ 8 = 13 ∨ 2 = 13 ∧ 8 = 13hsum:2 + 13 = 13 + 1⊢ 2 = 13 ∧ 13 = 1 ∨ 2 = 1 ∧ 13 = 13hsum:2 + 13 = 13 + 2⊢ 2 = 13 ∧ 13 = 2 ∨ 2 = 2 ∧ 13 = 13hsum:2 + 13 = 13 + 4⊢ 2 = 13 ∧ 13 = 4 ∨ 2 = 4 ∧ 13 = 13hsum:2 + 13 = 13 + 8⊢ 2 = 13 ∧ 13 = 8 ∨ 2 = 8 ∧ 13 = 13hsum:2 + 13 = 13 + 13⊢ 2 = 13 ∧ 13 = 13 ∨ 2 = 13 ∧ 13 = 13hsum:4 + 1 = 1 + 1⊢ 4 = 1 ∧ 1 = 1 ∨ 4 = 1 ∧ 1 = 1hsum:4 + 1 = 1 + 2⊢ 4 = 1 ∧ 1 = 2 ∨ 4 = 2 ∧ 1 = 1hsum:4 + 1 = 1 + 4⊢ 4 = 1 ∧ 1 = 4 ∨ 4 = 4 ∧ 1 = 1hsum:4 + 1 = 1 + 8⊢ 4 = 1 ∧ 1 = 8 ∨ 4 = 8 ∧ 1 = 1hsum:4 + 1 = 1 + 13⊢ 4 = 1 ∧ 1 = 13 ∨ 4 = 13 ∧ 1 = 1hsum:4 + 2 = 1 + 1⊢ 4 = 1 ∧ 2 = 1 ∨ 4 = 1 ∧ 2 = 1hsum:4 + 2 = 1 + 2⊢ 4 = 1 ∧ 2 = 2 ∨ 4 = 2 ∧ 2 = 1hsum:4 + 2 = 1 + 4⊢ 4 = 1 ∧ 2 = 4 ∨ 4 = 4 ∧ 2 = 1hsum:4 + 2 = 1 + 8⊢ 4 = 1 ∧ 2 = 8 ∨ 4 = 8 ∧ 2 = 1hsum:4 + 2 = 1 + 13⊢ 4 = 1 ∧ 2 = 13 ∨ 4 = 13 ∧ 2 = 1hsum:4 + 4 = 1 + 1⊢ 4 = 1 ∧ 4 = 1 ∨ 4 = 1 ∧ 4 = 1hsum:4 + 4 = 1 + 2⊢ 4 = 1 ∧ 4 = 2 ∨ 4 = 2 ∧ 4 = 1hsum:4 + 4 = 1 + 4⊢ 4 = 1 ∧ 4 = 4 ∨ 4 = 4 ∧ 4 = 1hsum:4 + 4 = 1 + 8⊢ 4 = 1 ∧ 4 = 8 ∨ 4 = 8 ∧ 4 = 1hsum:4 + 4 = 1 + 13⊢ 4 = 1 ∧ 4 = 13 ∨ 4 = 13 ∧ 4 = 1hsum:4 + 8 = 1 + 1⊢ 4 = 1 ∧ 8 = 1 ∨ 4 = 1 ∧ 8 = 1hsum:4 + 8 = 1 + 2⊢ 4 = 1 ∧ 8 = 2 ∨ 4 = 2 ∧ 8 = 1hsum:4 + 8 = 1 + 4⊢ 4 = 1 ∧ 8 = 4 ∨ 4 = 4 ∧ 8 = 1hsum:4 + 8 = 1 + 8⊢ 4 = 1 ∧ 8 = 8 ∨ 4 = 8 ∧ 8 = 1hsum:4 + 8 = 1 + 13⊢ 4 = 1 ∧ 8 = 13 ∨ 4 = 13 ∧ 8 = 1hsum:4 + 13 = 1 + 1⊢ 4 = 1 ∧ 13 = 1 ∨ 4 = 1 ∧ 13 = 1hsum:4 + 13 = 1 + 2⊢ 4 = 1 ∧ 13 = 2 ∨ 4 = 2 ∧ 13 = 1hsum:4 + 13 = 1 + 4⊢ 4 = 1 ∧ 13 = 4 ∨ 4 = 4 ∧ 13 = 1hsum:4 + 13 = 1 + 8⊢ 4 = 1 ∧ 13 = 8 ∨ 4 = 8 ∧ 13 = 1hsum:4 + 13 = 1 + 13⊢ 4 = 1 ∧ 13 = 13 ∨ 4 = 13 ∧ 13 = 1hsum:4 + 1 = 2 + 1⊢ 4 = 2 ∧ 1 = 1 ∨ 4 = 1 ∧ 1 = 2hsum:4 + 1 = 2 + 2⊢ 4 = 2 ∧ 1 = 2 ∨ 4 = 2 ∧ 1 = 2hsum:4 + 1 = 2 + 4⊢ 4 = 2 ∧ 1 = 4 ∨ 4 = 4 ∧ 1 = 2hsum:4 + 1 = 2 + 8⊢ 4 = 2 ∧ 1 = 8 ∨ 4 = 8 ∧ 1 = 2hsum:4 + 1 = 2 + 13⊢ 4 = 2 ∧ 1 = 13 ∨ 4 = 13 ∧ 1 = 2hsum:4 + 2 = 2 + 1⊢ 4 = 2 ∧ 2 = 1 ∨ 4 = 1 ∧ 2 = 2hsum:4 + 2 = 2 + 2⊢ 4 = 2 ∧ 2 = 2 ∨ 4 = 2 ∧ 2 = 2hsum:4 + 2 = 2 + 4⊢ 4 = 2 ∧ 2 = 4 ∨ 4 = 4 ∧ 2 = 2hsum:4 + 2 = 2 + 8⊢ 4 = 2 ∧ 2 = 8 ∨ 4 = 8 ∧ 2 = 2hsum:4 + 2 = 2 + 13⊢ 4 = 2 ∧ 2 = 13 ∨ 4 = 13 ∧ 2 = 2hsum:4 + 4 = 2 + 1⊢ 4 = 2 ∧ 4 = 1 ∨ 4 = 1 ∧ 4 = 2hsum:4 + 4 = 2 + 2⊢ 4 = 2 ∧ 4 = 2 ∨ 4 = 2 ∧ 4 = 2hsum:4 + 4 = 2 + 4⊢ 4 = 2 ∧ 4 = 4 ∨ 4 = 4 ∧ 4 = 2hsum:4 + 4 = 2 + 8⊢ 4 = 2 ∧ 4 = 8 ∨ 4 = 8 ∧ 4 = 2hsum:4 + 4 = 2 + 13⊢ 4 = 2 ∧ 4 = 13 ∨ 4 = 13 ∧ 4 = 2hsum:4 + 8 = 2 + 1⊢ 4 = 2 ∧ 8 = 1 ∨ 4 = 1 ∧ 8 = 2hsum:4 + 8 = 2 + 2⊢ 4 = 2 ∧ 8 = 2 ∨ 4 = 2 ∧ 8 = 2hsum:4 + 8 = 2 + 4⊢ 4 = 2 ∧ 8 = 4 ∨ 4 = 4 ∧ 8 = 2hsum:4 + 8 = 2 + 8⊢ 4 = 2 ∧ 8 = 8 ∨ 4 = 8 ∧ 8 = 2hsum:4 + 8 = 2 + 13⊢ 4 = 2 ∧ 8 = 13 ∨ 4 = 13 ∧ 8 = 2hsum:4 + 13 = 2 + 1⊢ 4 = 2 ∧ 13 = 1 ∨ 4 = 1 ∧ 13 = 2hsum:4 + 13 = 2 + 2⊢ 4 = 2 ∧ 13 = 2 ∨ 4 = 2 ∧ 13 = 2hsum:4 + 13 = 2 + 4⊢ 4 = 2 ∧ 13 = 4 ∨ 4 = 4 ∧ 13 = 2hsum:4 + 13 = 2 + 8⊢ 4 = 2 ∧ 13 = 8 ∨ 4 = 8 ∧ 13 = 2hsum:4 + 13 = 2 + 13⊢ 4 = 2 ∧ 13 = 13 ∨ 4 = 13 ∧ 13 = 2hsum:4 + 1 = 4 + 1⊢ 4 = 4 ∧ 1 = 1 ∨ 4 = 1 ∧ 1 = 4hsum:4 + 1 = 4 + 2⊢ 4 = 4 ∧ 1 = 2 ∨ 4 = 2 ∧ 1 = 4hsum:4 + 1 = 4 + 4⊢ 4 = 4 ∧ 1 = 4 ∨ 4 = 4 ∧ 1 = 4hsum:4 + 1 = 4 + 8⊢ 4 = 4 ∧ 1 = 8 ∨ 4 = 8 ∧ 1 = 4hsum:4 + 1 = 4 + 13⊢ 4 = 4 ∧ 1 = 13 ∨ 4 = 13 ∧ 1 = 4hsum:4 + 2 = 4 + 1⊢ 4 = 4 ∧ 2 = 1 ∨ 4 = 1 ∧ 2 = 4hsum:4 + 2 = 4 + 2⊢ 4 = 4 ∧ 2 = 2 ∨ 4 = 2 ∧ 2 = 4hsum:4 + 2 = 4 + 4⊢ 4 = 4 ∧ 2 = 4 ∨ 4 = 4 ∧ 2 = 4hsum:4 + 2 = 4 + 8⊢ 4 = 4 ∧ 2 = 8 ∨ 4 = 8 ∧ 2 = 4hsum:4 + 2 = 4 + 13⊢ 4 = 4 ∧ 2 = 13 ∨ 4 = 13 ∧ 2 = 4hsum:4 + 4 = 4 + 1⊢ 4 = 4 ∧ 4 = 1 ∨ 4 = 1 ∧ 4 = 4hsum:4 + 4 = 4 + 2⊢ 4 = 4 ∧ 4 = 2 ∨ 4 = 2 ∧ 4 = 4hsum:4 + 4 = 4 + 4⊢ 4 = 4 ∧ 4 = 4 ∨ 4 = 4 ∧ 4 = 4hsum:4 + 4 = 4 + 8⊢ 4 = 4 ∧ 4 = 8 ∨ 4 = 8 ∧ 4 = 4hsum:4 + 4 = 4 + 13⊢ 4 = 4 ∧ 4 = 13 ∨ 4 = 13 ∧ 4 = 4hsum:4 + 8 = 4 + 1⊢ 4 = 4 ∧ 8 = 1 ∨ 4 = 1 ∧ 8 = 4hsum:4 + 8 = 4 + 2⊢ 4 = 4 ∧ 8 = 2 ∨ 4 = 2 ∧ 8 = 4hsum:4 + 8 = 4 + 4⊢ 4 = 4 ∧ 8 = 4 ∨ 4 = 4 ∧ 8 = 4hsum:4 + 8 = 4 + 8⊢ 4 = 4 ∧ 8 = 8 ∨ 4 = 8 ∧ 8 = 4hsum:4 + 8 = 4 + 13⊢ 4 = 4 ∧ 8 = 13 ∨ 4 = 13 ∧ 8 = 4hsum:4 + 13 = 4 + 1⊢ 4 = 4 ∧ 13 = 1 ∨ 4 = 1 ∧ 13 = 4hsum:4 + 13 = 4 + 2⊢ 4 = 4 ∧ 13 = 2 ∨ 4 = 2 ∧ 13 = 4hsum:4 + 13 = 4 + 4⊢ 4 = 4 ∧ 13 = 4 ∨ 4 = 4 ∧ 13 = 4hsum:4 + 13 = 4 + 8⊢ 4 = 4 ∧ 13 = 8 ∨ 4 = 8 ∧ 13 = 4hsum:4 + 13 = 4 + 13⊢ 4 = 4 ∧ 13 = 13 ∨ 4 = 13 ∧ 13 = 4hsum:4 + 1 = 8 + 1⊢ 4 = 8 ∧ 1 = 1 ∨ 4 = 1 ∧ 1 = 8hsum:4 + 1 = 8 + 2⊢ 4 = 8 ∧ 1 = 2 ∨ 4 = 2 ∧ 1 = 8hsum:4 + 1 = 8 + 4⊢ 4 = 8 ∧ 1 = 4 ∨ 4 = 4 ∧ 1 = 8hsum:4 + 1 = 8 + 8⊢ 4 = 8 ∧ 1 = 8 ∨ 4 = 8 ∧ 1 = 8hsum:4 + 1 = 8 + 13⊢ 4 = 8 ∧ 1 = 13 ∨ 4 = 13 ∧ 1 = 8hsum:4 + 2 = 8 + 1⊢ 4 = 8 ∧ 2 = 1 ∨ 4 = 1 ∧ 2 = 8hsum:4 + 2 = 8 + 2⊢ 4 = 8 ∧ 2 = 2 ∨ 4 = 2 ∧ 2 = 8hsum:4 + 2 = 8 + 4⊢ 4 = 8 ∧ 2 = 4 ∨ 4 = 4 ∧ 2 = 8hsum:4 + 2 = 8 + 8⊢ 4 = 8 ∧ 2 = 8 ∨ 4 = 8 ∧ 2 = 8hsum:4 + 2 = 8 + 13⊢ 4 = 8 ∧ 2 = 13 ∨ 4 = 13 ∧ 2 = 8hsum:4 + 4 = 8 + 1⊢ 4 = 8 ∧ 4 = 1 ∨ 4 = 1 ∧ 4 = 8hsum:4 + 4 = 8 + 2⊢ 4 = 8 ∧ 4 = 2 ∨ 4 = 2 ∧ 4 = 8hsum:4 + 4 = 8 + 4⊢ 4 = 8 ∧ 4 = 4 ∨ 4 = 4 ∧ 4 = 8hsum:4 + 4 = 8 + 8⊢ 4 = 8 ∧ 4 = 8 ∨ 4 = 8 ∧ 4 = 8hsum:4 + 4 = 8 + 13⊢ 4 = 8 ∧ 4 = 13 ∨ 4 = 13 ∧ 4 = 8hsum:4 + 8 = 8 + 1⊢ 4 = 8 ∧ 8 = 1 ∨ 4 = 1 ∧ 8 = 8hsum:4 + 8 = 8 + 2⊢ 4 = 8 ∧ 8 = 2 ∨ 4 = 2 ∧ 8 = 8hsum:4 + 8 = 8 + 4⊢ 4 = 8 ∧ 8 = 4 ∨ 4 = 4 ∧ 8 = 8hsum:4 + 8 = 8 + 8⊢ 4 = 8 ∧ 8 = 8 ∨ 4 = 8 ∧ 8 = 8hsum:4 + 8 = 8 + 13⊢ 4 = 8 ∧ 8 = 13 ∨ 4 = 13 ∧ 8 = 8hsum:4 + 13 = 8 + 1⊢ 4 = 8 ∧ 13 = 1 ∨ 4 = 1 ∧ 13 = 8hsum:4 + 13 = 8 + 2⊢ 4 = 8 ∧ 13 = 2 ∨ 4 = 2 ∧ 13 = 8hsum:4 + 13 = 8 + 4⊢ 4 = 8 ∧ 13 = 4 ∨ 4 = 4 ∧ 13 = 8hsum:4 + 13 = 8 + 8⊢ 4 = 8 ∧ 13 = 8 ∨ 4 = 8 ∧ 13 = 8hsum:4 + 13 = 8 + 13⊢ 4 = 8 ∧ 13 = 13 ∨ 4 = 13 ∧ 13 = 8hsum:4 + 1 = 13 + 1⊢ 4 = 13 ∧ 1 = 1 ∨ 4 = 1 ∧ 1 = 13hsum:4 + 1 = 13 + 2⊢ 4 = 13 ∧ 1 = 2 ∨ 4 = 2 ∧ 1 = 13hsum:4 + 1 = 13 + 4⊢ 4 = 13 ∧ 1 = 4 ∨ 4 = 4 ∧ 1 = 13hsum:4 + 1 = 13 + 8⊢ 4 = 13 ∧ 1 = 8 ∨ 4 = 8 ∧ 1 = 13hsum:4 + 1 = 13 + 13⊢ 4 = 13 ∧ 1 = 13 ∨ 4 = 13 ∧ 1 = 13hsum:4 + 2 = 13 + 1⊢ 4 = 13 ∧ 2 = 1 ∨ 4 = 1 ∧ 2 = 13hsum:4 + 2 = 13 + 2⊢ 4 = 13 ∧ 2 = 2 ∨ 4 = 2 ∧ 2 = 13hsum:4 + 2 = 13 + 4⊢ 4 = 13 ∧ 2 = 4 ∨ 4 = 4 ∧ 2 = 13hsum:4 + 2 = 13 + 8⊢ 4 = 13 ∧ 2 = 8 ∨ 4 = 8 ∧ 2 = 13hsum:4 + 2 = 13 + 13⊢ 4 = 13 ∧ 2 = 13 ∨ 4 = 13 ∧ 2 = 13hsum:4 + 4 = 13 + 1⊢ 4 = 13 ∧ 4 = 1 ∨ 4 = 1 ∧ 4 = 13hsum:4 + 4 = 13 + 2⊢ 4 = 13 ∧ 4 = 2 ∨ 4 = 2 ∧ 4 = 13hsum:4 + 4 = 13 + 4⊢ 4 = 13 ∧ 4 = 4 ∨ 4 = 4 ∧ 4 = 13hsum:4 + 4 = 13 + 8⊢ 4 = 13 ∧ 4 = 8 ∨ 4 = 8 ∧ 4 = 13hsum:4 + 4 = 13 + 13⊢ 4 = 13 ∧ 4 = 13 ∨ 4 = 13 ∧ 4 = 13hsum:4 + 8 = 13 + 1⊢ 4 = 13 ∧ 8 = 1 ∨ 4 = 1 ∧ 8 = 13hsum:4 + 8 = 13 + 2⊢ 4 = 13 ∧ 8 = 2 ∨ 4 = 2 ∧ 8 = 13hsum:4 + 8 = 13 + 4⊢ 4 = 13 ∧ 8 = 4 ∨ 4 = 4 ∧ 8 = 13hsum:4 + 8 = 13 + 8⊢ 4 = 13 ∧ 8 = 8 ∨ 4 = 8 ∧ 8 = 13hsum:4 + 8 = 13 + 13⊢ 4 = 13 ∧ 8 = 13 ∨ 4 = 13 ∧ 8 = 13hsum:4 + 13 = 13 + 1⊢ 4 = 13 ∧ 13 = 1 ∨ 4 = 1 ∧ 13 = 13hsum:4 + 13 = 13 + 2⊢ 4 = 13 ∧ 13 = 2 ∨ 4 = 2 ∧ 13 = 13hsum:4 + 13 = 13 + 4⊢ 4 = 13 ∧ 13 = 4 ∨ 4 = 4 ∧ 13 = 13hsum:4 + 13 = 13 + 8⊢ 4 = 13 ∧ 13 = 8 ∨ 4 = 8 ∧ 13 = 13hsum:4 + 13 = 13 + 13⊢ 4 = 13 ∧ 13 = 13 ∨ 4 = 13 ∧ 13 = 13hsum:8 + 1 = 1 + 1⊢ 8 = 1 ∧ 1 = 1 ∨ 8 = 1 ∧ 1 = 1hsum:8 + 1 = 1 + 2⊢ 8 = 1 ∧ 1 = 2 ∨ 8 = 2 ∧ 1 = 1hsum:8 + 1 = 1 + 4⊢ 8 = 1 ∧ 1 = 4 ∨ 8 = 4 ∧ 1 = 1hsum:8 + 1 = 1 + 8⊢ 8 = 1 ∧ 1 = 8 ∨ 8 = 8 ∧ 1 = 1hsum:8 + 1 = 1 + 13⊢ 8 = 1 ∧ 1 = 13 ∨ 8 = 13 ∧ 1 = 1hsum:8 + 2 = 1 + 1⊢ 8 = 1 ∧ 2 = 1 ∨ 8 = 1 ∧ 2 = 1hsum:8 + 2 = 1 + 2⊢ 8 = 1 ∧ 2 = 2 ∨ 8 = 2 ∧ 2 = 1hsum:8 + 2 = 1 + 4⊢ 8 = 1 ∧ 2 = 4 ∨ 8 = 4 ∧ 2 = 1hsum:8 + 2 = 1 + 8⊢ 8 = 1 ∧ 2 = 8 ∨ 8 = 8 ∧ 2 = 1hsum:8 + 2 = 1 + 13⊢ 8 = 1 ∧ 2 = 13 ∨ 8 = 13 ∧ 2 = 1hsum:8 + 4 = 1 + 1⊢ 8 = 1 ∧ 4 = 1 ∨ 8 = 1 ∧ 4 = 1hsum:8 + 4 = 1 + 2⊢ 8 = 1 ∧ 4 = 2 ∨ 8 = 2 ∧ 4 = 1hsum:8 + 4 = 1 + 4⊢ 8 = 1 ∧ 4 = 4 ∨ 8 = 4 ∧ 4 = 1hsum:8 + 4 = 1 + 8⊢ 8 = 1 ∧ 4 = 8 ∨ 8 = 8 ∧ 4 = 1hsum:8 + 4 = 1 + 13⊢ 8 = 1 ∧ 4 = 13 ∨ 8 = 13 ∧ 4 = 1hsum:8 + 8 = 1 + 1⊢ 8 = 1 ∧ 8 = 1 ∨ 8 = 1 ∧ 8 = 1hsum:8 + 8 = 1 + 2⊢ 8 = 1 ∧ 8 = 2 ∨ 8 = 2 ∧ 8 = 1hsum:8 + 8 = 1 + 4⊢ 8 = 1 ∧ 8 = 4 ∨ 8 = 4 ∧ 8 = 1hsum:8 + 8 = 1 + 8⊢ 8 = 1 ∧ 8 = 8 ∨ 8 = 8 ∧ 8 = 1hsum:8 + 8 = 1 + 13⊢ 8 = 1 ∧ 8 = 13 ∨ 8 = 13 ∧ 8 = 1hsum:8 + 13 = 1 + 1⊢ 8 = 1 ∧ 13 = 1 ∨ 8 = 1 ∧ 13 = 1hsum:8 + 13 = 1 + 2⊢ 8 = 1 ∧ 13 = 2 ∨ 8 = 2 ∧ 13 = 1hsum:8 + 13 = 1 + 4⊢ 8 = 1 ∧ 13 = 4 ∨ 8 = 4 ∧ 13 = 1hsum:8 + 13 = 1 + 8⊢ 8 = 1 ∧ 13 = 8 ∨ 8 = 8 ∧ 13 = 1hsum:8 + 13 = 1 + 13⊢ 8 = 1 ∧ 13 = 13 ∨ 8 = 13 ∧ 13 = 1hsum:8 + 1 = 2 + 1⊢ 8 = 2 ∧ 1 = 1 ∨ 8 = 1 ∧ 1 = 2hsum:8 + 1 = 2 + 2⊢ 8 = 2 ∧ 1 = 2 ∨ 8 = 2 ∧ 1 = 2hsum:8 + 1 = 2 + 4⊢ 8 = 2 ∧ 1 = 4 ∨ 8 = 4 ∧ 1 = 2hsum:8 + 1 = 2 + 8⊢ 8 = 2 ∧ 1 = 8 ∨ 8 = 8 ∧ 1 = 2hsum:8 + 1 = 2 + 13⊢ 8 = 2 ∧ 1 = 13 ∨ 8 = 13 ∧ 1 = 2hsum:8 + 2 = 2 + 1⊢ 8 = 2 ∧ 2 = 1 ∨ 8 = 1 ∧ 2 = 2hsum:8 + 2 = 2 + 2⊢ 8 = 2 ∧ 2 = 2 ∨ 8 = 2 ∧ 2 = 2hsum:8 + 2 = 2 + 4⊢ 8 = 2 ∧ 2 = 4 ∨ 8 = 4 ∧ 2 = 2hsum:8 + 2 = 2 + 8⊢ 8 = 2 ∧ 2 = 8 ∨ 8 = 8 ∧ 2 = 2hsum:8 + 2 = 2 + 13⊢ 8 = 2 ∧ 2 = 13 ∨ 8 = 13 ∧ 2 = 2hsum:8 + 4 = 2 + 1⊢ 8 = 2 ∧ 4 = 1 ∨ 8 = 1 ∧ 4 = 2hsum:8 + 4 = 2 + 2⊢ 8 = 2 ∧ 4 = 2 ∨ 8 = 2 ∧ 4 = 2hsum:8 + 4 = 2 + 4⊢ 8 = 2 ∧ 4 = 4 ∨ 8 = 4 ∧ 4 = 2hsum:8 + 4 = 2 + 8⊢ 8 = 2 ∧ 4 = 8 ∨ 8 = 8 ∧ 4 = 2hsum:8 + 4 = 2 + 13⊢ 8 = 2 ∧ 4 = 13 ∨ 8 = 13 ∧ 4 = 2hsum:8 + 8 = 2 + 1⊢ 8 = 2 ∧ 8 = 1 ∨ 8 = 1 ∧ 8 = 2hsum:8 + 8 = 2 + 2⊢ 8 = 2 ∧ 8 = 2 ∨ 8 = 2 ∧ 8 = 2hsum:8 + 8 = 2 + 4⊢ 8 = 2 ∧ 8 = 4 ∨ 8 = 4 ∧ 8 = 2hsum:8 + 8 = 2 + 8⊢ 8 = 2 ∧ 8 = 8 ∨ 8 = 8 ∧ 8 = 2hsum:8 + 8 = 2 + 13⊢ 8 = 2 ∧ 8 = 13 ∨ 8 = 13 ∧ 8 = 2hsum:8 + 13 = 2 + 1⊢ 8 = 2 ∧ 13 = 1 ∨ 8 = 1 ∧ 13 = 2hsum:8 + 13 = 2 + 2⊢ 8 = 2 ∧ 13 = 2 ∨ 8 = 2 ∧ 13 = 2hsum:8 + 13 = 2 + 4⊢ 8 = 2 ∧ 13 = 4 ∨ 8 = 4 ∧ 13 = 2hsum:8 + 13 = 2 + 8⊢ 8 = 2 ∧ 13 = 8 ∨ 8 = 8 ∧ 13 = 2hsum:8 + 13 = 2 + 13⊢ 8 = 2 ∧ 13 = 13 ∨ 8 = 13 ∧ 13 = 2hsum:8 + 1 = 4 + 1⊢ 8 = 4 ∧ 1 = 1 ∨ 8 = 1 ∧ 1 = 4hsum:8 + 1 = 4 + 2⊢ 8 = 4 ∧ 1 = 2 ∨ 8 = 2 ∧ 1 = 4hsum:8 + 1 = 4 + 4⊢ 8 = 4 ∧ 1 = 4 ∨ 8 = 4 ∧ 1 = 4hsum:8 + 1 = 4 + 8⊢ 8 = 4 ∧ 1 = 8 ∨ 8 = 8 ∧ 1 = 4hsum:8 + 1 = 4 + 13⊢ 8 = 4 ∧ 1 = 13 ∨ 8 = 13 ∧ 1 = 4hsum:8 + 2 = 4 + 1⊢ 8 = 4 ∧ 2 = 1 ∨ 8 = 1 ∧ 2 = 4hsum:8 + 2 = 4 + 2⊢ 8 = 4 ∧ 2 = 2 ∨ 8 = 2 ∧ 2 = 4hsum:8 + 2 = 4 + 4⊢ 8 = 4 ∧ 2 = 4 ∨ 8 = 4 ∧ 2 = 4hsum:8 + 2 = 4 + 8⊢ 8 = 4 ∧ 2 = 8 ∨ 8 = 8 ∧ 2 = 4hsum:8 + 2 = 4 + 13⊢ 8 = 4 ∧ 2 = 13 ∨ 8 = 13 ∧ 2 = 4hsum:8 + 4 = 4 + 1⊢ 8 = 4 ∧ 4 = 1 ∨ 8 = 1 ∧ 4 = 4hsum:8 + 4 = 4 + 2⊢ 8 = 4 ∧ 4 = 2 ∨ 8 = 2 ∧ 4 = 4hsum:8 + 4 = 4 + 4⊢ 8 = 4 ∧ 4 = 4 ∨ 8 = 4 ∧ 4 = 4hsum:8 + 4 = 4 + 8⊢ 8 = 4 ∧ 4 = 8 ∨ 8 = 8 ∧ 4 = 4hsum:8 + 4 = 4 + 13⊢ 8 = 4 ∧ 4 = 13 ∨ 8 = 13 ∧ 4 = 4hsum:8 + 8 = 4 + 1⊢ 8 = 4 ∧ 8 = 1 ∨ 8 = 1 ∧ 8 = 4hsum:8 + 8 = 4 + 2⊢ 8 = 4 ∧ 8 = 2 ∨ 8 = 2 ∧ 8 = 4hsum:8 + 8 = 4 + 4⊢ 8 = 4 ∧ 8 = 4 ∨ 8 = 4 ∧ 8 = 4hsum:8 + 8 = 4 + 8⊢ 8 = 4 ∧ 8 = 8 ∨ 8 = 8 ∧ 8 = 4hsum:8 + 8 = 4 + 13⊢ 8 = 4 ∧ 8 = 13 ∨ 8 = 13 ∧ 8 = 4hsum:8 + 13 = 4 + 1⊢ 8 = 4 ∧ 13 = 1 ∨ 8 = 1 ∧ 13 = 4hsum:8 + 13 = 4 + 2⊢ 8 = 4 ∧ 13 = 2 ∨ 8 = 2 ∧ 13 = 4hsum:8 + 13 = 4 + 4⊢ 8 = 4 ∧ 13 = 4 ∨ 8 = 4 ∧ 13 = 4hsum:8 + 13 = 4 + 8⊢ 8 = 4 ∧ 13 = 8 ∨ 8 = 8 ∧ 13 = 4hsum:8 + 13 = 4 + 13⊢ 8 = 4 ∧ 13 = 13 ∨ 8 = 13 ∧ 13 = 4hsum:8 + 1 = 8 + 1⊢ 8 = 8 ∧ 1 = 1 ∨ 8 = 1 ∧ 1 = 8hsum:8 + 1 = 8 + 2⊢ 8 = 8 ∧ 1 = 2 ∨ 8 = 2 ∧ 1 = 8hsum:8 + 1 = 8 + 4⊢ 8 = 8 ∧ 1 = 4 ∨ 8 = 4 ∧ 1 = 8hsum:8 + 1 = 8 + 8⊢ 8 = 8 ∧ 1 = 8 ∨ 8 = 8 ∧ 1 = 8hsum:8 + 1 = 8 + 13⊢ 8 = 8 ∧ 1 = 13 ∨ 8 = 13 ∧ 1 = 8hsum:8 + 2 = 8 + 1⊢ 8 = 8 ∧ 2 = 1 ∨ 8 = 1 ∧ 2 = 8hsum:8 + 2 = 8 + 2⊢ 8 = 8 ∧ 2 = 2 ∨ 8 = 2 ∧ 2 = 8hsum:8 + 2 = 8 + 4⊢ 8 = 8 ∧ 2 = 4 ∨ 8 = 4 ∧ 2 = 8hsum:8 + 2 = 8 + 8⊢ 8 = 8 ∧ 2 = 8 ∨ 8 = 8 ∧ 2 = 8hsum:8 + 2 = 8 + 13⊢ 8 = 8 ∧ 2 = 13 ∨ 8 = 13 ∧ 2 = 8hsum:8 + 4 = 8 + 1⊢ 8 = 8 ∧ 4 = 1 ∨ 8 = 1 ∧ 4 = 8hsum:8 + 4 = 8 + 2⊢ 8 = 8 ∧ 4 = 2 ∨ 8 = 2 ∧ 4 = 8hsum:8 + 4 = 8 + 4⊢ 8 = 8 ∧ 4 = 4 ∨ 8 = 4 ∧ 4 = 8hsum:8 + 4 = 8 + 8⊢ 8 = 8 ∧ 4 = 8 ∨ 8 = 8 ∧ 4 = 8hsum:8 + 4 = 8 + 13⊢ 8 = 8 ∧ 4 = 13 ∨ 8 = 13 ∧ 4 = 8hsum:8 + 8 = 8 + 1⊢ 8 = 8 ∧ 8 = 1 ∨ 8 = 1 ∧ 8 = 8hsum:8 + 8 = 8 + 2⊢ 8 = 8 ∧ 8 = 2 ∨ 8 = 2 ∧ 8 = 8hsum:8 + 8 = 8 + 4⊢ 8 = 8 ∧ 8 = 4 ∨ 8 = 4 ∧ 8 = 8hsum:8 + 8 = 8 + 8⊢ 8 = 8 ∧ 8 = 8 ∨ 8 = 8 ∧ 8 = 8hsum:8 + 8 = 8 + 13⊢ 8 = 8 ∧ 8 = 13 ∨ 8 = 13 ∧ 8 = 8hsum:8 + 13 = 8 + 1⊢ 8 = 8 ∧ 13 = 1 ∨ 8 = 1 ∧ 13 = 8hsum:8 + 13 = 8 + 2⊢ 8 = 8 ∧ 13 = 2 ∨ 8 = 2 ∧ 13 = 8hsum:8 + 13 = 8 + 4⊢ 8 = 8 ∧ 13 = 4 ∨ 8 = 4 ∧ 13 = 8hsum:8 + 13 = 8 + 8⊢ 8 = 8 ∧ 13 = 8 ∨ 8 = 8 ∧ 13 = 8hsum:8 + 13 = 8 + 13⊢ 8 = 8 ∧ 13 = 13 ∨ 8 = 13 ∧ 13 = 8hsum:8 + 1 = 13 + 1⊢ 8 = 13 ∧ 1 = 1 ∨ 8 = 1 ∧ 1 = 13hsum:8 + 1 = 13 + 2⊢ 8 = 13 ∧ 1 = 2 ∨ 8 = 2 ∧ 1 = 13hsum:8 + 1 = 13 + 4⊢ 8 = 13 ∧ 1 = 4 ∨ 8 = 4 ∧ 1 = 13hsum:8 + 1 = 13 + 8⊢ 8 = 13 ∧ 1 = 8 ∨ 8 = 8 ∧ 1 = 13hsum:8 + 1 = 13 + 13⊢ 8 = 13 ∧ 1 = 13 ∨ 8 = 13 ∧ 1 = 13hsum:8 + 2 = 13 + 1⊢ 8 = 13 ∧ 2 = 1 ∨ 8 = 1 ∧ 2 = 13hsum:8 + 2 = 13 + 2⊢ 8 = 13 ∧ 2 = 2 ∨ 8 = 2 ∧ 2 = 13hsum:8 + 2 = 13 + 4⊢ 8 = 13 ∧ 2 = 4 ∨ 8 = 4 ∧ 2 = 13hsum:8 + 2 = 13 + 8⊢ 8 = 13 ∧ 2 = 8 ∨ 8 = 8 ∧ 2 = 13hsum:8 + 2 = 13 + 13⊢ 8 = 13 ∧ 2 = 13 ∨ 8 = 13 ∧ 2 = 13hsum:8 + 4 = 13 + 1⊢ 8 = 13 ∧ 4 = 1 ∨ 8 = 1 ∧ 4 = 13hsum:8 + 4 = 13 + 2⊢ 8 = 13 ∧ 4 = 2 ∨ 8 = 2 ∧ 4 = 13hsum:8 + 4 = 13 + 4⊢ 8 = 13 ∧ 4 = 4 ∨ 8 = 4 ∧ 4 = 13hsum:8 + 4 = 13 + 8⊢ 8 = 13 ∧ 4 = 8 ∨ 8 = 8 ∧ 4 = 13hsum:8 + 4 = 13 + 13⊢ 8 = 13 ∧ 4 = 13 ∨ 8 = 13 ∧ 4 = 13hsum:8 + 8 = 13 + 1⊢ 8 = 13 ∧ 8 = 1 ∨ 8 = 1 ∧ 8 = 13hsum:8 + 8 = 13 + 2⊢ 8 = 13 ∧ 8 = 2 ∨ 8 = 2 ∧ 8 = 13hsum:8 + 8 = 13 + 4⊢ 8 = 13 ∧ 8 = 4 ∨ 8 = 4 ∧ 8 = 13hsum:8 + 8 = 13 + 8⊢ 8 = 13 ∧ 8 = 8 ∨ 8 = 8 ∧ 8 = 13hsum:8 + 8 = 13 + 13⊢ 8 = 13 ∧ 8 = 13 ∨ 8 = 13 ∧ 8 = 13hsum:8 + 13 = 13 + 1⊢ 8 = 13 ∧ 13 = 1 ∨ 8 = 1 ∧ 13 = 13hsum:8 + 13 = 13 + 2⊢ 8 = 13 ∧ 13 = 2 ∨ 8 = 2 ∧ 13 = 13hsum:8 + 13 = 13 + 4⊢ 8 = 13 ∧ 13 = 4 ∨ 8 = 4 ∧ 13 = 13hsum:8 + 13 = 13 + 8⊢ 8 = 13 ∧ 13 = 8 ∨ 8 = 8 ∧ 13 = 13hsum:8 + 13 = 13 + 13⊢ 8 = 13 ∧ 13 = 13 ∨ 8 = 13 ∧ 13 = 13hsum:13 + 1 = 1 + 1⊢ 13 = 1 ∧ 1 = 1 ∨ 13 = 1 ∧ 1 = 1hsum:13 + 1 = 1 + 2⊢ 13 = 1 ∧ 1 = 2 ∨ 13 = 2 ∧ 1 = 1hsum:13 + 1 = 1 + 4⊢ 13 = 1 ∧ 1 = 4 ∨ 13 = 4 ∧ 1 = 1hsum:13 + 1 = 1 + 8⊢ 13 = 1 ∧ 1 = 8 ∨ 13 = 8 ∧ 1 = 1hsum:13 + 1 = 1 + 13⊢ 13 = 1 ∧ 1 = 13 ∨ 13 = 13 ∧ 1 = 1hsum:13 + 2 = 1 + 1⊢ 13 = 1 ∧ 2 = 1 ∨ 13 = 1 ∧ 2 = 1hsum:13 + 2 = 1 + 2⊢ 13 = 1 ∧ 2 = 2 ∨ 13 = 2 ∧ 2 = 1hsum:13 + 2 = 1 + 4⊢ 13 = 1 ∧ 2 = 4 ∨ 13 = 4 ∧ 2 = 1hsum:13 + 2 = 1 + 8⊢ 13 = 1 ∧ 2 = 8 ∨ 13 = 8 ∧ 2 = 1hsum:13 + 2 = 1 + 13⊢ 13 = 1 ∧ 2 = 13 ∨ 13 = 13 ∧ 2 = 1hsum:13 + 4 = 1 + 1⊢ 13 = 1 ∧ 4 = 1 ∨ 13 = 1 ∧ 4 = 1hsum:13 + 4 = 1 + 2⊢ 13 = 1 ∧ 4 = 2 ∨ 13 = 2 ∧ 4 = 1hsum:13 + 4 = 1 + 4⊢ 13 = 1 ∧ 4 = 4 ∨ 13 = 4 ∧ 4 = 1hsum:13 + 4 = 1 + 8⊢ 13 = 1 ∧ 4 = 8 ∨ 13 = 8 ∧ 4 = 1hsum:13 + 4 = 1 + 13⊢ 13 = 1 ∧ 4 = 13 ∨ 13 = 13 ∧ 4 = 1hsum:13 + 8 = 1 + 1⊢ 13 = 1 ∧ 8 = 1 ∨ 13 = 1 ∧ 8 = 1hsum:13 + 8 = 1 + 2⊢ 13 = 1 ∧ 8 = 2 ∨ 13 = 2 ∧ 8 = 1hsum:13 + 8 = 1 + 4⊢ 13 = 1 ∧ 8 = 4 ∨ 13 = 4 ∧ 8 = 1hsum:13 + 8 = 1 + 8⊢ 13 = 1 ∧ 8 = 8 ∨ 13 = 8 ∧ 8 = 1hsum:13 + 8 = 1 + 13⊢ 13 = 1 ∧ 8 = 13 ∨ 13 = 13 ∧ 8 = 1hsum:13 + 13 = 1 + 1⊢ 13 = 1 ∧ 13 = 1 ∨ 13 = 1 ∧ 13 = 1hsum:13 + 13 = 1 + 2⊢ 13 = 1 ∧ 13 = 2 ∨ 13 = 2 ∧ 13 = 1hsum:13 + 13 = 1 + 4⊢ 13 = 1 ∧ 13 = 4 ∨ 13 = 4 ∧ 13 = 1hsum:13 + 13 = 1 + 8⊢ 13 = 1 ∧ 13 = 8 ∨ 13 = 8 ∧ 13 = 1hsum:13 + 13 = 1 + 13⊢ 13 = 1 ∧ 13 = 13 ∨ 13 = 13 ∧ 13 = 1hsum:13 + 1 = 2 + 1⊢ 13 = 2 ∧ 1 = 1 ∨ 13 = 1 ∧ 1 = 2hsum:13 + 1 = 2 + 2⊢ 13 = 2 ∧ 1 = 2 ∨ 13 = 2 ∧ 1 = 2hsum:13 + 1 = 2 + 4⊢ 13 = 2 ∧ 1 = 4 ∨ 13 = 4 ∧ 1 = 2hsum:13 + 1 = 2 + 8⊢ 13 = 2 ∧ 1 = 8 ∨ 13 = 8 ∧ 1 = 2hsum:13 + 1 = 2 + 13⊢ 13 = 2 ∧ 1 = 13 ∨ 13 = 13 ∧ 1 = 2hsum:13 + 2 = 2 + 1⊢ 13 = 2 ∧ 2 = 1 ∨ 13 = 1 ∧ 2 = 2hsum:13 + 2 = 2 + 2⊢ 13 = 2 ∧ 2 = 2 ∨ 13 = 2 ∧ 2 = 2hsum:13 + 2 = 2 + 4⊢ 13 = 2 ∧ 2 = 4 ∨ 13 = 4 ∧ 2 = 2hsum:13 + 2 = 2 + 8⊢ 13 = 2 ∧ 2 = 8 ∨ 13 = 8 ∧ 2 = 2hsum:13 + 2 = 2 + 13⊢ 13 = 2 ∧ 2 = 13 ∨ 13 = 13 ∧ 2 = 2hsum:13 + 4 = 2 + 1⊢ 13 = 2 ∧ 4 = 1 ∨ 13 = 1 ∧ 4 = 2hsum:13 + 4 = 2 + 2⊢ 13 = 2 ∧ 4 = 2 ∨ 13 = 2 ∧ 4 = 2hsum:13 + 4 = 2 + 4⊢ 13 = 2 ∧ 4 = 4 ∨ 13 = 4 ∧ 4 = 2hsum:13 + 4 = 2 + 8⊢ 13 = 2 ∧ 4 = 8 ∨ 13 = 8 ∧ 4 = 2hsum:13 + 4 = 2 + 13⊢ 13 = 2 ∧ 4 = 13 ∨ 13 = 13 ∧ 4 = 2hsum:13 + 8 = 2 + 1⊢ 13 = 2 ∧ 8 = 1 ∨ 13 = 1 ∧ 8 = 2hsum:13 + 8 = 2 + 2⊢ 13 = 2 ∧ 8 = 2 ∨ 13 = 2 ∧ 8 = 2hsum:13 + 8 = 2 + 4⊢ 13 = 2 ∧ 8 = 4 ∨ 13 = 4 ∧ 8 = 2hsum:13 + 8 = 2 + 8⊢ 13 = 2 ∧ 8 = 8 ∨ 13 = 8 ∧ 8 = 2hsum:13 + 8 = 2 + 13⊢ 13 = 2 ∧ 8 = 13 ∨ 13 = 13 ∧ 8 = 2hsum:13 + 13 = 2 + 1⊢ 13 = 2 ∧ 13 = 1 ∨ 13 = 1 ∧ 13 = 2hsum:13 + 13 = 2 + 2⊢ 13 = 2 ∧ 13 = 2 ∨ 13 = 2 ∧ 13 = 2hsum:13 + 13 = 2 + 4⊢ 13 = 2 ∧ 13 = 4 ∨ 13 = 4 ∧ 13 = 2hsum:13 + 13 = 2 + 8⊢ 13 = 2 ∧ 13 = 8 ∨ 13 = 8 ∧ 13 = 2hsum:13 + 13 = 2 + 13⊢ 13 = 2 ∧ 13 = 13 ∨ 13 = 13 ∧ 13 = 2hsum:13 + 1 = 4 + 1⊢ 13 = 4 ∧ 1 = 1 ∨ 13 = 1 ∧ 1 = 4hsum:13 + 1 = 4 + 2⊢ 13 = 4 ∧ 1 = 2 ∨ 13 = 2 ∧ 1 = 4hsum:13 + 1 = 4 + 4⊢ 13 = 4 ∧ 1 = 4 ∨ 13 = 4 ∧ 1 = 4hsum:13 + 1 = 4 + 8⊢ 13 = 4 ∧ 1 = 8 ∨ 13 = 8 ∧ 1 = 4hsum:13 + 1 = 4 + 13⊢ 13 = 4 ∧ 1 = 13 ∨ 13 = 13 ∧ 1 = 4hsum:13 + 2 = 4 + 1⊢ 13 = 4 ∧ 2 = 1 ∨ 13 = 1 ∧ 2 = 4hsum:13 + 2 = 4 + 2⊢ 13 = 4 ∧ 2 = 2 ∨ 13 = 2 ∧ 2 = 4hsum:13 + 2 = 4 + 4⊢ 13 = 4 ∧ 2 = 4 ∨ 13 = 4 ∧ 2 = 4hsum:13 + 2 = 4 + 8⊢ 13 = 4 ∧ 2 = 8 ∨ 13 = 8 ∧ 2 = 4hsum:13 + 2 = 4 + 13⊢ 13 = 4 ∧ 2 = 13 ∨ 13 = 13 ∧ 2 = 4hsum:13 + 4 = 4 + 1⊢ 13 = 4 ∧ 4 = 1 ∨ 13 = 1 ∧ 4 = 4hsum:13 + 4 = 4 + 2⊢ 13 = 4 ∧ 4 = 2 ∨ 13 = 2 ∧ 4 = 4hsum:13 + 4 = 4 + 4⊢ 13 = 4 ∧ 4 = 4 ∨ 13 = 4 ∧ 4 = 4hsum:13 + 4 = 4 + 8⊢ 13 = 4 ∧ 4 = 8 ∨ 13 = 8 ∧ 4 = 4hsum:13 + 4 = 4 + 13⊢ 13 = 4 ∧ 4 = 13 ∨ 13 = 13 ∧ 4 = 4hsum:13 + 8 = 4 + 1⊢ 13 = 4 ∧ 8 = 1 ∨ 13 = 1 ∧ 8 = 4hsum:13 + 8 = 4 + 2⊢ 13 = 4 ∧ 8 = 2 ∨ 13 = 2 ∧ 8 = 4hsum:13 + 8 = 4 + 4⊢ 13 = 4 ∧ 8 = 4 ∨ 13 = 4 ∧ 8 = 4hsum:13 + 8 = 4 + 8⊢ 13 = 4 ∧ 8 = 8 ∨ 13 = 8 ∧ 8 = 4hsum:13 + 8 = 4 + 13⊢ 13 = 4 ∧ 8 = 13 ∨ 13 = 13 ∧ 8 = 4hsum:13 + 13 = 4 + 1⊢ 13 = 4 ∧ 13 = 1 ∨ 13 = 1 ∧ 13 = 4hsum:13 + 13 = 4 + 2⊢ 13 = 4 ∧ 13 = 2 ∨ 13 = 2 ∧ 13 = 4hsum:13 + 13 = 4 + 4⊢ 13 = 4 ∧ 13 = 4 ∨ 13 = 4 ∧ 13 = 4hsum:13 + 13 = 4 + 8⊢ 13 = 4 ∧ 13 = 8 ∨ 13 = 8 ∧ 13 = 4hsum:13 + 13 = 4 + 13⊢ 13 = 4 ∧ 13 = 13 ∨ 13 = 13 ∧ 13 = 4hsum:13 + 1 = 8 + 1⊢ 13 = 8 ∧ 1 = 1 ∨ 13 = 1 ∧ 1 = 8hsum:13 + 1 = 8 + 2⊢ 13 = 8 ∧ 1 = 2 ∨ 13 = 2 ∧ 1 = 8hsum:13 + 1 = 8 + 4⊢ 13 = 8 ∧ 1 = 4 ∨ 13 = 4 ∧ 1 = 8hsum:13 + 1 = 8 + 8⊢ 13 = 8 ∧ 1 = 8 ∨ 13 = 8 ∧ 1 = 8hsum:13 + 1 = 8 + 13⊢ 13 = 8 ∧ 1 = 13 ∨ 13 = 13 ∧ 1 = 8hsum:13 + 2 = 8 + 1⊢ 13 = 8 ∧ 2 = 1 ∨ 13 = 1 ∧ 2 = 8hsum:13 + 2 = 8 + 2⊢ 13 = 8 ∧ 2 = 2 ∨ 13 = 2 ∧ 2 = 8hsum:13 + 2 = 8 + 4⊢ 13 = 8 ∧ 2 = 4 ∨ 13 = 4 ∧ 2 = 8hsum:13 + 2 = 8 + 8⊢ 13 = 8 ∧ 2 = 8 ∨ 13 = 8 ∧ 2 = 8hsum:13 + 2 = 8 + 13⊢ 13 = 8 ∧ 2 = 13 ∨ 13 = 13 ∧ 2 = 8hsum:13 + 4 = 8 + 1⊢ 13 = 8 ∧ 4 = 1 ∨ 13 = 1 ∧ 4 = 8hsum:13 + 4 = 8 + 2⊢ 13 = 8 ∧ 4 = 2 ∨ 13 = 2 ∧ 4 = 8hsum:13 + 4 = 8 + 4⊢ 13 = 8 ∧ 4 = 4 ∨ 13 = 4 ∧ 4 = 8hsum:13 + 4 = 8 + 8⊢ 13 = 8 ∧ 4 = 8 ∨ 13 = 8 ∧ 4 = 8hsum:13 + 4 = 8 + 13⊢ 13 = 8 ∧ 4 = 13 ∨ 13 = 13 ∧ 4 = 8hsum:13 + 8 = 8 + 1⊢ 13 = 8 ∧ 8 = 1 ∨ 13 = 1 ∧ 8 = 8hsum:13 + 8 = 8 + 2⊢ 13 = 8 ∧ 8 = 2 ∨ 13 = 2 ∧ 8 = 8hsum:13 + 8 = 8 + 4⊢ 13 = 8 ∧ 8 = 4 ∨ 13 = 4 ∧ 8 = 8hsum:13 + 8 = 8 + 8⊢ 13 = 8 ∧ 8 = 8 ∨ 13 = 8 ∧ 8 = 8hsum:13 + 8 = 8 + 13⊢ 13 = 8 ∧ 8 = 13 ∨ 13 = 13 ∧ 8 = 8hsum:13 + 13 = 8 + 1⊢ 13 = 8 ∧ 13 = 1 ∨ 13 = 1 ∧ 13 = 8hsum:13 + 13 = 8 + 2⊢ 13 = 8 ∧ 13 = 2 ∨ 13 = 2 ∧ 13 = 8hsum:13 + 13 = 8 + 4⊢ 13 = 8 ∧ 13 = 4 ∨ 13 = 4 ∧ 13 = 8hsum:13 + 13 = 8 + 8⊢ 13 = 8 ∧ 13 = 8 ∨ 13 = 8 ∧ 13 = 8hsum:13 + 13 = 8 + 13⊢ 13 = 8 ∧ 13 = 13 ∨ 13 = 13 ∧ 13 = 8hsum:13 + 1 = 13 + 1⊢ 13 = 13 ∧ 1 = 1 ∨ 13 = 1 ∧ 1 = 13hsum:13 + 1 = 13 + 2⊢ 13 = 13 ∧ 1 = 2 ∨ 13 = 2 ∧ 1 = 13hsum:13 + 1 = 13 + 4⊢ 13 = 13 ∧ 1 = 4 ∨ 13 = 4 ∧ 1 = 13hsum:13 + 1 = 13 + 8⊢ 13 = 13 ∧ 1 = 8 ∨ 13 = 8 ∧ 1 = 13hsum:13 + 1 = 13 + 13⊢ 13 = 13 ∧ 1 = 13 ∨ 13 = 13 ∧ 1 = 13hsum:13 + 2 = 13 + 1⊢ 13 = 13 ∧ 2 = 1 ∨ 13 = 1 ∧ 2 = 13hsum:13 + 2 = 13 + 2⊢ 13 = 13 ∧ 2 = 2 ∨ 13 = 2 ∧ 2 = 13hsum:13 + 2 = 13 + 4⊢ 13 = 13 ∧ 2 = 4 ∨ 13 = 4 ∧ 2 = 13hsum:13 + 2 = 13 + 8⊢ 13 = 13 ∧ 2 = 8 ∨ 13 = 8 ∧ 2 = 13hsum:13 + 2 = 13 + 13⊢ 13 = 13 ∧ 2 = 13 ∨ 13 = 13 ∧ 2 = 13hsum:13 + 4 = 13 + 1⊢ 13 = 13 ∧ 4 = 1 ∨ 13 = 1 ∧ 4 = 13hsum:13 + 4 = 13 + 2⊢ 13 = 13 ∧ 4 = 2 ∨ 13 = 2 ∧ 4 = 13hsum:13 + 4 = 13 + 4⊢ 13 = 13 ∧ 4 = 4 ∨ 13 = 4 ∧ 4 = 13hsum:13 + 4 = 13 + 8⊢ 13 = 13 ∧ 4 = 8 ∨ 13 = 8 ∧ 4 = 13hsum:13 + 4 = 13 + 13⊢ 13 = 13 ∧ 4 = 13 ∨ 13 = 13 ∧ 4 = 13hsum:13 + 8 = 13 + 1⊢ 13 = 13 ∧ 8 = 1 ∨ 13 = 1 ∧ 8 = 13hsum:13 + 8 = 13 + 2⊢ 13 = 13 ∧ 8 = 2 ∨ 13 = 2 ∧ 8 = 13hsum:13 + 8 = 13 + 4⊢ 13 = 13 ∧ 8 = 4 ∨ 13 = 4 ∧ 8 = 13hsum:13 + 8 = 13 + 8⊢ 13 = 13 ∧ 8 = 8 ∨ 13 = 8 ∧ 8 = 13hsum:13 + 8 = 13 + 13⊢ 13 = 13 ∧ 8 = 13 ∨ 13 = 13 ∧ 8 = 13hsum:13 + 13 = 13 + 1⊢ 13 = 13 ∧ 13 = 1 ∨ 13 = 1 ∧ 13 = 13hsum:13 + 13 = 13 + 2⊢ 13 = 13 ∧ 13 = 2 ∨ 13 = 2 ∧ 13 = 13hsum:13 + 13 = 13 + 4⊢ 13 = 13 ∧ 13 = 4 ∨ 13 = 4 ∧ 13 = 13hsum:13 + 13 = 13 + 8⊢ 13 = 13 ∧ 13 = 8 ∨ 13 = 8 ∧ 13 = 13hsum:13 + 13 = 13 + 13⊢ 13 = 13 ∧ 13 = 13 ∨ 13 = 13 ∧ 13 = 13 All goals completed! 🐙

For any N, there exists a Sidon set of size at least √N/2.

@[category textbook, AMS 5 11] theorem declaration uses 'sorry'sidon_set_lower_bound (N : ℕ) (hN : 1 ≤ N) : ∃ᵉ (A ⊆ Finset.Icc 1 N), IsSidon (A : Set ℕ) ∧ N.sqrt / 2 ≤ A.card := N:ℕhN:1 ≤ N⊢ ∃ A ⊆ Finset.Icc 1 N, IsSidon ↑A ∧ N.sqrt / 2 ≤ #A All goals completed! 🐙

The greedy construction gives a Sidon set of size approximately √N.

@[category textbook, AMS 5 11] theorem declaration uses 'sorry'greedy_sidon_construction (N : ℕ) (hN : 1 ≤ N) : ∃ᵉ (A ⊆ Finset.Icc 1 N), IsSidon (A : Set ℕ) ∧ A.card ≥ N.sqrt := N:ℕhN:1 ≤ N⊢ ∃ A ⊆ Finset.Icc 1 N, IsSidon ↑A ∧ #A ≥ N.sqrt All goals completed! 🐙 end Erdos44