K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
o : StAct k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' =
          ListBlank.mk (List.reverse (List.map some (update S k (stWrite v (S k) o) k_1)))) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q (stVar v (S k) o)
          ((Tape.move Dir.right^[List.length (update S k (stWrite v (S k) o) k)]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
o : StAct k
⊢ let v' := stVar v (S k) o;
  let Sk' := stWrite v (S k) o;
  let S' := update S k Sk';
  ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.reverse (List.map some (S' k)))) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q v' ((Tape.move Dir.right^[List.length (S' k)]) (Tape.mk' ∅ (addBottom L')))
dsimp only
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
o : StAct k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' =
          ListBlank.mk (List.reverse (List.map some (update S k (stWrite v (S k) o) k_1)))) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q (stVar v (S k) o)
          ((Tape.move Dir.right^[List.length (stWrite v (S k) o)]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
o : StAct k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' =
          ListBlank.mk (List.reverse (List.map some (update S k (stWrite v (S k) o) k_1)))) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q (stVar v (S k) o)
          ((Tape.move Dir.right^[List.length (update S k (stWrite v (S k) o) k)]) (Tape.mk' ∅ (addBottom L')))
simp
case push
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
a✝ : σ → Γ k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (a✝ v :: S k) k_1)))) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
                update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (a✝ v)))
              ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right^[List.length (a✝ v :: S k)]) (Tape.mk' ∅ (addBottom L')))

case peek
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
a✝ : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (S k) k_1)))) ∧
      TM1.stepAux q
          (a✝ v
            (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head
              k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (a✝ v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L')))

case pop
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
a✝ : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (List.tail (S k)) k_1)))) ∧
      (bif ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst then
          TM1.stepAux q (a✝ v none) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (a✝ v
              (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head
                k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head.fst,
                update
                  (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head.snd k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (a✝ v (List.head? (S k)))
          ((Tape.move Dir.right^[List.length (List.tail (S k))]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
o : StAct k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' =
          ListBlank.mk (List.reverse (List.map some (update S k (stWrite v (S k) o) k_1)))) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q (stVar v (S k) o)
          ((Tape.move Dir.right^[List.length (stWrite v (S k) o)]) (Tape.mk' ∅ (addBottom L')))
cases o <;> simp only [stWrite, stVar, trStAct, TM1.stepAux]
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k_1)))) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
                update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (f v)))
              ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right^[List.length (f v :: S k)]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k_1)))) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
                update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (f v)))
              ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right^[List.length (f v :: S k)]) (Tape.mk' ∅ (addBottom L')))
have := Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k (some (f v)))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k_1)))) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
                update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (f v)))
              ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right^[List.length (f v :: S k)]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k_1)))) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
                update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (f v)))
              ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right^[List.length (f v :: S k)]) (Tape.mk' ∅ (addBottom L')))
dsimp only at this
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k (some (f v))) (List.length (S k)) L) =
    ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k_1)))) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
                update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (f v)))
              ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right^[List.length (f v :: S k)]) (Tape.mk' ∅ (addBottom L')))
refine'
  ⟨_, fun k' ↦ _, by
    erw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this,
      addBottom_modifyNth fun a ↦ update a k (some (f v)), Nat.add_one, iterate_succ']
    rfl⟩
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
⊢ ListBlank.nth (ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k (some (f v))) (List.length (S k)) L))
      i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k (some (f v))) (List.length (S k)) L) =
    ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))
refine' ListBlank.ext fun i ↦ _
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
⊢ ListBlank.nth (ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k (some (f v))) (List.length (S k)) L))
      i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
h' : k' = k
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i

case neg
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
by_cases h' : k' = k
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right^[List.length (S k)])
          (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a => update a k (some (f v))) (List.length (S k)) L))))) =
    TM1.stepAux q v ((Tape.move Dir.right ∘ Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom ?m.674949)))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        (Tape.write
          (((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst,
            update ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.snd k (some (f v)))
          ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q v ((Tape.move Dir.right^[List.length (f v :: S k)]) (Tape.mk' ∅ (addBottom ?m.674949)))
erw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this,
  addBottom_modifyNth fun a ↦ update a k (some (f v)), Nat.add_one, iterate_succ']
no goals
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right^[List.length (S k)])
          (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a => update a k (some (f v))) (List.length (S k)) L))))) =
    TM1.stepAux q v ((Tape.move Dir.right ∘ Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom ?m.674949)))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))

K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
⊢ ListBlank ((k : K) → Option (Γ k))
rfl
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k)))) i
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
h' : k' = k
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
subst k'
case pos.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h : i = List.length (S k)
⊢ some (f v) = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i

