---

Step * of Lemma dep-accum_wf

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[g:a:A ⟶ b:B ⟶ C[a;b]]. ∀[bs:B List].
  (dep-accum(L,b.f[L;b];a,b.g[a;b];bs) ∈ {L:(a:A × b:B × C[a;b]) List| 
                                          vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = bs ∈ (B List))} )
BY
{ (InductionOnLength
   THEN (InstLemma `last-decomp2` [⌜bs⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN (SplitOnConclITE THENA Auto)
   THEN ((Unfold `dep-accum` 0
          THEN (RWO "list_accum_append" 0 THENA Auto)
          THEN Fold `dep-accum` 0
          THEN Reduce 0
          THEN (InstHyp [⌜firstn(||bs|| - 1;bs)⌝] (-3)⋅ THENA Auto)
          THEN (GenConclTerm ⌜dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs))⌝⋅ THENA Auto))
   ORELSE (RepUR``dep-accum`` 0 THEN MemTypeCD THEN Auto THEN ProveVdfEq)
   )) }

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 : {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))} 
⊢ v @ let a = f[v;last(bs)] in [<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))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[f:very-dep-fun(A;B;a,b.C[a;b])].  \mforall{}[g:a:A  {}\mrightarrow{}  b:B  {}\mrightarrow{}  C[a;b]].
\mforall{}[bs:B  List].
    (dep-accum(L,b.f[L;b];a,b.g[a;b];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)  =  bs)\}  )


By

---

Latex:
(InductionOnLength
  THEN  (InstLemma  `last-decomp2`  [\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  ((Unfold  `dep-accum`  0
                THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
                THEN  Fold  `dep-accum`  0
                THEN  Reduce  0
                THEN  (InstHyp  [\mkleeneopen{}firstn(||bs||  -  1;bs)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
                THEN  (GenConclTerm  \mkleeneopen{}dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs||  -  1;bs))\mkleeneclose{}\mcdot{}  THENA  Auto))
  ORELSE  (RepUR``dep-accum``  0  THEN  MemTypeCD  THEN  Auto  THEN  ProveVdfEq)
  ))

---

Home Index