---

Step * of Lemma stream-pointwise-iff

∀[T:Type]
  ∀R:T ⟶ T ⟶ ℙ. ∀s1,s2:stream(T).
    (s1 stream-pointwise(R) s2 ⇐⇒ (s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) stream-pointwise(R) s-tl(s2)))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `bigrel-iff` [⌜stream(T)⌝;⌜λ2lex.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) lex s-tl(s2)))⌝]⋅ THENA A\000Cuto)
   THEN Try ((Fold `stream-pointwise` (-1) THEN RepUR ``rel_implies`` (-1) THEN Auto THEN BackThruSomeHyp THEN Auto))) }

1
.....antecedent..... 
1. [T] : Type
2. R : T ⟶ T ⟶ ℙ@i'
3. s1 : stream(T)@i
4. s2 : stream(T)@i
⊢ rel-monotone{i:l}(stream(T);R@0.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) R@0 s-tl(s2))))

2
.....antecedent..... 
1. [T] : Type
2. R : T ⟶ T ⟶ ℙ@i'
3. s1 : stream(T)@i
4. s2 : stream(T)@i
⊢ rel-continuous{i:l}(stream(T);R@0.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) R@0 s-tl(s2))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}s1,s2:stream(T).
        (s1  stream-pointwise(R)  s2  \mLeftarrow{}{}\mRightarrow{}  (s-hd(s1)  R  s-hd(s2))  \mwedge{}  (s-tl(s1)  stream-pointwise(R)  s-tl(s2)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `bigrel-iff`  [\mkleeneopen{}stream(T)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}lex.\mlambda{}s1,s2.  ((s-hd(s1)  R  s-hd(s2))
                                                                                                                  \mwedge{}  (s-tl(s1)  lex  s-tl(s2)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Try  ((Fold  `stream-pointwise`  (-1)
                        THEN  RepUR  ``rel\_implies``  (-1)
                        THEN  Auto
                        THEN  BackThruSomeHyp
                        THEN  Auto)))

---

Home Index