case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h : ¬i = List.length (S k)
⊢ ListBlank.nth L i k = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k)))) i
split_ifs with h
  <;> simp only [List.reverse_cons, Function.update_same, ListBlank.nth_mk, List.map]
case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h : ¬i = List.length (S k)
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h : ¬i = List.length (S k)
⊢ ListBlank.nth L i k = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
rw [← proj_map_nth, hL, ListBlank.nth_mk]
case pos.inr.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : i < List.length (S k)
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i

case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : i > List.length (S k)
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h : ¬i = List.length (S k)
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
cases' lt_or_gt_of_ne h with h h
no goals
case pos.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h : i = List.length (S k)
⊢ some (f v) = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
rw [List.getI_eq_get, List.get_append_right'] <;>
  simp only [h, List.get_singleton, List.length_map, List.length_reverse, Nat.succ_pos',
    List.length_append, lt_add_iff_pos_right, List.length, le_refl]
case pos.inr.inl.h
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : i < List.length (S k)
⊢ i < List.length (List.reverse (List.map some (S k)))
case pos.inr.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : i < List.length (S k)
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
rw [List.getI_append]
no goals
case pos.inr.inl.h
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : i < List.length (S k)
⊢ i < List.length (List.reverse (List.map some (S k)))
simpa only [List.length_map, List.length_reverse] using h
case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : List.length (S k) < i
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : i > List.length (S k)
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
rw [gt_iff_lt] at h
no goals
case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = List.length (S k)
h : List.length (S k) < i
⊢ List.getI (List.reverse (List.map some (S k))) i = List.getI (List.reverse (List.map some (S k)) ++ [some (f v)]) i
rw [List.getI_eq_default, List.getI_eq_default] <;>
  simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
    List.length_append, List.length_map]
case neg.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = List.length (S k)
⊢ ListBlank.nth (ListBlank.mk (List.reverse (List.map some (S k')))) i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
case neg
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ ite (i = List.length (S k)) (update (ListBlank.nth L i) k (some (f v))) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
split_ifs <;> rw [Function.update_noteq h', ← proj_map_nth, hL]
no goals
case neg.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Γ k
this :
  ∀ (L R : ListBlank Γ') (n : ℕ),
    Tape.write ((ListBlank.nth R n).fst, update (ListBlank.nth R n).snd k (some (f v)))
        ((Tape.move Dir.right^[n]) (Tape.mk' L R)) =
      (Tape.move Dir.right^[n]) (Tape.mk' L (ListBlank.modifyNth (fun a => (a.fst, update a.snd k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = List.length (S k)
⊢ ListBlank.nth (ListBlank.mk (List.reverse (List.map some (S k')))) i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (f v :: S k) k')))) i
rw [Function.update_noteq h']
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.reverse (List.map some (S k)))) ∧
      TM1.stepAux q
          (f v
            (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head
              k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (S k) k_1)))) ∧
      TM1.stepAux q
          (f v
            (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head
              k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L')))
rw [Function.update_eq_self]
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ TM1.stepAux q
      (f v
        (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head k))
      (Tape.move Dir.right
        (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.reverse (List.map some (S k)))) ∧
      TM1.stepAux q
          (f v
            (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head
              k))
          (Tape.move Dir.right
            (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L')))
use L, hL
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ TM1.stepAux q
      (f v
        (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head k))
      ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
    TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ TM1.stepAux q
      (f v
        (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head k))
      (Tape.move Dir.right
        (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))
rw [Tape.move_left_right]
case e_a.e_a
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head k =
    List.head? (S k)
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ TM1.stepAux q
      (f v
        (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head k))
      ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))) =
    TM1.stepAux q (f v (List.head? (S k))) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))
congr
case e_a.e_a.nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head k =
    List.head? []

case e_a.e_a.cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (head✝ :: tail✝)]) (Tape.mk' ∅ (addBottom L)))).head
      k =
    List.head? (head✝ :: tail✝)
case e_a.e_a
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head k =
    List.head? (S k)
cases e : S k
case e_a.e_a.cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ some head✝ = List.head? (head✝ :: tail✝)
case e_a.e_a.cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (head✝ :: tail✝)]) (Tape.mk' ∅ (addBottom L)))).head
      k =
    List.head? (head✝ :: tail✝)
rw [List.length_cons, iterate_succ', Function.comp, Tape.move_right_left,
  Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hL k), e,
  List.reverse_cons, ← List.length_reverse, List.get?_concat_length]
no goals
case e_a.e_a.cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ some head✝ = List.head? (head✝ :: tail✝)
rfl
no goals
case e_a.e_a.nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head k =
    List.head? []
rfl
case nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (List.tail []) k_1)))) ∧
      (bif ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L))).head.fst then
          TM1.stepAux q (f v none) ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v
              (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head
                k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head.fst,
                update (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head.snd
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (List.head? []))
          ((Tape.move Dir.right^[List.length (List.tail [])]) (Tape.mk' ∅ (addBottom L')))

