basics

Stream: new members

[Iocta]

Why does this fail, and how to fix it?

def show_p : (p ∧ q) ∨ (p ∧ r) → p :=
  (assume h: (p ∧ q) ∨ (p ∧ r),
  show p,
  from or.elim h
  and.left
  and.left
)

def show_q_or_r : (p ∧ q) ∨ (p ∧ r) → q ∨ r :=
(assume h: (p ∧ q) ∨ (p ∧ r),
  show q ∨ r,
  from or.elim h
  (λ z, or.inl  (and.right z))
  (λ z, or.inr (and.right z))
)

example : (p ∧ q) ∨ (p ∧ r) → p ∧ (q ∨ r) :=
(assume h: (p ∧ q) ∨ (p ∧ r) ,
show p ∧ (q ∨ r),
from and.intro ((show_p h ) ∧ (show_q_or_r h))
)

[Kenny Lau]

the last line should be:

from and.intro (show_p h) (show_q_or_r h)

[Kenny Lau]

and.intro : ∀ {a b : Prop}, a → b → a ∧ b

[Kenny Lau]

and.intro is a function that takes a proof of a and a proof of b and gives a proof of a ∧ b

[Kenny Lau]

show_p h is the first input

[Kenny Lau]

show_q_or_r h is the second input

[Iocta]

Thanks

[Iocta]

Hm it's not quite that? Doesn't compile.

def show_p : (p ∧ q) ∨ (p ∧ r) → p :=
  (assume h: (p ∧ q) ∨ (p ∧ r),
  show p,
  from or.elim h
  and.left
  and.left
)

def show_q_or_r : (p ∧ q) ∨ (p ∧ r) → q ∨ r :=
(assume h: (p ∧ q) ∨ (p ∧ r),
  show q ∨ r,
  from or.elim h
  (λ z, or.inl  (and.right z))
  (λ z, or.inr (and.right z))
)

example : (p ∧ q) ∨ (p ∧ r) → p ∧ (q ∨ r) :=
(assume h: (p ∧ q) ∨ (p ∧ r) ,
show p ∧ (q ∨ r),
from and.intro (show_p h )  (show_q_or_r h)
)

[Patrick Massot]

How do you declare your variables p, q and r?

[Patrick Massot]

You seem to use them implicitly, hence they should appear between curly brackets.

[Iocta]

I have variables p q r : Prop at the top of the page.

[Patrick Massot]

This defaults to regular parentheses, hence explicit arguments.

[Patrick Massot]

Switch to variables {p q r : Prop}.

[Iocta]

That works. How should my code be if I wanted to keep the variables p q r : Prop?

[Bryan Gin-ge Chen]

You have to provide all explicit parameters to the function show_p, so your last example should look like this:

example : (p ∧ q) ∨ (p ∧ r) → p ∧ (q ∨ r) :=
(assume h: (p ∧ q) ∨ (p ∧ r) ,
show p ∧ (q ∨ r),
from and.intro (show_p p q r h )  (show_q_or_r p q r h)
)

[Iocta]

Oh I see. Thank you all.

[Patrick Massot]

That kind of verbosity is precisely what implicit arguments are meant to deal with.

[Patrick Massot]

(of course you're free to use them or not, I only want to make sure you understand the point).

[Iocta]

Yep, got it.

[Iocta]

Is there a built-in function \lambda h, h?

[Aria Miuk]

That should be id.

[Iocta]

Thanks

[Iocta]

Is it possible to do this without classical? example : ¬(p ↔ ¬p) := sorry

[Simon Hudon]

Yes. Do you want to prove it yourself?

[Aria Miuk]

Yes it is provable. Think about how to get p into context and the definition of not.

[Iocta]

No luck. How do I get p into context?

[Bryan Gin-ge Chen]

Have you been able to get ¬p into the goal? Remember that this is actually p → false.

[Aria Miuk]

Strat with intros contra (or \lambda contra, _) and see how one magically conjures hypotheses :).

[Iocta]

I'm missing something. I can't find anything shaped like p or p \to false.

[Aria Miuk]

You're on the right path. You're looking for something p \to false. Can you prove it?

[Iocta]

No I'm back where I started :-)

[Aria Miuk]

Look at your contradictory hypothesis, (p ↔ ¬p). You "win" once you either know p, or not p. Agreed? (As this then leads to contradiction.)

[Aria Miuk]

So then surely the only way to prove this is to either know p or not p. There is bound to be no other way.

[Aria Miuk]

So choose one, whichever you prefer. And formulate: have h : p, { ... }. (Or the other one.)

[Aria Miuk]

Can you prove either of these? What happens if you attempt?

[Iocta]

I want to do something like or.elim hp, but I can't figure out how to make hp.

example : ¬(p ↔ ¬p) :=
λ c,
have hp: p, from _,
show false, from _

[Iocta]

If hp then hnp, and absurd hp hnp. And vice versa. But how do I state either of those hypotheses?

[Aria Miuk]

So you need to prove p. Surely your only hypothesis is c. Let's use it. c.2 gives us not p -> p, we apply it to get the conclusion not p. So far so good?

[Bryan Gin-ge Chen]

Here's another transcript of my thoughts as I work through the start of this one "automatically" (in the style of this previous post).

We start out with a single underscore and let Lean tell us what's missing:

-- (1)
example (p : Prop) : ¬(p ↔ ¬p) :=
_
/- p : Prop
⊢ ¬(p ↔ ¬p) -/

Here and below, I'll just quote the part of the error message(s) that shows the hypotheses in the context and the goal. Since ¬(p ↔ ¬p) is the same as (p ↔ ¬p) → false, which is a function type, we should be able to make progress by introducing a lambda:

-- (2a)
example (p : Prop) : ¬(p ↔ ¬p) :=
λ h, _
/- p : Prop,
h : p ↔ ¬p
⊢ false -/

Note that p ↔ ¬p is the same as (p → ¬p) ∧ (¬p → p) so we could proceed by using h.1 and h.2. However, I'll redo this step by making use of Lean's pattern-matching syntax to split h into two hypotheses:

-- (2b)
example (p : Prop) : ¬(p ↔ ¬p) :=
λ ⟨h1, h2⟩, _
/- p : Prop,
_x : p ↔ ¬p,
_fun_match : (p ↔ ¬p) → false,
h1 : p → ¬p,
h2 : ¬p → p
⊢ false -/

Aside from h1 and h2 there's some other junk in the context related to the pattern-matching; I won't show it again below. Now, how do we make progress towards the goal of false? Now we realize that h1 : p → ¬p is short for h1 : p → p → false. Since passing two parameters to h1 will yield false, we should try replacing the underscore with h1 _ _:

-- (3)
example (p : Prop) : ¬(p ↔ ¬p) :=
λ ⟨h1, h2⟩, h1 _ _
/- h1 : p → ¬p,
h2 : ¬p → p
⊢ p -/
/- h1 : p → ¬p,
h2 : ¬p → p
⊢ p -/

There are now two error messages because there are two underscores. Since I'm only intending to show a few more steps, from here on out I'm only going to show the error message corresponding to the first underscore. How do we make progress towards p there? Well, note that h2 : ¬p → p is a function which takes one parameter and returns p, so let's replace the underscore with h2 _:

-- (4)
example (p : Prop) : ¬(p ↔ ¬p) :=
λ ⟨h1, h2⟩, h1 (h2 _) _
/- h1 : p → ¬p,
h2 : ¬p → p
⊢ ¬p -/

Hey, here's the goal of ¬p we hinted at! Now what? Well, naïvely, we might apply h1 again, since it ends in ¬p. However, if you try this, you'll see that continuing this way won't work (try it, what happens?). What should we do instead? Well, if we instead observe that ¬p is the same as p → false, we can alternatively introduce another lambda here:

-- (5)
example (p : Prop) : ¬(p ↔ ¬p) :=
λ ⟨h1, h2⟩, h1 (h2 (λ h3, _)) _
/- h1 : p → ¬p,
h2 : ¬p → p,
h3 : p
⊢ false -/

Now we have p in the context, as desired! I'll leave the rest to you, but one final hint. Our goal is false again. Last time we saw this (step (3)), we replaced the underscore with h1 _ _. You should try doing this again. You'll end up in a state with 3 underscores / errors, but there's now something in the context which will let you close two of them right away...

You can fill in the last underscore very similarly.

