---

Step * of Lemma stream-lex-iff

∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀s1,s2:stream(T).
  (s1 stream-lex(T;R) s2 ⇐⇒ (s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) stream-lex(T;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-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) lex s-tl(s2))))⌝]⋅
         THENA Auto
         )
   THEN Try ((Fold `stream-lex` (-1) THEN RepUR ``rel_implies`` (-1) THEN Auto THEN BackThruSomeHyp THEN Auto))) }

1
.....antecedent..... 
1. T : Type@i'
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-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R@0 s-tl(s2)))))

2
.....antecedent..... 
1. T : Type@i'
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-hd(s1) = s-hd(s2) ∈ T) ⇒ (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-lex(T;R)  s2
    \mLeftarrow{}{}\mRightarrow{}  (s-hd(s1)  R  s-hd(s2))  \mwedge{}  ((s-hd(s1)  =  s-hd(s2))  {}\mRightarrow{}  (s-tl(s1)  stream-lex(T;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-hd(s1)  =  s-hd(s2))
                                                                                                                      {}\mRightarrow{}  (s-tl(s1)  lex  s-tl(s2))))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Try  ((Fold  `stream-lex`  (-1)
                        THEN  RepUR  ``rel\_implies``  (-1)
                        THEN  Auto
                        THEN  BackThruSomeHyp
                        THEN  Auto)))

---

Home Index