case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' =
          ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k_1)))) ∧
      (bif ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L))).head.fst then
          TM1.stepAux q (f v none) ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v
              (Prod.snd
                (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head
                k))
            (Tape.write
              ((Tape.move Dir.left
                      ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head.fst,
                update
                  (Tape.move Dir.left
                        ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head.snd
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (List.head? (hd :: tl)))
          ((Tape.move Dir.right^[List.length (List.tail (hd :: tl))]) (Tape.mk' ∅ (addBottom L')))
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (List.tail (S k)) k_1)))) ∧
      (bif ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L))).head.fst then
          TM1.stepAux q (f v none) ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v
              (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head
                k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head.fst,
                update
                  (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))).head.snd k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length (S k)]) (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (List.head? (S k)))
          ((Tape.move Dir.right^[List.length (List.tail (S k))]) (Tape.mk' ∅ (addBottom L')))
cases' e : S k with hd tl
case nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k [] k_1)))) ∧
      (bif (ListBlank.head (addBottom L)).fst then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (Prod.snd (ListBlank.head ∅) k))
            (Tape.mk' (ListBlank.tail ∅)
              (ListBlank.cons ((ListBlank.head ∅).fst, update (ListBlank.head ∅).snd k none) (addBottom L)))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))
case nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k (List.tail []) k_1)))) ∧
      (bif ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L))).head.fst then
          TM1.stepAux q (f v none) ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v
              (Prod.snd (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head
                k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head.fst,
                update (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))).head.snd
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length []]) (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (List.head? []))
          ((Tape.move Dir.right^[List.length (List.tail [])]) (Tape.mk' ∅ (addBottom L')))
simp only [Tape.mk'_head, ListBlank.head_cons, Tape.move_left_mk', List.length,
  Tape.write_mk', List.head?, iterate_zero_apply, List.tail_nil]
case nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.reverse (List.map some (S k)))) ∧
      (bif (ListBlank.head (addBottom L)).fst then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (Prod.snd (ListBlank.head ∅) k))
            (Tape.mk' (ListBlank.tail ∅)
              (ListBlank.cons ((ListBlank.head ∅).fst, update (ListBlank.head ∅).snd k none) (addBottom L)))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))
case nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.reverse (List.map some (update S k [] k_1)))) ∧
      (bif (ListBlank.head (addBottom L)).fst then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (Prod.snd (ListBlank.head ∅) k))
            (Tape.mk' (ListBlank.tail ∅)
              (ListBlank.cons ((ListBlank.head ∅).fst, update (ListBlank.head ∅).snd k none) (addBottom L)))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))
rw [← e, Function.update_eq_self]
no goals
case nil
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.reverse (List.map some (S k)))) ∧
      (bif (ListBlank.head (addBottom L)).fst then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (Prod.snd (ListBlank.head ∅) k))
            (Tape.mk' (ListBlank.tail ∅)
              (ListBlank.cons ((ListBlank.head ∅).fst, update (ListBlank.head ∅).snd k none) (addBottom L)))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))
exact ⟨L, hL, by rw [addBottom_head_fst, cond]⟩
no goals
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
e : S k = []
⊢ (bif (ListBlank.head (addBottom L)).fst then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
    else
      TM1.stepAux q (f v (Prod.snd (ListBlank.head ∅) k))
        (Tape.mk' (ListBlank.tail ∅)
          (ListBlank.cons ((ListBlank.head ∅).fst, update (ListBlank.head ∅).snd k none) (addBottom L)))) =
    TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
rw [addBottom_head_fst, cond]
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k none) (List.length tl) L) =
    ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' =
          ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k_1)))) ∧
      (bif ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L))).head.fst then
          TM1.stepAux q (f v none) ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v
              (Prod.snd
                (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head
                k))
            (Tape.write
              ((Tape.move Dir.left
                      ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head.fst,
                update
                  (Tape.move Dir.left
                        ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head.snd
                  k none)
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (List.head? (hd :: tl)))
          ((Tape.move Dir.right^[List.length (List.tail (hd :: tl))]) (Tape.mk' ∅ (addBottom L')))
refine'
  ⟨_, fun k' ↦ _, by
    erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
      cond, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
      Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k none),
      addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
      stk_nth_val _ (hL k), e,
      show (List.cons hd tl).reverse.get? tl.length = some hd by
        rw [List.reverse_cons, ← List.length_reverse, List.get?_concat_length],
      List.head?, List.tail]⟩
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
⊢ ListBlank.nth (ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k none) (List.length tl) L)) i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k none) (List.length tl) L) =
    ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))
