---

Step * of Lemma combine-skips_wf

∀[bs,as:colist(ℕ)]. ∀[k:ℕ].  (combine-skips(as;bs;k) ∈ colist(ℕ))
BY
{ (Auto
   THEN Unfold `colist` 0
   THEN Unfold `corec` 0
   THEN (MemTypeCD THENW Auto)
   THEN RepeatFor 3 (MoveToConcl (-2))
   THEN NatInd 1
   THEN Intros
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)
   THEN Try (MemTop)) }

1
1. n : ℤ
2. 0 < n
3. ∀bs,as:colist(ℕ). ∀k:ℕ.  (combine-skips(as;bs;k) ∈ primrec(n - 1;Top;λ,L. (Unit ⋃ (ℕ × L))))
4. bs : colist(ℕ)
5. as : colist(ℕ)
6. k : ℕ
⊢ combine-skips(as;bs;k) ∈ Unit ⋃ (ℕ × primrec(n - 1;Top;λ,L. (Unit ⋃ (ℕ × L))))

---

Latex:

---

Latex:
\mforall{}[bs,as:colist(\mBbbN{})].  \mforall{}[k:\mBbbN{}].    (combine-skips(as;bs;k)  \mmember{}  colist(\mBbbN{}))


By

---

Latex:
(Auto
  THEN  Unfold  `colist`  0
  THEN  Unfold  `corec`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-2))
  THEN  NatInd  1
  THEN  Intros
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto)
  THEN  Try  (MemTop))

---

Home Index