---

Step * of Lemma map-square-board_wf

∀[n:ℕ]. ∀[T1,T2:Type]. ∀[f:ℕn ⟶ ℕn ⟶ T1 ⟶ T2]. ∀[b:square-board(n;T1)].
  (map-square-board(i,j,v.f[i;j;v];b) ∈ square-board(n;T2))
BY
{ (Auto THEN All (RepUR ``map-square-board square-board``) THEN RepeatFor 2 (D -1) THEN MemTypeCD) }

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

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

3
.....wf..... 
1. n : ℕ
2. T1 : Type
3. T2 : Type
4. f : ℕn ⟶ ℕn ⟶ T1 ⟶ T2
5. b : T1 List List
6. ||b|| = n ∈ ℤ
7. ∀i:ℕn. (||b[i]|| = n ∈ ℤ)
8. s : T2 List List
⊢ (||s|| = n ∈ ℤ) ∧ (∀i:ℕn. (||s[i]|| = n ∈ ℤ)) ∈ Type

---

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)].
    (map-square-board(i,j,v.f[i;j;v];b)  \mmember{}  square-board(n;T2))


By

---

Latex:
(Auto  THEN  All  (RepUR  ``map-square-board  square-board``)  THEN  RepeatFor  2  (D  -1)  THEN  MemTypeCD)

---

Home Index