---

Step * of Lemma map-square-board-cell

∀[n:ℕ]. ∀[T1,T2:Type]. ∀[f:ℕn ⟶ ℕn ⟶ T1 ⟶ T2]. ∀[b:square-board(n;T1)]. ∀[i,j:ℕn].
  (board-cell(map-square-board(i,j,v.f[i;j;v];b);i;j) = f[i;j;board-cell(b;i;j)] ∈ T2)
BY
{ (Auto THEN D -3 THEN RepUR ``board-cell map-square-board`` 0) }

1
1. n : ℕ
2. T1 : Type
3. T2 : Type
4. f : ℕn ⟶ ℕn ⟶ T1 ⟶ T2
5. b : T1 List List
6. (||b|| = n ∈ ℤ) ∧ (∀i:ℕn. (||b[i]|| = n ∈ ℤ))
7. i : ℕn
8. j : ℕn
⊢ map-index(λi,r. map-index(λj,v. f[i;j;v];r);b)[i][j] = f[i;j;b[i][j]] ∈ T2

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[T1,T2:Type].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  T1  {}\mrightarrow{}  T2].  \mforall{}[b:square-board(n;T1)].  \mforall{}[i,j:\mBbbN{}n].
    (board-cell(map-square-board(i,j,v.f[i;j;v];b);i;j)  =  f[i;j;board-cell(b;i;j)])


By

---

Latex:
(Auto  THEN  D  -3  THEN  RepUR  ``board-cell  map-square-board``  0)

---

Home Index