---

Step * of Lemma stream-coinduction

∀[A:Type]. ∀[R:stream(A) ⟶ stream(A) ⟶ ℙ].
  ∀[x,y:stream(A)].  x = y ∈ stream(A) supposing x R y 
  supposing ∀x,y:stream(A).  ((x R y) ⇒ ((s-hd(x) = s-hd(y) ∈ A) ∧ (s-tl(x) R s-tl(y))))
BY
{ (Auto
   THEN InstLemma `coinduction-principle` [⌜λ2T.A × T⌝;⌜R⌝]⋅
   THEN Auto
   THEN All (Fold `stream`)
   THEN Auto
   THEN Try ((BHyp (-1) THEN Auto))) }

1
1. A : Type
2. R : stream(A) ⟶ stream(A) ⟶ ℙ
3. ∀x,y:stream(A).  ((x R y) ⇒ ((s-hd(x) = s-hd(y) ∈ A) ∧ (s-tl(x) R s-tl(y))))
4. x : stream(A)
5. y : stream(A)
6. x R y
⊢ x,y.R[x;y] is an T.A × T-bisimulation

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:stream(A)  {}\mrightarrow{}  stream(A)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[x,y:stream(A)].    x  =  y  supposing  x  R  y 
    supposing  \mforall{}x,y:stream(A).    ((x  R  y)  {}\mRightarrow{}  ((s-hd(x)  =  s-hd(y))  \mwedge{}  (s-tl(x)  R  s-tl(y))))


By

---

Latex:
(Auto
  THEN  InstLemma  `coinduction-principle`  [\mkleeneopen{}\mlambda{}\msubtwo{}T.A  \mtimes{}  T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  (Fold  `stream`)
  THEN  Auto
  THEN  Try  ((BHyp  (-1)  THEN  Auto)))

---

Home Index