Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
⊢ ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L) = L
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
⊢ (Tape.move Dir.right^[n]) (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons (ListBlank.head R) L) (ListBlank.tail R)
suffices ∀ i L, (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L) = L by
  refine' (Eq.symm _).trans (this n _)
  simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
    ListBlank.tail_cons]
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
i : ℕ
L✝ : Tape Bool
⊢ (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L✝) = L✝
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
⊢ ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L) = L
intro i _
case zero
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
L✝ : Tape Bool
⊢ (Tape.move Dir.right^[Nat.zero]) ((Tape.move Dir.left^[Nat.zero]) L✝) = L✝

case succ
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L✝) = L✝
⊢ (Tape.move Dir.right^[Nat.succ i]) ((Tape.move Dir.left^[Nat.succ i]) L✝) = L✝
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
i : ℕ
L✝ : Tape Bool
⊢ (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L✝) = L✝
induction' i with i IH
no goals
case succ
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L✝) = L✝
⊢ (Tape.move Dir.right^[Nat.succ i]) ((Tape.move Dir.left^[Nat.succ i]) L✝) = L✝
rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L) = L
⊢ (Tape.move Dir.right^[n])
      ((Tape.move Dir.left^[n]) (trTape' enc0 (ListBlank.cons (ListBlank.head R) L) (ListBlank.tail R))) =
    (Tape.move Dir.right^[n]) (trTape' enc0 L R)
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape (?m.376770 i)), (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L) = L
⊢ (Tape.move Dir.right^[n]) (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons (ListBlank.head R) L) (ListBlank.tail R)
refine' (Eq.symm _).trans (this n _)
no goals
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right^[i]) ((Tape.move Dir.left^[i]) L) = L
⊢ (Tape.move Dir.right^[n])
      ((Tape.move Dir.left^[n]) (trTape' enc0 (ListBlank.cons (ListBlank.head R) L) (ListBlank.tail R))) =
    (Tape.move Dir.right^[n]) (trTape' enc0 L R)
simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
  ListBlank.tail_cons]
no goals
case zero
Γ : Type u_1
inst✝² : Inhabited Γ
Λ : Type ?u.373349
inst✝¹ : Inhabited Λ
σ : Type ?u.373355
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
enc0 : enc default = Vector.replicate n false
M : Λ → Stmt₁
L R : ListBlank Γ
L✝ : Tape Bool
⊢ (Tape.move Dir.right^[Nat.zero]) ((Tape.move Dir.left^[Nat.zero]) L✝) = L✝
rfl