Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/before_first_simp.lean

Created July 13, 2018 07:07
Show Gist options
  • Save kbuzzard/d9f70ae02b5861bbce0f8d958e16619a to your computer and use it in GitHub Desktop.
Save kbuzzard/d9f70ae02b5861bbce0f8d958e16619a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
before_first_simp.lean
c : ℕ,
h : c ≥ 3
⊢ N_min
(pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 -
↑((λ (t : multiset ℕ) (h : t < c :: 0),
strong_induction_on t
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap
(λ (a : ℕ) (h : a ∈ C2),
a - 2 + int.nat_abs (2 - ↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap
(λ (a : ℕ) (h : a ∈ L2),
a - 4 + int.nat_abs (4 - ↑(HL (erase L2 a) _)))
L2
_))))
(erase (c :: 0) a)
_
0)))
(c :: 0)
_ +
pmap
(λ (a : ℕ) (h : a ∈ 0),
a - 4 +
int.nat_abs
(4 -
↑((λ (t : multiset ℕ) (h : t < 0),
strong_induction_on t
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 -
↑((λ (t : multiset ℕ) (h : t < c :: 0),
strong_induction_on t
(λ (C2 : multiset ℕ)
(HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ)
(HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap
(λ (a : ℕ) (h : a ∈ C2),
a - 2 +
int.nat_abs
(2 - ↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap
(λ (a : ℕ) (h : a ∈ L2),
a - 4 +
int.nat_abs (4 - ↑(HL (erase L2 a) _)))
L2
_))))
(erase (c :: 0) a)
_
L2)))
(c :: 0)
_ +
pmap
(λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 - ↑(HL (erase L2 a) _)))
L2
_)))
(erase 0 a)
_)))
0
_) =
c
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment