α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : Results s a m
h2 : Results (f a) b n
this : a ∈ s
⊢ Results (bind s f) b (n + m)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : Results s a m
h2 : Results (f a) b n
⊢ Results (bind s f) b (n + m)
have := h1.mem
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
⊢ ∀ {m : ℕ}, Results s a m → Results (bind s f) b (n + m)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : Results s a m
h2 : Results (f a) b n
this : a ∈ s
⊢ Results (bind s f) b (n + m)
revert m
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
⊢ ∀ {m : ℕ}, Results (pure a) a m → Results (bind (pure a) f) b (n + m)

α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, Results s a m → Results (bind s f) b (n + m)) →
      ∀ {m : ℕ}, Results (think s) a m → Results (bind (think s) f) b (n + m)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
⊢ ∀ {m : ℕ}, Results s a m → Results (bind s f) b (n + m)
apply memRecOn this _ fun s IH => _
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
m✝ : ℕ
h1 : Results (pure a) a m✝
⊢ Results (bind (pure a) f) b (n + m✝)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
⊢ ∀ {m : ℕ}, Results (pure a) a m → Results (bind (pure a) f) b (n + m)
intro _ h1
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
m✝ : ℕ
h1 : Results (pure a) a m✝
⊢ Results (f a) b (n + m✝)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
m✝ : ℕ
h1 : Results (pure a) a m✝
⊢ Results (bind (pure a) f) b (n + m✝)
rw [ret_bind]
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
m✝ : ℕ
h1 : Results (pure a) a m✝
⊢ Results (f a) b (n + 0)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
m✝ : ℕ
h1 : Results (pure a) a m✝
⊢ Results (f a) b (n + m✝)
rw [h1.len_unique (results_pure _)]
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
m✝ : ℕ
h1 : Results (pure a) a m✝
⊢ Results (f a) b (n + 0)
exact h2
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1 : Results (think s✝) a m✝
⊢ Results (bind (think s✝) f) b (n + m✝)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, Results s a m → Results (bind s f) b (n + m)) →
      ∀ {m : ℕ}, Results (think s) a m → Results (bind (think s) f) b (n + m)
intro _ h3 _ h1
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1 : Results (think s✝) a m✝
⊢ Results (think (bind s✝ f)) b (n + m✝)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1 : Results (think s✝) a m✝
⊢ Results (bind (think s✝) f) b (n + m✝)
rw [think_bind]
case intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1 : Results (think s✝) a m✝
m' : ℕ
h : Results s✝ a m' ∧ m✝ = m' + 1
⊢ Results (think (bind s✝ f)) b (n + m✝)
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1 : Results (think s✝) a m✝
⊢ Results (think (bind s✝ f)) b (n + m✝)
cases' of_results_think h1 with m' h
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1✝ : Results (think s✝) a m✝
m' : ℕ
h1 : Results s✝ a m'
e : m✝ = m' + 1
⊢ Results (think (bind s✝ f)) b (n + m✝)
case intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1 : Results (think s✝) a m✝
m' : ℕ
h : Results s✝ a m' ∧ m✝ = m' + 1
⊢ Results (think (bind s✝ f)) b (n + m✝)
cases' h with h1 e
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1✝ : Results (think s✝) a m✝
m' : ℕ
h1 : Results s✝ a m'
e : m✝ = m' + 1
⊢ Results (think (bind s✝ f)) b (n + (m' + 1))
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1✝ : Results (think s✝) a m✝
m' : ℕ
h1 : Results s✝ a m'
e : m✝ = m' + 1
⊢ Results (think (bind s✝ f)) b (n + m✝)
rw [e]
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : Results (f a) b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, Results s✝ a m → Results (bind s✝ f) b (n + m)
m✝ : ℕ
h1✝ : Results (think s✝) a m✝
m' : ℕ
h1 : Results s✝ a m'
e : m✝ = m' + 1
⊢ Results (think (bind s✝ f)) b (n + (m' + 1))
exact results_think (h3 h1)