case halt
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.eval Cont.halt v

case cons₁
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ a✝² a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₁ a✝² a✝¹ a✝) v

case cons₂
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ a✝¹ a✝) v

case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
k : Cont
v : List ℕ
⊢ eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
induction k generalizing v
case cons₁
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ a✝² a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₁ a✝² a✝¹ a✝) v

case cons₂
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ a✝¹ a✝) v

case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case halt
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.eval Cont.halt v

case cons₁
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ a✝² a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₁ a✝² a✝¹ a✝) v

case cons₂
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ a✝¹ a✝) v

case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case halt =>
  simp only [mem_eval, Cont.eval, map_pure]
  exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
case cons₂
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ a✝¹ a✝) v

case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case cons₁
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ a✝² a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₁ a✝² a✝¹ a✝) v

case cons₂
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ a✝¹ a✝) v

case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case cons₁ fs as k IH =>
  rw [Cont.eval, stepRet, code_is_ok]
  simp only [← bind_pure_comp, bind_assoc]; congr ; funext v'
  rw [reaches_eval]; swap; exact ReflTransGen.single rfl
  rw [stepRet, IH, bind_pure_comp]
case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case cons₂
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ a✝¹ a✝) v

case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case comp
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.comp a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.comp a✝¹ a✝) v

case fix
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, eval step (stepRet a✝ v) = Cfg.halt <$> Cont.eval a✝ v
v : List ℕ
⊢ eval step (stepRet (Cont.fix a✝¹ a✝) v) = Cfg.halt <$> Cont.eval (Cont.fix a✝¹ a✝) v
case comp f k IH =>
  rw [Cont.eval, stepRet, code_is_ok]
  simp only [← bind_pure_comp, bind_assoc]; congr ; funext v'
  rw [reaches_eval]; swap; exact ReflTransGen.single rfl
  rw [IH, bind_pure_comp]
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = pure (Cfg.halt v)
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.eval Cont.halt v
simp only [mem_eval, Cont.eval, map_pure]
no goals
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = pure (Cfg.halt v)
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v_1 ← Code.eval fs as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    Cfg.halt <$>
      (fun v => do
          let ns ← Code.eval fs as
          Cont.eval k (List.headI v :: ns))
        v
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> Cont.eval (Cont.cons₁ fs as k) v
rw [Cont.eval, stepRet, code_is_ok]
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v_1 ← Code.eval fs as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← Code.eval fs as
    let a ← Cont.eval k (List.headI v :: x)
    pure (Cfg.halt a)
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v_1 ← Code.eval fs as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    Cfg.halt <$>
      (fun v => do
          let ns ← Code.eval fs as
          Cont.eval k (List.headI v :: ns))
        v
simp only [← bind_pure_comp, bind_assoc]
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x => do
    let a ← Cont.eval k (List.headI v :: x)
    pure (Cfg.halt a)
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v_1 ← Code.eval fs as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← Code.eval fs as
    let a ← Cont.eval k (List.headI v :: x)
    pure (Cfg.halt a)
congr
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x => do
    let a ← Cont.eval k (List.headI v :: x)
    pure (Cfg.halt a)
funext v'
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.199598 = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)

case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.199598

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)
rw [reaches_eval]
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.199598

case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.199598 = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.199598 = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)

case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.199598

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
swap
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.199598

case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.199598 = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
exact ReflTransGen.single rfl
no goals
case e_a.h
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← Cont.eval k (List.headI v :: v')
    pure (Cfg.halt a)
rw [stepRet, IH, bind_pure_comp]
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (stepRet k (List.headI ns :: v)) = Cfg.halt <$> (fun v => Cont.eval k (List.headI ns :: v)) v
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> Cont.eval (Cont.cons₂ ns k) v
rw [Cont.eval, stepRet]
no goals
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (stepRet k (List.headI ns :: v)) = Cfg.halt <$> (fun v => Cont.eval k (List.headI ns :: v)) v
exact IH
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v ← Code.eval f v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun v => Code.eval f v >>= Cont.eval k) v
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> Cont.eval (Cont.comp f k) v
rw [Cont.eval, stepRet, code_is_ok]
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v ← Code.eval f v
      eval step (Cfg.ret k v)) =
    do
    let x ← Code.eval f v
    let a ← Cont.eval k x
    pure (Cfg.halt a)
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v ← Code.eval f v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun v => Code.eval f v >>= Cont.eval k) v
simp only [← bind_pure_comp, bind_assoc]
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (fun v => eval step (Cfg.ret k v)) = fun x => do
    let a ← Cont.eval k x
    pure (Cfg.halt a)
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (do
      let v ← Code.eval f v
      eval step (Cfg.ret k v)) =
    do
    let x ← Code.eval f v
    let a ← Cont.eval k x
    pure (Cfg.halt a)
