/-
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 FormalConjecturesUtilErdős Problem 44: Extending Sidon Sets
Reference: erdosproblems.com/44
open Function Set Finsetnamespace Erdos44
The maximum size of a Sidon set in {1, ..., N} is less than or equal to 2 * √N.
N:ℕhN:1 ≤ Nkey:(Finset.Icc 1 N).maxSidonSubsetCard ^ 2 ≤ 4 * Nh1:↑(Finset.Icc 1 N).maxSidonSubsetCard ^ 2 ≤ 4 * ↑Nh2:2 * √↑N = √(4 * ↑N)⊢ √(↑(Finset.Icc 1 N).maxSidonSubsetCard ^ 2) ≤ √(4 * ↑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 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 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}
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 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 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