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