congr
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (Cfg.ret k v') = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ (fun v => eval step (Cfg.ret k v)) = fun x => do
    let a ← Cont.eval k x
    pure (Cfg.halt a)
funext v'
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.200290 = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)

case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.200290

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (Cfg.ret k v') = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)
rw [reaches_eval]
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.200290

case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.200290 = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.200290 = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)

case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.200290

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
swap
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (stepRet k v') = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.200290

case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step ?m.200290 = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ Cfg
exact ReflTransGen.single rfl
no goals
case e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v v' : List ℕ
⊢ eval step (stepRet k v') = do
    let a ← Cont.eval k v'
    pure (Cfg.halt a)
rw [IH, bind_pure_comp]
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (if List.headI v = 0 then stepRet k (List.tail v) else stepNormal f (Cont.fix f k) (List.tail v)) =
    Cfg.halt <$>
      (fun v =>
          if List.headI v = 0 then Cont.eval k (List.tail v) else Code.eval (Code.fix f) (List.tail v) >>= Cont.eval k)
        v
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (stepRet (Cont.fix f k) v) = Cfg.halt <$> Cont.eval (Cont.fix f k) v
rw [Cont.eval, stepRet]
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (if List.headI v = 0 then stepRet k (List.tail v) else stepNormal f (Cont.fix f k) (List.tail v)) =
    Cfg.halt <$>
      if List.headI v = 0 then Cont.eval k (List.tail v) else Code.eval (Code.fix f) (List.tail v) >>= Cont.eval k
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (if List.headI v = 0 then stepRet k (List.tail v) else stepNormal f (Cont.fix f k) (List.tail v)) =
    Cfg.halt <$>
      (fun v =>
          if List.headI v = 0 then Cont.eval k (List.tail v) else Code.eval (Code.fix f) (List.tail v) >>= Cont.eval k)
        v
simp only [bind_pure_comp]
case inl
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : List.headI v = 0
⊢ eval step (stepRet k (List.tail v)) = Cfg.halt <$> Cont.eval k (List.tail v)

case inr
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ eval step (stepNormal f (Cont.fix f k) (List.tail v)) =
    Cfg.halt <$> (Code.eval (Code.fix f) (List.tail v) >>= Cont.eval k)
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
⊢ eval step (if List.headI v = 0 then stepRet k (List.tail v) else stepNormal f (Cont.fix f k) (List.tail v)) =
    Cfg.halt <$>
      if List.headI v = 0 then Cont.eval k (List.tail v) else Code.eval (Code.fix f) (List.tail v) >>= Cont.eval k
split_ifs
case inr
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ (do
      let v ← Code.eval (Code.fix f) (List.tail v)
      eval step (Cfg.ret k v)) =
    do
    let x ← Code.eval (Code.fix f) (List.tail v)
    let a ← Cont.eval k x
    pure (Cfg.halt a)
case inr
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ eval step (stepNormal f (Cont.fix f k) (List.tail v)) =
    Cfg.halt <$> (Code.eval (Code.fix f) (List.tail v) >>= Cont.eval k)
simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
case inr.e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ (fun v => eval step (Cfg.ret k v)) = fun x => do
    let a ← Cont.eval k x
    pure (Cfg.halt a)
case inr
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ (do
      let v ← Code.eval (Code.fix f) (List.tail v)
      eval step (Cfg.ret k v)) =
    do
    let x ← Code.eval (Code.fix f) (List.tail v)
    let a ← Cont.eval k x
    pure (Cfg.halt a)
congr
case inr.e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = do
    let a ← Cont.eval k x✝
    pure (Cfg.halt a)
case inr.e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ (fun v => eval step (Cfg.ret k v)) = fun x => do
    let a ← Cont.eval k x
    pure (Cfg.halt a)
funext
case inr.e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = eval step (stepRet k x✝)
case inr.e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = do
    let a ← Cont.eval k x✝
    pure (Cfg.halt a)
rw [bind_pure_comp, ← IH]
no goals
case inr.e_a.h
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : ¬List.headI v = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = eval step (stepRet k x✝)
exact reaches_eval (ReflTransGen.single rfl)
no goals
case inl
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> Cont.eval k v
v : List ℕ
h✝ : List.headI v = 0
⊢ eval step (stepRet k (List.tail v)) = Cfg.halt <$> Cont.eval k (List.tail v)
exact IH