Skip to content

Instantly share code, notes, and snippets.

@semorrison

semorrison/gist:2ab6ff0c68a69cc657752ef16145b031

Created August 24, 2019 06:58
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save semorrison/2ab6ff0c68a69cc657752ef16145b031 to your computer and use it in GitHub Desktop.
Save semorrison/2ab6ff0c68a69cc657752ef16145b031 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
decidable.rec
(λ
(hp :
¬∀ (i : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
(λ (m : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_)
i <
mk punit pempty (λ (_x : punit), 0) pempty.elim), is_false _)
(λ
(hp :
∀ (i : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
(λ (m : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_)
i <
mk punit pempty (λ (_x : punit), 0) pempty.elim),
dite
(∀ (j : pempty),
mk (left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]))
(right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]))
(λ (m : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_)
(λ (m : right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_) <
pempty.elim j)
(λ
(hq :
∀ (j : pempty),
mk (left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]))
(right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]))
(λ (m : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_)
(λ (m : right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_) <
pempty.elim j), is_true _)
(λ
(hq :
¬∀ (j : pempty),
mk (left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]))
(right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]))
(λ (m : left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_left (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_)
(λ (m : right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
have this :
finset.card (move_right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m) <
finset.card (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]), from
_,
(λ (y : finset (ℤ × ℤ))
(a :
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y
(list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)])),
acc.rec
(λ (x₁ : finset (ℤ × ℤ))
(ac₁ :
∀ (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
acc (λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y)
(ih :
Π (y : finset (ℤ × ℤ)),
(λ (y x : finset (ℤ × ℤ)), has_well_founded.r y x) y x₁ →
(λ (_x : finset (ℤ × ℤ)), pgame) y),
(λ (_x : finset (ℤ × ℤ)),
id_rhs ((Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame) → pgame)
(λ (_F : Π (_y : finset (ℤ × ℤ)), has_well_founded.r _y _x → pgame),
mk (left _x) (right _x)
(λ (m : left _x),
have this : finset.card (move_left _x m) < finset.card _x, from _,
_F (move_left _x m) _)
(λ (m : right _x),
have this : finset.card (move_right _x m) < finset.card _x, from _,
_F (move_right _x m) _)))
x₁
ih)
_)
(move_right (list.to_finset [(0, 2), (0, 1), (0, 0), (1, 0)]) m)
_) <
pempty.elim j), is_false _))
fintype.decidable_forall_fintype
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment