FormalConjectures.Wikipedia.Taxicab

/-
Copyright 2026 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.
-/
module

public import FormalConjecturesUtil

Taxicab numbers

A taxicab number for natural numbers $k, m, n$ is the smallest number $x$ that can be expressed as a sum of $m$ positive $k$-th powers in at least $n$ distinct ways. The most famous taxicab number is $ 1729 = 1³ + 12³ = 9³ + 10³, $ also known as the Hardy–Ramanujan number.

However, a taxicab number is not known for $k=5$, $m=2$, and any $n ≥ 2$: No positive integer is known that can be written as the sum of two 5th powers in more than one way, and it is not known whether such a number exists.

In particular, it is not known whether there exists a taxicab number for $k=5$, $m=2$, and $n=2$.

References:

Wikipedia

Generalized taxicab number

OEIS taxicab cubes

OEIS taxicab 4th powers

OEIS taxicab conjecture

@[expose] public sectionnamespace Taxicab

$x$ is a candidate for being a taxicab number for $k, m, n$ if there exist at least $n$ distinct multisets of $m$ positive integers such that the sum of the $k$-th powers of the elements of each multiset is $x$. Using multisets means that two representations that differ only in the order of their terms count as one way.

def IsTaxicabFor' (k m n x : ℕ) : Prop :=
  ∃ S : Finset (Multiset ℕ), n ≤ S.card ∧
    ∀ L ∈ S, Multiset.card L = m ∧ 0 ∉ L ∧ (L.map (· ^ k)).sum = x

$1729$ is a possible taxicab number for $k=3, m=2, n=2$.

@[category test, AMS 11]
theorem taxicab_1729 : IsTaxicabFor' 3 2 2 1729 := by⊢ IsTaxicabFor' 3 2 2 1729
  use {{1, 12}, {9, 10}}h⊢ 2 ≤ {{1, 12}, {9, 10}}.card ∧ ∀ L ∈ {{1, 12}, {9, 10}}, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 3) L).sum = 1729
  decideAll goals completed! 🐙

$x$ is a taxicab number if it is the smallest number that can be expressed as a sum of $m$ positive $k$-th powers in at least $n$ distinct ways.

