Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝ : Γ → Stmt Bool Λ' σ
this :
  ∀ (i : ℕ) (f : Vector Bool i → Stmt Bool Λ' σ),
    (∀ (v : Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
v✝ : Vector Bool n
⊢ SupportsStmt S (move Dir.left (f✝ (dec v✝)))
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝ : Γ → Stmt Bool Λ' σ
this :
  ∀ (i : ℕ) (f : Vector Bool i → Stmt Bool Λ' σ),
    (∀ (v : Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
⊢ ∀ (v : Vector Bool n), SupportsStmt S (move Dir.left (f✝ (dec v)))
intro
no goals
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝ : Γ → Stmt Bool Λ' σ
this :
  ∀ (i : ℕ) (f : Vector Bool i → Stmt Bool Λ' σ),
    (∀ (v : Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
v✝ : Vector Bool n
⊢ SupportsStmt S (move Dir.left (f✝ (dec v✝)))
simp only [supportsStmt_move, hf]
case zero
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝¹ : Γ → Stmt Bool Λ' σ
i : ℕ
f✝ : Vector Bool i → Stmt Bool Λ' σ
hf✝ : ∀ (v : Vector Bool i), SupportsStmt S (f✝ v)
f : Vector Bool Nat.zero → Stmt Bool Λ' σ
hf : ∀ (v : Vector Bool Nat.zero), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux Nat.zero f)

case succ
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝¹ : Γ → Stmt Bool Λ' σ
i✝ : ℕ
f✝ : Vector Bool i✝ → Stmt Bool Λ' σ
hf✝ : ∀ (v : Vector Bool i✝), SupportsStmt S (f✝ v)
i : ℕ
IH :
  ∀ (f : Vector Bool i → Stmt Bool Λ' σ), (∀ (v : Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : Vector Bool (Nat.succ i) → Stmt Bool Λ' σ
hf : ∀ (v : Vector Bool (Nat.succ i)), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux (Nat.succ i) f)
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝ : Γ → Stmt Bool Λ' σ
i : ℕ
f : Vector Bool i → Stmt Bool Λ' σ
hf : ∀ (v : Vector Bool i), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux i f)
induction' i with i IH
no goals
case succ
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝¹ : Γ → Stmt Bool Λ' σ
i✝ : ℕ
f✝ : Vector Bool i✝ → Stmt Bool Λ' σ
hf✝ : ∀ (v : Vector Bool i✝), SupportsStmt S (f✝ v)
i : ℕ
IH :
  ∀ (f : Vector Bool i → Stmt Bool Λ' σ), (∀ (v : Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : Vector Bool (Nat.succ i) → Stmt Bool Λ' σ
hf : ∀ (v : Vector Bool (Nat.succ i)), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux (Nat.succ i) f)
constructor <;> apply IH <;> intro <;> apply hf
no goals
case zero
Γ : Type u_3
inst✝² : Inhabited Γ
Λ : Type u_2
inst✝¹ : Inhabited Λ
σ : Type u_1
inst✝ : Inhabited σ
n : ℕ
enc : Γ → Vector Bool n
dec : Vector Bool n → Γ
S : Finset Λ'
f✝¹ : Γ → Stmt Bool Λ' σ
i : ℕ
f✝ : Vector Bool i → Stmt Bool Λ' σ
hf✝ : ∀ (v : Vector Bool i), SupportsStmt S (f✝ v)
f : Vector Bool Nat.zero → Stmt Bool Λ' σ
hf : ∀ (v : Vector Bool Nat.zero), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux Nat.zero f)
exact hf _