When you get to the end, you'll notice that in blindly "chasing underscores" we end up with quite a bit of duplication. We could have avoided this by naming some terms with have statements, and it's worth refactoring the proof along those lines. Then you might start again from scratch and try to write a version of the proof with the have statements from the beginning.

[Iocta]

I'll meditate on this. Thanks.

[Iocta]

The basic version looks like

example (p : Prop) : ¬(p ↔ ¬p) :=
λ (|h1, h2|),
(h1
  (h2 (λ hp, absurd hp (h1 hp)))
  (h2 (λ hp, absurd hp (h1 hp)))
)

Is this less redundant, or is it the same thing?

example (p : Prop) : ¬(p ↔ ¬p) :=
λ (|h1, h2|),
have hnp : ¬p, from (λ hp', absurd hp' (h1 hp')),
have hp: p, from (h2 hnp),
show false, from (absurd hp hnp)

[Bryan Gin-ge Chen]

Well, absurd itself is short for a certain proof term... do you know how absurd is proved?

[Kenny Lau]

@Iocta maybe try this more general theorem:

theorem Curry's_paradox (p q : Prop) : (p ↔ (p → q)) → q :=
_

[Iocta]

example (p : Prop) : ¬(p ↔ ¬p) :=
λ (|h1, h2|),
have hnp : ¬p, from (λ hp', (h1 hp')  hp'),
have hp: p, from (h2 hnp),
show false, from hnp hp

[Iocta]

theorem Curry's_paradox (p q : Prop) : (p ↔ (p → q)) → q :=
λ (|h1, h2|),
have hp : p, from (h2 (λ hp', h1 hp' hp')),
show q, from (h1 hp hp)

[Kevin Buzzard]

import tactic

theorem Curry's_paradox (p q : Prop) : (p ↔ (p → q)) → q := by tauto!

[Iocta]

Why's this wrong? How to fix it?

open classical

lemma unnotnot : ¬¬p → p :=
λ hnnp, or.elim (em p) id (λ hnp, false.elim (absurd hnp hnnp))


example : ¬(p ∧ q) → ¬p ∨ ¬q :=
λ h, or.elim (em p)
(λ hp,
have hnq : ¬q, from (by_contradiction (λ hnnq, h (and.intro hp (unnotnot hnnq)))),
  show _, from or.inr
)
or.inl

[Kenny Lau]

or.inr should be or.inr hnq:

open classical

variables {p q : Prop}

lemma unnotnot : ¬¬p → p :=
λ hnnp, or.elim (em p) id (λ hnp, false.elim (absurd hnp hnnp))


example : ¬(p ∧ q) → ¬p ∨ ¬q :=
λ h, or.elim (em p)
(λ hp,
have hnq : ¬q, from (by_contradiction (λ hnnq, h (and.intro hp (unnotnot hnnq)))),
  show _, from or.inr hnq
)
or.inl

[Kenny Lau]

the type of or.inr is unified with ¬q → ¬p ∨ ¬q

[Iocta]

Thanks

[Iocta]

Is it possible to prove unnotnot without classical?

[Kenny Lau]

no

[Kenny Lau]

it's equivalent to em

[Iocta]

When I have \not p in context and p in goal, is there something I should be saying to myself?

[Kenny Lau]

if you can prove the goal, then you can prove false; so maybe aim to prove false instead

[Iocta]

Alright

[Iocta]

Can I fill this underscore, or am I down the wrong path?

example : ¬(p → q) → p ∧ ¬q :=
λ h,
have notq : ¬q, from (λ hq', (h (λ hp, hq'))),
and.intro
(or.elim (em p) id (λ hnp, _))
notq

[Chris Hughes]

You can fill in the underscore

[Iocta]

ok

[Iocta]

Is it possible to get into situations where I wouldn't be able to fill in the underscore, but where the overall claim is true?

[Kenny Lau]

example : true :=
false.elim _

[Bryan Gin-ge Chen]

There was another example at the very end of this reply to one of your questions (step 2R).

[Iocta]

how do I find conversations I've been involved in on zulip?

[Kevin Buzzard]

search for yourself using the search bar at the top.

[Iocta]

ah I see

[Iocta]

This example works but it's quite long. Did I miss some opportunity to simplify?

variables p q : Prop

theorem contrap : (p → q) → (¬q → ¬p) :=
λ h hnq hp, hnq (h hp)


open classical

lemma unnotnot : ¬¬p → p :=
λ hnnp, or.elim (em p) id (λ hnp, false.elim (absurd hnp hnnp))

lemma notnot : p → ¬¬p :=
λ hp hnp, hnp hp

theorem ncontrap : ( ¬p → ¬q) → (q → p) :=
λ np2nq hq,
or.elim (em p)
id
(λ hnp,  (absurd (np2nq hnp)   (notnot _ hq)))


lemma contrapositive_not : ¬(p → q) → ¬(¬q → ¬p) :=
λh h',
or.elim (em q)
(λ hq,
  have nnp2nnq : _, from (contrap _ _ h'),
  have p2q : p → q, from
  (λ hp,
    have hq: _,
    from unnotnot _ (nnp2nnq (notnot _ hp)), hq),
  absurd p2q h)
(λ hnq,
  have hnp: ¬p, from h' hnq,
  have p2q: p → q, from ncontrap _ _ h',
  have false' : _, from h p2q,
  false')


example : ¬(p → q) → p ∧ ¬q :=
λ h,
have hnq : ¬q, from (λ hq', (h (λ hp, hq'))),
and.intro
(or.elim (em p) id (λ hnp,
have h' : _, from contrapositive_not _ _ h,
(false.elim (h' (λ hnq', hnp)))))
hnq

[Reid Barton]

This looks a lot more complicated than necessary. In particular, you shouldn't need to use em again to fill in the underscore.
In the context of the underscore, you know not p and also not (p -> q). But not p is p -> false, and from false you can prove q, so you get p -> q, which contradicts not (p -> q).

[Iocta]

Thanks.

[Kevin Buzzard]

Of course you can also prove all of these basic logic statements with one line using tactics, and most if not all of them will already be proved in lean or mathlib already. If you're interested in seeing very short proofs you can read the proofs in the library

[Iocta]

I'm still working through the tutorial, haven't got to tactics yet.

[Iocta]

I'm confused about the forall syntax. How do you fill this? def prime (n : ℕ) : Prop := sorry

[Iocta]

def nondivisible (n : ℕ) : Prop :=
  forall m : ℕ, (and.intro (m > 1) (m < n) ) → not (divides m n)

nope

[Kenny Lau]

and.intro (hp : p) (hq : q) is a proof of p and q

[Iocta]

How do I take an m : \N such that 1 < m < nas an argument?

[Iocta]

I guess I could say or.elim (em 1 < m) but that seems roundabout

[Mario Carneiro]

You just write

  forall m : ℕ, 1 < m < n → not (divides m n)

[Mario Carneiro]

except that doesn't actually work, but this does:

  forall m : ℕ, (and (m > 1) (m < n) ) → not (divides m n)

[Mario Carneiro]

or

  forall m : ℕ, m > 1 → m < n → not (divides m n)

[Iocta]

Oh, easy. Thanks.

[Iocta]

def prime (n : ℕ) : Prop :=
forall m : ℕ, and (m > 1) (m < n) → not (divides m n)

variable m: ℕ

example : Prop :=
forall n : ℕ, (n > 2) → ∃ k : ℕ,  (and (eq (k + m) n) (and (prime k) (prime m)))

What's the quantifier on m?

[Iocta]

compared to forall n : ℕ, (n > 2) → ∃ k : ℕ, ∃m : ℕ, (and (eq (k + m) n) (and (prime k) (prime m)))

[Iocta]

(m in the example)

[Iocta]

Oh I see, we're taking it as an argument.

[Iocta]

Why doesn't it complain that it doesn't match Prop then?

[Mario Carneiro]

When you refer to a variable, it automatically adds the variable binder to the definition, as if you had written

example (m : ℕ) : Prop :=
forall n : ℕ, (n > 2) → ∃ k : ℕ,  (and (eq (k + m) n) (and (prime k) (prime m)))

[Iocta]

Aha

[Iocta]

Given

def divides (m n : ℕ) : Prop := ∃ k, m * k = n

How do I check whether divides 3 6?

[Iocta]

#check/#eval/#print don't seem to do it

[Mario Carneiro]

You need to prove the predicate is decidable first, which amounts to giving a decision procedure. In most programming languages, for example, you decide m | n by testing if m % n = 0

[Mario Carneiro]

Luckily, we've already gone to the trouble to do this, but you have to use the built-in divides relation to get this

[Alex J. Best]

Once you have a decidable proposition #eval to_bool (divides 3 6) will display either tt or ff

[Mario Carneiro]

Note that by the syntactic form of the expression (an exists over natural numbers of a basic proposition) it is not obviously decidable. For example Goldbach's conjecture can also be written in this form but it's an open question if this is a decidable proposition

[Kevin Buzzard]

With inbuilt divides, it just works: #eval to_bool (3 ∣ 6) -- tt. Note that this is \| not |.

[Kevin Buzzard]

example (a b : ℕ) : decidable (a ∣ b) := by apply_instance -- already inbuilt

[Kevin Buzzard]

def prime (n : ℕ) : Prop :=
forall m : ℕ, and (m > 1) (m < n) → not (divides m n)

There is notation which makes this more readable for mathematicians, right?

def prime (n : ℕ) : Prop :=
∀ m : ℕ, m > 1 ∧ m < n → ¬ (divides m n)

But Mario's suggestion of currying it and writing m > 1 → m < n → ¬ (divides m n) is better for functional languages because it's easier to work with; typically m>1 comes from one proof and m<n comes from another, and if you curry it then you don't need to apply the and.intro

[Cerek Hillen (he) (W2'20)]

sorry if this is out of place (new to lean and to the community :happy:) but i've been searching all over the docs and can't find an answer. i'm trying to rewrite with rw mem_empty_eq, and receiving the following error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 ∈ ∅
state:
α : Type,
A : set α
⊢ {a : α | a ∈ A ∧ a ∈ ∅} = ∅

[Kevin Buzzard]

ouch

[Cerek Hillen (he) (W2'20)]

i would think that a ∈ ∅ is sufficient to rewrite?

[Kevin Buzzard]

It's hidden too deep in the term.

[Kevin Buzzard]

try ext first

[Kevin Buzzard]

You can't rewrite under a lambda.

[Cerek Hillen (he) (W2'20)]

ah! that makes sense. is that just to protect against accidentally rewriting already-bound terms?

[Kevin Buzzard]

Alternatively you could try simp only [mem_empty_eq]

[Kevin Buzzard]

I have no idea why it makes sense, I am a mathematician. I just know the workarounds.

[Cerek Hillen (he) (W2'20)]

I am a mathematician

Hahaha, well thank you all the same :happy:

[Kevin Buzzard]

mem_empty_eq is definitionally true, so you could just write show {a : α | a ∈ A ∧ false} = ∅

[Kevin Buzzard]

but then you probably won't be able to rewrite and_false on the next line, you'll perhaps have to do ext in the end if you want to prove this by hand. Did you try simp?

[Cerek Hillen (he) (W2'20)]

yeah, simp goes through the entire proof for me. i'm trying to get a better handle on lean by doing some introductory exercises on an undergrad abstract algebra textbook i found

[Cerek Hillen (he) (W2'20)]

i got it to work with simp only [...] for both the mem_empty_eq and and_false steps. i'm going to try with ext to get more experience with that too

[Kevin Buzzard]

After ext the rewrites do work.

[Cerek Hillen (he) (W2'20)]

yep, although only on the rhs of the iff, i can show that forall a. a \not \in ... with a iff_false, and then i can map that to the set being \emptyset maybe?

[Cerek Hillen (he) (W2'20)]

thank you for your help :)

[Cerek Hillen (he) (W2'20)]

after many hours of syntax errors, i'm proud to say i've shown... A ∩ ∅ = ∅ :face_palm:

lemma intersection_empty (α : Type) (A : set α) :
        A ∩ ∅ = ∅ :=
        begin
            rw inter_def,
            ext a,
            rw mem_set_of_eq,
            repeat {rw mem_empty_eq},
            rw and_false,
        end

[Cerek Hillen (he) (W2'20)]

thanks again Kevin!

[Daniel Keys]

@Cerek Hillen (he) (W2'20) Hey Cerek, that doesn't work for me, do you need to include or open some stuff?

[Cerek Hillen (he) (W2'20)]

yeah! i have the following at the top of my .lean file:

import data.set.basic
import data.nat.basic
import logic.basic

open set
open nat

[Iocta]

example : (∃x :α, p x) → α :=
λ h, exists.elim h, _

How to write this?

[Bryan Gin-ge Chen]

@Iocta The answer depends on the type of α:

import logic.basic

variables (α : Prop)

example (p : α → Prop) : (∃x :α, p x) → α :=
λ h, exists.elim h (λ x h', x)

variables (β : Type*)

noncomputable example (p : β → Prop) : (∃x :β, p x) → β :=
λ h, exists.classical_rec_on h (λ x h', x)

[Bryan Gin-ge Chen]

@Cerek Hillen (he) (W2'20) Maybe you already know this, but just to be sure, your intersection_empty is also known as set.inter_empty in mathlib. You can find this out if you import tactic and then use library_search:

lemma intersection_empty (α : Type) (A : set α) :
        A ∩ ∅ = ∅ := by library_search

[Cerek Hillen (he) (W2'20)]

Cerek Hillen (he) (W2'20) Maybe you already know this, but just to be sure, your intersection_empty is also known as set.inter_empty in mathlib. You can find this out if you import tactic and then use library_search:

lemma intersection_empty (α : Type) (A : set α) :
        A ∩ ∅ = ∅ := by library_search

I was aware, but thank you! I'm looking to get a better handle on Lean by going through proofs manually

[Patrick Massot]

@Cerek Hillen (he) (W2'20) your proof works but it breaks many abstraction barriers. You know too much about how sets are implemented, and know too many lemmas about them. Maybe try:

example (α : Type) (A : set α) : A ∩ ∅ = ∅ :=
begin
  ext a,
  split,
  { rintro ⟨ha, ha'⟩,
    assumption },
  { intro h,
    exfalso,
    assumption },
end

[Patrick Massot]

Another useful exercise from the opposite of the style spectrum is to understand the following proof term:

example (α : Type) (A : set α) : A ∩ ∅ = ∅ :=
set.ext $ λ a, ⟨λ ⟨h, h'⟩, h', λ h, false.elim h⟩

[Cerek Hillen (he) (W2'20)]

I'm just recently learning about the axiomatic description of set theory, so bear with me. When you say I know too much about how sets are implemented / too many lemmas about them, do just mean that it's generally better to provide proofs that don't rely on operators' definitions & facts about them?

[Cerek Hillen (he) (W2'20)]

Or just that in this situation, since it's a base-level proof about the union identity, that it's better to prove it without knowledge of constructions and proofs that one would prove with the result itself?

[Cerek Hillen (he) (W2'20)]

Also another introductory question, say I have the following 2 hypotheses:

h : ∀ (x : α), x ∈ A → x ∈ B,
a : α

Intuitively I should be able to construct a hypothesis that states a ∈ A → a ∈ B, but how would I actually do that?

[Bryan Gin-ge Chen]

h a has type a ∈ A → a ∈ B.

[Cerek Hillen (he) (W2'20)]

oh! i didn't realize that \forall operators actually presented themselves as functions, or function-adjacent thing

[Cerek Hillen (he) (W2'20)]

i get the sense that i'm using the word wrong so far as lean is concerned

[Bryan Gin-ge Chen]

Well, the way I would phrase it (which might be a little off still...) is that the forall "creates" a dependent function type, thus something whose type is a forall (like h) is a function. (The section of TPiL I linked talks about "Pi" types, see this section for why forall and Pi are the same).

[Cerek Hillen (he) (W2'20)]

Ah ok, that makes sense--it's like in a type theoretic mathematical system where you'd say a thing is true iff there exists a function of the type A -> true (or A -> 1 i guess technically)

[Cerek Hillen (he) (W2'20)]

but since forall describes a property of some thing, it's just equivalent to some A -> Prop, except you have to provide some a : A

[Cerek Hillen (he) (W2'20)]

my only knowledge of type theory is the introductory section of Homotopy Type Theory so some of my intuitions might be off

[Kevin Buzzard]

You should probably read the first few sections of theorem proving in Lean, I think you'll find it very enlightening

[Cerek Hillen (he) (W2'20)]

On it :slight_smile:

[Cerek Hillen (he) (W2'20)]

Thanks for pointing me towards Theorem Proving in Lean, Kevin. I'm finding it a big help. NN game focuses a lot on rewrite rules so Chapt 3 has been really good about getting a sense for constructive proofs

[Cerek Hillen (he) (W2'20)]

(at least the early parts of NN Game)