---

Step * 1 1 of Lemma dep-accum_wf


1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. g : a:A ⟶ b:B ⟶ C[a;b]
6. n : ℕ
7. bs : B List
8. ∀b1:B List
     (||b1|| < ||bs||
     ⇒ (dep-accum(L,b.f[L;b];a,b.g[a;b];b1) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                                vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = b1 ∈ (B List))} ))
9. bs ~ if (||bs|| =z 0) then [] else firstn(||bs|| - 1;bs) @ [last(bs)] fi 
10. ¬(||bs|| = 0 ∈ ℤ)
11. dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs|| - 1;bs)) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                                              vdf-eq(A;f;L)
                                                              ∧ (map(λx.(fst(snd(x)));L)
                                                                = firstn(||bs|| - 1;bs)
                                                                ∈ (B List))} 
12. v : {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))} 
13. dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs))
= v
∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))} 
14. f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)}  ⟶ B ⟶ A
15. a : A
16. f[v;last(bs)] = a ∈ A
⊢ v @ [<a, last(bs), g[a;last(bs)]>] ∈ {L:(a:A × b:B × C[a;b]) List| 
                                       vdf-eq(A;f;L)
                                       ∧ (map(λx.(fst(snd(x)));L) = (firstn(||bs|| - 1;bs) @ [last(bs)]) ∈ (B List))} 
BY
{ (DVar `v' THEN (MemTypeCD THENW Auto) THEN (D 0 ORELSE Auto)) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. g : a:A ⟶ b:B ⟶ C[a;b]
6. n : ℕ
7. bs : B List
8. ∀b1:B List
     (||b1|| < ||bs||
     ⇒ (dep-accum(L,b.f[L;b];a,b.g[a;b];b1) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                                vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = b1 ∈ (B List))} ))
9. bs ~ if (||bs|| =z 0) then [] else firstn(||bs|| - 1;bs) @ [last(bs)] fi 
10. ¬(||bs|| = 0 ∈ ℤ)
11. dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs|| - 1;bs)) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                                              vdf-eq(A;f;L)
                                                              ∧ (map(λx.(fst(snd(x)));L)
                                                                = firstn(||bs|| - 1;bs)
                                                                ∈ (B List))} 
12. v : (a:A × b:B × C[a;b]) List
13. vdf-eq(A;f;v) ∧ (map(λx.(fst(snd(x)));v) = firstn(||bs|| - 1;bs) ∈ (B List))
14. dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs))
= v
∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))} 
15. f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)}  ⟶ B ⟶ A
16. a : A
17. f[v;last(bs)] = a ∈ A
⊢ vdf-eq(A;f;v @ [<a, last(bs), g[a;last(bs)]>])

2
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. g : a:A ⟶ b:B ⟶ C[a;b]
6. n : ℕ
7. bs : B List
8. ∀b1:B List
     (||b1|| < ||bs||
     ⇒ (dep-accum(L,b.f[L;b];a,b.g[a;b];b1) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                                vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = b1 ∈ (B List))} ))
9. bs ~ if (||bs|| =z 0) then [] else firstn(||bs|| - 1;bs) @ [last(bs)] fi 
10. ¬(||bs|| = 0 ∈ ℤ)
11. dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs|| - 1;bs)) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                                              vdf-eq(A;f;L)
                                                              ∧ (map(λx.(fst(snd(x)));L)
                                                                = firstn(||bs|| - 1;bs)
                                                                ∈ (B List))} 
12. v : (a:A × b:B × C[a;b]) List
13. vdf-eq(A;f;v) ∧ (map(λx.(fst(snd(x)));v) = firstn(||bs|| - 1;bs) ∈ (B List))
14. dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs))
= v
∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))} 
15. f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)}  ⟶ B ⟶ A
16. a : A
17. f[v;last(bs)] = a ∈ A
⊢ map(λx.(fst(snd(x)));v @ [<a, last(bs), g[a;last(bs)]>]) = (firstn(||bs|| - 1;bs) @ [last(bs)]) ∈ (B List)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type
4.  f  :  very-dep-fun(A;B;a,b.C[a;b])
5.  g  :  a:A  {}\mrightarrow{}  b:B  {}\mrightarrow{}  C[a;b]
6.  n  :  \mBbbN{}
7.  bs  :  B  List
8.  \mforall{}b1:B  List
          (||b1||  <  ||bs||
          {}\mRightarrow{}  (dep-accum(L,b.f[L;b];a,b.g[a;b];b1)  \mmember{}  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List| 
                                                                                                vdf-eq(A;f;L)  \mwedge{}  (map(\mlambda{}x.(fst(snd(x)));L)  =  b1)\}  ))
9.  bs  \msim{}  if  (||bs||  =\msubz{}  0)  then  []  else  firstn(||bs||  -  1;bs)  @  [last(bs)]  fi 
10.  \mneg{}(||bs||  =  0)
11.  dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs||  -  1;bs))  \mmember{}  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List| 
                                                                                                                            vdf-eq(A;f;L)
                                                                                                                            \mwedge{}  (map(\mlambda{}x.(fst(snd(x)));L)
                                                                                                                                =  firstn(||bs||  -  1;bs))\} 
12.  v  :  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List| 
                  vdf-eq(A;f;L)  \mwedge{}  (map(\mlambda{}x.(fst(snd(x)));L)  =  firstn(||bs||  -  1;bs))\} 
13.  dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs||  -  1;bs))  =  v
14.  f  \mmember{}  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List|  vdf-eq(A;f;L)\}    {}\mrightarrow{}  B  {}\mrightarrow{}  A
15.  a  :  A
16.  f[v;last(bs)]  =  a
\mvdash{}  v  @  [<a,  last(bs),  g[a;last(bs)]>]  \mmember{}  \{L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List| 
                                                                              vdf-eq(A;f;L)
                                                                              \mwedge{}  (map(\mlambda{}x.(fst(snd(x)));L)
                                                                                  =  (firstn(||bs||  -  1;bs)  @  [last(bs)]))\} 


By

---

Latex:
(DVar  `v'  THEN  (MemTypeCD  THENW  Auto)  THEN  (D  0  ORELSE  Auto))

---

Home Index