---

Step * of Lemma stream-decomp

∀[s:stream(Top)]. (s ~ s-hd(s).s-tl(s))
BY
{ ((Auto THEN GenConcl⌜s = ss ∈ (Top × stream(Top))⌝⋅)
   THEN Auto
   THEN Try ((D -2 THEN RepUR ``s-hd s-tl s-cons`` 0 THEN Auto))) }

1
.....wf..... 
1. s : stream(Top)
⊢ s ∈ Top × stream(Top)

---

Latex:

---

Latex:
\mforall{}[s:stream(Top)].  (s  \msim{}  s-hd(s).s-tl(s))


By

---

Latex:
((Auto  THEN  GenConcl\mkleeneopen{}s  =  ss\mkleeneclose{}\mcdot{})
  THEN  Auto
  THEN  Try  ((D  -2  THEN  RepUR  ``s-hd  s-tl  s-cons``  0  THEN  Auto)))

---

Home Index