refine' ListBlank.ext fun i ↦ _
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
⊢ ListBlank.nth (ListBlank.map (proj k') (ListBlank.modifyNth (fun a => update a k none) (List.length tl) L)) i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : k' = k
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i

case neg
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
case cons
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
by_cases h' : k' = k
no goals
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ (bif ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L))).head.fst then
      TM1.stepAux q (f v none) ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux q
        (f v
          (Prod.snd
            (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head k))
        (Tape.write
          ((Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head.fst,
            update
              (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))).head.snd
              k none)
          (Tape.move Dir.left ((Tape.move Dir.right^[List.length (hd :: tl)]) (Tape.mk' ∅ (addBottom L)))))) =
    TM1.stepAux q (f v (List.head? (hd :: tl)))
      ((Tape.move Dir.right^[List.length (List.tail (hd :: tl))]) (Tape.mk' ∅ (addBottom ?m.691653)))
erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
  cond, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
  Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k none),
  addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
  stk_nth_val _ (hL k), e,
  show (List.cons hd tl).reverse.get? tl.length = some hd by
    rw [List.reverse_cons, ← List.length_reverse, List.get?_concat_length],
  List.head?, List.tail]
no goals
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ List.get? (List.reverse (hd :: tl)) (List.length tl) = some hd
rw [List.reverse_cons, ← List.length_reverse, List.get?_concat_length]
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k)))) i
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : k' = k
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
subst k'
case pos.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = List.length tl
⊢ none = List.getI (List.reverse (List.map some tl)) i

case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = List.length tl
⊢ ListBlank.nth L i k = List.getI (List.reverse (List.map some tl)) i
case pos
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k)))) i
split_ifs with h <;> simp only [Function.update_same, ListBlank.nth_mk, List.tail]
case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = List.length tl
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = List.length tl
⊢ ListBlank.nth L i k = List.getI (List.reverse (List.map some tl)) i
rw [← proj_map_nth, hL, ListBlank.nth_mk, e, List.map, List.reverse_cons]
case pos.inr.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : i < List.length tl
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i

case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : i > List.length tl
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
case pos.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = List.length tl
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
cases' lt_or_gt_of_ne h with h h
case pos.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = List.length tl
⊢ none = default

case pos.inl.hn
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = List.length tl
⊢ List.length (List.reverse (List.map some tl)) ≤ i
case pos.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = List.length tl
⊢ none = List.getI (List.reverse (List.map some tl)) i
rw [List.getI_eq_default]
no goals
case pos.inl.hn
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = List.length tl
⊢ List.length (List.reverse (List.map some tl)) ≤ i
rw [h, List.length_reverse, List.length_map]
no goals
case pos.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = List.length tl
⊢ none = default
rfl
case pos.inr.inl.h
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : i < List.length tl
⊢ i < List.length (List.reverse (List.map some tl))
case pos.inr.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : i < List.length tl
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
rw [List.getI_append]
no goals
case pos.inr.inl.h
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : i < List.length tl
⊢ i < List.length (List.reverse (List.map some tl))
simpa only [List.length_map, List.length_reverse] using h
case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : List.length tl < i
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : i > List.length tl
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
rw [gt_iff_lt] at h
no goals
case pos.inr.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = List.length tl
h : List.length tl < i
⊢ List.getI (List.reverse (List.map some tl) ++ [some hd]) i = List.getI (List.reverse (List.map some tl)) i
rw [List.getI_eq_default, List.getI_eq_default] <;>
  simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
    List.length_append, List.length_map]
case neg.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = List.length tl
⊢ ListBlank.nth (ListBlank.mk (List.reverse (List.map some (S k')))) i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
case neg
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
⊢ ite (i = List.length tl) (update (ListBlank.nth L i) k none) (ListBlank.nth L i) k' =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
split_ifs <;> rw [Function.update_noteq h', ← proj_map_nth, hL]
no goals
case neg.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_1
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
q : TM1.Stmt Γ' Λ' σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some (S k)))
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = List.length tl
⊢ ListBlank.nth (ListBlank.mk (List.reverse (List.map some (S k')))) i =
    ListBlank.nth (ListBlank.mk (List.reverse (List.map some (update S k (List.tail (hd :: tl)) k')))) i
rw [Function.update_noteq h']