def IsTaxicabFor (k m n : ℕ) (x : ℕ) : Prop :=
  IsLeast { x : ℕ | IsTaxicabFor' k m n x } x

@[category test, AMS 11]
theorem taxicab_4' : IsTaxicabFor' 1 2 2 4 := by⊢ IsTaxicabFor' 1 2 2 4
  use {{1, 3}, {2, 2}}h⊢ 2 ≤ {{1, 3}, {2, 2}}.card ∧ ∀ L ∈ {{1, 3}, {2, 2}}, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = 4
  decideAll goals completed! 🐙

$4$ is the taxicab number for $k=1, m=2, n=2$.


@[category test, AMS 11]
theorem taxicab_4 : IsTaxicabFor 1 2 2 4 := by⊢ IsTaxicabFor 1 2 2 4
  constructorleft⊢ 4 ∈ {x | IsTaxicabFor' 1 2 2 x}right⊢ 4 ∈ lowerBounds {x | IsTaxicabFor' 1 2 2 x}
  ·left⊢ 4 ∈ {x | IsTaxicabFor' 1 2 2 x} exact taxicab_4'All goals completed! 🐙
  ·right⊢ 4 ∈ lowerBounds {x | IsTaxicabFor' 1 2 2 x} rintro x ⟨S, hS₁, hS₂⟩rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = x⊢ 4 ≤ x
    obtain ⟨s, hs, t, ht, hst⟩ := Finset.one_lt_card.mp hS₁rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xs:Multiset ℕhs:s ∈ St:Multiset ℕht:t ∈ Shst:s ≠ t⊢ 4 ≤ x
    obtain ⟨hs₁, hs₂, hs₃⟩ := hS₂ s hsrightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xs:Multiset ℕhs:s ∈ St:Multiset ℕht:t ∈ Shst:s ≠ ths₁:s.card = 2hs₂:0 ∉ shs₃:(Multiset.map (fun x ↦ x ^ 1) s).sum = x⊢ 4 ≤ x
    obtain ⟨ht₁, ht₂, ht₃⟩ := hS₂ t htrightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xs:Multiset ℕhs:s ∈ St:Multiset ℕht:t ∈ Shst:s ≠ ths₁:s.card = 2hs₂:0 ∉ shs₃:(Multiset.map (fun x ↦ x ^ 1) s).sum = xht₁:t.card = 2ht₂:0 ∉ tht₃:(Multiset.map (fun x ↦ x ^ 1) t).sum = x⊢ 4 ≤ x
    obtain ⟨a, b, rfl⟩ := Multiset.card_eq_two.mp hs₁rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xt:Multiset ℕht:t ∈ Sht₁:t.card = 2ht₂:0 ∉ tht₃:(Multiset.map (fun x ↦ x ^ 1) t).sum = xa:ℕb:ℕhs:{a, b} ∈ Shst:{a, b} ≠ ths₁:{a, b}.card = 2hs₂:0 ∉ {a, b}hs₃:(Multiset.map (fun x ↦ x ^ 1) {a, b}).sum = x⊢ 4 ≤ x
    obtain ⟨c, d, rfl⟩ := Multiset.card_eq_two.mp ht₁rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2hs₂:0 ∉ {a, b}hs₃:(Multiset.map (fun x ↦ x ^ 1) {a, b}).sum = xc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:0 ∉ {c, d}ht₃:(Multiset.map (fun x ↦ x ^ 1) {c, d}).sum = xhst:{a, b} ≠ {c, d}⊢ 4 ≤ x
    simp at hs₂ ht₂ hs₃ ht₃rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = x⊢ 4 ≤ x
    by_contra hrightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ x⊢ False
    have ha : a ≤ 2 := by⊢ IsTaxicabFor 1 2 2 4rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2⊢ False omegarightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2⊢ Falserightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2⊢ False
    have hb : b ≤ 2 := by⊢ IsTaxicabFor 1 2 2 4rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2⊢ False omegarightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2⊢ Falserightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2⊢ False
    have hc : c ≤ 2 := by⊢ IsTaxicabFor 1 2 2 4rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2hc:c ≤ 2⊢ False omegarightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2hc:c ≤ 2⊢ Falserightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2hc:c ≤ 2⊢ False
    have hd : d ≤ 2 := by⊢ IsTaxicabFor 1 2 2 4rightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2hc:c ≤ 2hd:d ≤ 2⊢ False omegarightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2hc:c ≤ 2hd:d ≤ 2⊢ Falserightx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕhs:{a, b} ∈ Shs₁:{a, b}.card = 2c:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2hst:{a, b} ≠ {c, d}hs₂:¬0 = a ∧ ¬0 = bht₂:¬0 = c ∧ ¬0 = dhs₃:a + b = xht₃:c + d = xh:¬4 ≤ xha:a ≤ 2hb:b ≤ 2hc:c ≤ 2hd:d ≤ 2⊢ False
    interval_cases aright.«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhb:b ≤ 2hc:c ≤ 2hd:d ≤ 2hs:{0, b} ∈ Shs₁:{0, b}.card = 2hst:{0, b} ≠ {c, d}hs₂:¬0 = 0 ∧ ¬0 = bhs₃:0 + b = xha:0 ≤ 2⊢ Falseright.«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhb:b ≤ 2hc:c ≤ 2hd:d ≤ 2hs:{1, b} ∈ Shs₁:{1, b}.card = 2hst:{1, b} ≠ {c, d}hs₂:¬0 = 1 ∧ ¬0 = bhs₃:1 + b = xha:1 ≤ 2⊢ Falseright.«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhb:b ≤ 2hc:c ≤ 2hd:d ≤ 2hs:{2, b} ∈ Shs₁:{2, b}.card = 2hst:{2, b} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = bhs₃:2 + b = xha:2 ≤ 2⊢ False <;>right.«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhb:b ≤ 2hc:c ≤ 2hd:d ≤ 2hs:{0, b} ∈ Shs₁:{0, b}.card = 2hst:{0, b} ≠ {c, d}hs₂:¬0 = 0 ∧ ¬0 = bhs₃:0 + b = xha:0 ≤ 2⊢ Falseright.«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhb:b ≤ 2hc:c ≤ 2hd:d ≤ 2hs:{1, b} ∈ Shs₁:{1, b}.card = 2hst:{1, b} ≠ {c, d}hs₂:¬0 = 1 ∧ ¬0 = bhs₃:1 + b = xha:1 ≤ 2⊢ Falseright.«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhb:b ≤ 2hc:c ≤ 2hd:d ≤ 2hs:{2, b} ∈ Shs₁:{2, b}.card = 2hst:{2, b} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = bhs₃:2 + b = xha:2 ≤ 2⊢ False interval_cases bright.«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hst:{2, 0} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = x⊢ Falseright.«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hst:{2, 1} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = x⊢ Falseright.«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hst:{2, 2} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = x⊢ False <;>right.«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hst:{0, 0} ≠ {c, d}hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = x⊢ Falseright.«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hst:{0, 1} ≠ {c, d}hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = x⊢ Falseright.«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hst:{0, 2} ≠ {c, d}hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = x⊢ Falseright.«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hst:{1, 0} ≠ {c, d}hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = x⊢ Falseright.«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hst:{1, 1} ≠ {c, d}hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = x⊢ Falseright.«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hst:{1, 2} ≠ {c, d}hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = x⊢ Falseright.«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hst:{2, 0} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = x⊢ Falseright.«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hst:{2, 1} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = x⊢ Falseright.«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕht:{c, d} ∈ Sht₁:{c, d}.card = 2ht₂:¬0 = c ∧ ¬0 = dht₃:c + d = xh:¬4 ≤ xhc:c ≤ 2hd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hst:{2, 2} ≠ {c, d}hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = x⊢ False interval_cases cright.«2».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{2, 2} ≠ {0, d}⊢ Falseright.«2».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{2, 2} ≠ {1, d}⊢ Falseright.«2».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{2, 2} ≠ {2, d}⊢ False <;>right.«0».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{0, 0} ≠ {0, d}⊢ Falseright.«0».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{0, 0} ≠ {1, d}⊢ Falseright.«0».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{0, 0} ≠ {2, d}⊢ Falseright.«0».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{0, 1} ≠ {0, d}⊢ Falseright.«0».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{0, 1} ≠ {1, d}⊢ Falseright.«0».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{0, 1} ≠ {2, d}⊢ Falseright.«0».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{0, 2} ≠ {0, d}⊢ Falseright.«0».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{0, 2} ≠ {1, d}⊢ Falseright.«0».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{0, 2} ≠ {2, d}⊢ Falseright.«1».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{1, 0} ≠ {0, d}⊢ Falseright.«1».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{1, 0} ≠ {1, d}⊢ Falseright.«1».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{1, 0} ≠ {2, d}⊢ Falseright.«1».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{1, 1} ≠ {0, d}⊢ Falseright.«1».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{1, 1} ≠ {1, d}⊢ Falseright.«1».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{1, 1} ≠ {2, d}⊢ Falseright.«1».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{1, 2} ≠ {0, d}⊢ Falseright.«1».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{1, 2} ≠ {1, d}⊢ Falseright.«1».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{1, 2} ≠ {2, d}⊢ Falseright.«2».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{2, 0} ≠ {0, d}⊢ Falseright.«2».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{2, 0} ≠ {1, d}⊢ Falseright.«2».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{2, 0} ≠ {2, d}⊢ Falseright.«2».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{2, 1} ≠ {0, d}⊢ Falseright.«2».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{2, 1} ≠ {1, d}⊢ Falseright.«2».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{2, 1} ≠ {2, d}⊢ Falseright.«2».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xht:{0, d} ∈ Sht₁:{0, d}.card = 2ht₂:¬0 = 0 ∧ ¬0 = dht₃:0 + d = xhc:0 ≤ 2hst:{2, 2} ≠ {0, d}⊢ Falseright.«2».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xht:{1, d} ∈ Sht₁:{1, d}.card = 2ht₂:¬0 = 1 ∧ ¬0 = dht₃:1 + d = xhc:1 ≤ 2hst:{2, 2} ≠ {1, d}⊢ Falseright.«2».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xhd:d ≤ 2ha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xht:{2, d} ∈ Sht₁:{2, d}.card = 2ht₂:¬0 = 2 ∧ ¬0 = dht₃:2 + d = xhc:2 ≤ 2hst:{2, 2} ≠ {2, d}⊢ False interval_cases dright.«2».«2».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{2, 2} ≠ {2, 0}⊢ Falseright.«2».«2».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{2, 2} ≠ {2, 1}⊢ Falseright.«2».«2».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{2, 2} ≠ {2, 2}⊢ False <;>right.«0».«0».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{0, 0} ≠ {0, 0}⊢ Falseright.«0».«0».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{0, 0} ≠ {0, 1}⊢ Falseright.«0».«0».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{0, 0} ≠ {0, 2}⊢ Falseright.«0».«0».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{0, 0} ≠ {1, 0}⊢ Falseright.«0».«0».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{0, 0} ≠ {1, 1}⊢ Falseright.«0».«0».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{0, 0} ≠ {1, 2}⊢ Falseright.«0».«0».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{0, 0} ≠ {2, 0}⊢ Falseright.«0».«0».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{0, 0} ≠ {2, 1}⊢ Falseright.«0».«0».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:0 ≤ 2hs:{0, 0} ∈ Shs₁:{0, 0}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 0hs₃:0 + 0 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{0, 0} ≠ {2, 2}⊢ Falseright.«0».«1».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{0, 1} ≠ {0, 0}⊢ Falseright.«0».«1».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{0, 1} ≠ {0, 1}⊢ Falseright.«0».«1».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{0, 1} ≠ {0, 2}⊢ Falseright.«0».«1».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{0, 1} ≠ {1, 0}⊢ Falseright.«0».«1».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{0, 1} ≠ {1, 1}⊢ Falseright.«0».«1».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{0, 1} ≠ {1, 2}⊢ Falseright.«0».«1».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{0, 1} ≠ {2, 0}⊢ Falseright.«0».«1».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{0, 1} ≠ {2, 1}⊢ Falseright.«0».«1».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:1 ≤ 2hs:{0, 1} ∈ Shs₁:{0, 1}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 1hs₃:0 + 1 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{0, 1} ≠ {2, 2}⊢ Falseright.«0».«2».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{0, 2} ≠ {0, 0}⊢ Falseright.«0».«2».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{0, 2} ≠ {0, 1}⊢ Falseright.«0».«2».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{0, 2} ≠ {0, 2}⊢ Falseright.«0».«2».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{0, 2} ≠ {1, 0}⊢ Falseright.«0».«2».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{0, 2} ≠ {1, 1}⊢ Falseright.«0».«2».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{0, 2} ≠ {1, 2}⊢ Falseright.«0».«2».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{0, 2} ≠ {2, 0}⊢ Falseright.«0».«2».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{0, 2} ≠ {2, 1}⊢ Falseright.«0».«2».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:0 ≤ 2hb:2 ≤ 2hs:{0, 2} ∈ Shs₁:{0, 2}.card = 2hs₂:¬0 = 0 ∧ ¬0 = 2hs₃:0 + 2 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{0, 2} ≠ {2, 2}⊢ Falseright.«1».«0».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{1, 0} ≠ {0, 0}⊢ Falseright.«1».«0».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{1, 0} ≠ {0, 1}⊢ Falseright.«1».«0».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{1, 0} ≠ {0, 2}⊢ Falseright.«1».«0».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{1, 0} ≠ {1, 0}⊢ Falseright.«1».«0».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{1, 0} ≠ {1, 1}⊢ Falseright.«1».«0».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{1, 0} ≠ {1, 2}⊢ Falseright.«1».«0».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{1, 0} ≠ {2, 0}⊢ Falseright.«1».«0».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{1, 0} ≠ {2, 1}⊢ Falseright.«1».«0».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:0 ≤ 2hs:{1, 0} ∈ Shs₁:{1, 0}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 0hs₃:1 + 0 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{1, 0} ≠ {2, 2}⊢ Falseright.«1».«1».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{1, 1} ≠ {0, 0}⊢ Falseright.«1».«1».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{1, 1} ≠ {0, 1}⊢ Falseright.«1».«1».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{1, 1} ≠ {0, 2}⊢ Falseright.«1».«1».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{1, 1} ≠ {1, 0}⊢ Falseright.«1».«1».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{1, 1} ≠ {1, 1}⊢ Falseright.«1».«1».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{1, 1} ≠ {1, 2}⊢ Falseright.«1».«1».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{1, 1} ≠ {2, 0}⊢ Falseright.«1».«1».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{1, 1} ≠ {2, 1}⊢ Falseright.«1».«1».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:1 ≤ 2hs:{1, 1} ∈ Shs₁:{1, 1}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 1hs₃:1 + 1 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{1, 1} ≠ {2, 2}⊢ Falseright.«1».«2».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{1, 2} ≠ {0, 0}⊢ Falseright.«1».«2».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{1, 2} ≠ {0, 1}⊢ Falseright.«1».«2».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{1, 2} ≠ {0, 2}⊢ Falseright.«1».«2».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{1, 2} ≠ {1, 0}⊢ Falseright.«1».«2».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{1, 2} ≠ {1, 1}⊢ Falseright.«1».«2».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{1, 2} ≠ {1, 2}⊢ Falseright.«1».«2».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{1, 2} ≠ {2, 0}⊢ Falseright.«1».«2».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{1, 2} ≠ {2, 1}⊢ Falseright.«1».«2».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:1 ≤ 2hb:2 ≤ 2hs:{1, 2} ∈ Shs₁:{1, 2}.card = 2hs₂:¬0 = 1 ∧ ¬0 = 2hs₃:1 + 2 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{1, 2} ≠ {2, 2}⊢ Falseright.«2».«0».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{2, 0} ≠ {0, 0}⊢ Falseright.«2».«0».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{2, 0} ≠ {0, 1}⊢ Falseright.«2».«0».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{2, 0} ≠ {0, 2}⊢ Falseright.«2».«0».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{2, 0} ≠ {1, 0}⊢ Falseright.«2».«0».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{2, 0} ≠ {1, 1}⊢ Falseright.«2».«0».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{2, 0} ≠ {1, 2}⊢ Falseright.«2».«0».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{2, 0} ≠ {2, 0}⊢ Falseright.«2».«0».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{2, 0} ≠ {2, 1}⊢ Falseright.«2».«0».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:0 ≤ 2hs:{2, 0} ∈ Shs₁:{2, 0}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 0hs₃:2 + 0 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{2, 0} ≠ {2, 2}⊢ Falseright.«2».«1».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{2, 1} ≠ {0, 0}⊢ Falseright.«2».«1».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{2, 1} ≠ {0, 1}⊢ Falseright.«2».«1».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{2, 1} ≠ {0, 2}⊢ Falseright.«2».«1».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{2, 1} ≠ {1, 0}⊢ Falseright.«2».«1».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{2, 1} ≠ {1, 1}⊢ Falseright.«2».«1».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{2, 1} ≠ {1, 2}⊢ Falseright.«2».«1».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{2, 1} ≠ {2, 0}⊢ Falseright.«2».«1».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{2, 1} ≠ {2, 1}⊢ Falseright.«2».«1».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{2, 1} ≠ {2, 2}⊢ Falseright.«2».«2».«0».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:0 ≤ 2hd:0 ≤ 2ht:{0, 0} ∈ Sht₁:{0, 0}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 0ht₃:0 + 0 = xhst:{2, 2} ≠ {0, 0}⊢ Falseright.«2».«2».«0».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:0 ≤ 2hd:1 ≤ 2ht:{0, 1} ∈ Sht₁:{0, 1}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 1ht₃:0 + 1 = xhst:{2, 2} ≠ {0, 1}⊢ Falseright.«2».«2».«0».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:0 ≤ 2hd:2 ≤ 2ht:{0, 2} ∈ Sht₁:{0, 2}.card = 2ht₂:¬0 = 0 ∧ ¬0 = 2ht₃:0 + 2 = xhst:{2, 2} ≠ {0, 2}⊢ Falseright.«2».«2».«1».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:1 ≤ 2hd:0 ≤ 2ht:{1, 0} ∈ Sht₁:{1, 0}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 0ht₃:1 + 0 = xhst:{2, 2} ≠ {1, 0}⊢ Falseright.«2».«2».«1».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:1 ≤ 2hd:1 ≤ 2ht:{1, 1} ∈ Sht₁:{1, 1}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 1ht₃:1 + 1 = xhst:{2, 2} ≠ {1, 1}⊢ Falseright.«2».«2».«1».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:1 ≤ 2hd:2 ≤ 2ht:{1, 2} ∈ Sht₁:{1, 2}.card = 2ht₂:¬0 = 1 ∧ ¬0 = 2ht₃:1 + 2 = xhst:{2, 2} ≠ {1, 2}⊢ Falseright.«2».«2».«2».«0»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:2 ≤ 2hd:0 ≤ 2ht:{2, 0} ∈ Sht₁:{2, 0}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 0ht₃:2 + 0 = xhst:{2, 2} ≠ {2, 0}⊢ Falseright.«2».«2».«2».«1»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{2, 2} ≠ {2, 1}⊢ Falseright.«2».«2».«2».«2»x:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:2 ≤ 2hs:{2, 2} ∈ Shs₁:{2, 2}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 2hs₃:2 + 2 = xhc:2 ≤ 2hd:2 ≤ 2ht:{2, 2} ∈ Sht₁:{2, 2}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 2ht₃:2 + 2 = xhst:{2, 2} ≠ {2, 2}⊢ False
      first | omegaAll goals completed! 🐙 | exact hst (byx:ℕS:Finset (Multiset ℕ)hS₁:2 ≤ S.cardhS₂:∀ L ∈ S, L.card = 2 ∧ 0 ∉ L ∧ (Multiset.map (fun x ↦ x ^ 1) L).sum = xa:ℕb:ℕc:ℕd:ℕh:¬4 ≤ xha:2 ≤ 2hb:1 ≤ 2hs:{2, 1} ∈ Shs₁:{2, 1}.card = 2hs₂:¬0 = 2 ∧ ¬0 = 1hs₃:2 + 1 = xhc:2 ≤ 2hd:1 ≤ 2ht:{2, 1} ∈ Sht₁:{2, 1}.card = 2ht₂:¬0 = 2 ∧ ¬0 = 1ht₃:2 + 1 = xhst:{2, 1} ≠ {2, 1}⊢ {2, 1} = {2, 1} decideAll goals completed! 🐙)

Taxicab number for $k=5$, $m=2$, and $n=2$ is not known. Whether such a number exists is also not known.

@[category research open, AMS 11]
theorem taxicab_for_5_2_2 : answer(sorry) ↔ ∃ x : ℕ, IsTaxicabFor 5 2 2 x := by⊢ True ↔ ∃ x, IsTaxicabFor 5 2 2 x
  sorryAll goals completed! 🐙

Taxicab number for $k=5$ and $m=2$ is not-known for any $n ≥ 2$. Whether such a number exists is also not known.

@[category research open, AMS 11]
theorem taxicab_for_5_2_n : answer(sorry) ↔ ∃ n : ℕ, n ≥ 2 ∧ (∃ x : ℕ, IsTaxicabFor 5 2 n x)
  := by⊢ True ↔ ∃ n ≥ 2, ∃ x, IsTaxicabFor 5 2 n x sorryAll goals completed! 🐙

end Taxicab