---

Step * of Lemma list-at-combine-skips

∀[ms,ns:colist(ℕ)]. ∀[k:ℕ]. ∀[T:Type]. ∀[L:colist(T)].  (L@combine-skips(ns;ms;k) = nth_tl(k;L)@ns@ms ∈ colist(T))
BY
{ ((Auto
    THEN Unfold `colist` 0
    THEN Unfold `corec` 0
    THEN (EqTypeCD THENW Auto)
    THEN RepeatFor 5 (MoveToConcl (-2))
    THEN NatInd (-1)
    THEN Intros
    THEN (RWO "primrec-unroll" 0 THENA Auto)
    THEN (OReduce 0 THENA Auto))
   THENL [Auto
         ; (colistD (-5)
            THENL [((Unfold `combine-skips` 0 THEN Reduce 0) THEN Unfold `nil` 0 THEN BUnionLeft THEN Auto)
                  ; ...]
         )]
) }

1
1. n : ℤ
2. 0 < n
3. ∀ms,ns:colist(ℕ). ∀k:ℕ. ∀T:Type. ∀L:colist(T).
     (L@combine-skips(ns;ms;k) = nth_tl(k;L)@ns@ms ∈ primrec(n - 1;Top;λ,L. (Unit ⋃ (T × L))))
4. u : ℤ
5. T : Type
6. v : colist(ℕ)
7. u1 : ℕ
8. v1 : colist(ℕ)
9. k : ℕ
10. L : colist(T)
⊢ L@combine-skips([u1 / v1];[0 / v];k)
= nth_tl(k;L)@[u1 / v1]@[0 / v]
∈ (Unit ⋃ (T × primrec(n - 1;Top;λ,L. (Unit ⋃ (T × L)))))

2
1. n : ℤ
2. 0 < n
3. ∀ms,ns:colist(ℕ). ∀k:ℕ. ∀T:Type. ∀L:colist(T).
     (L@combine-skips(ns;ms;k) = nth_tl(k;L)@ns@ms ∈ primrec(n - 1;Top;λ,L. (Unit ⋃ (T × L))))
4. T : Type
5. u : ℤ
6. 0 < u
7. ∀v,ns:colist(ℕ). ∀k:ℕ. ∀L:colist(T).
     (L@combine-skips(ns;[u - 1 / v];k)
     = nth_tl(k;L)@ns@[u - 1 / v]
     ∈ (Unit ⋃ (T × primrec(n - 1;Top;λ,L. (Unit ⋃ (T × L))))))
8. v : colist(ℕ)
9. u1 : ℕ
10. v1 : colist(ℕ)
11. k : ℕ
12. L : colist(T)
13. ¬(u = 0 ∈ ℤ)
⊢ L@combine-skips([u1 / v1];[u / v];k)
= nth_tl(k;L)@[u1 / v1]@[u / v]
∈ (Unit ⋃ (T × primrec(n - 1;Top;λ,L. (Unit ⋃ (T × L)))))

---

Latex:

---

Latex:
\mforall{}[ms,ns:colist(\mBbbN{})].  \mforall{}[k:\mBbbN{}].  \mforall{}[T:Type].  \mforall{}[L:colist(T)].
    (L@combine-skips(ns;ms;k)  =  nth\_tl(k;L)@ns@ms)


By

---

Latex:
((Auto
    THEN  Unfold  `colist`  0
    THEN  Unfold  `corec`  0
    THEN  (EqTypeCD  THENW  Auto)
    THEN  RepeatFor  5  (MoveToConcl  (-2))
    THEN  NatInd  (-1)
    THEN  Intros
    THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
    THEN  (OReduce  0  THENA  Auto))
  THENL  [Auto
              ;  (colistD  (-5)
                    THENL  [((Unfold  `combine-skips`  0  THEN  Reduce  0)
                                    THEN  Unfold  `nil`  0
                                    THEN  BUnionLeft
                                    THEN  Auto)
                                ;  (MoveToConcl  (-1)
                                      THEN  RepeatFor  3  (MoveToConcl  (-2))
                                      THEN  NatInd  (-2)
                                      THEN  Intros
                                      THEN  Try  ((Assert  \mneg{}(u  =  0)  BY  Complete  (Auto)))
                                      THEN  OnVar  `ns'  colistD
                                      THEN  Try  (((Unfold  `combine-skips`  0  THEN  Reduce  0)
                                                            THEN  Unfold  `nil`  0
                                                            THEN  BUnionLeft
                                                            THEN  Auto)))]
              )]
)

---

Home Index