---

Step * of Lemma stream-lex_transitivity

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (Trans(T;x,y.x R y) ⇒ AntiSym(T;x,y.x R y) ⇒ Trans(stream(T);s1,s2.s1 stream-lex(T;R) s2))
BY
{ (Auto
   THEN Unfold `stream-lex` 0
   THEN InstLemma `bigrel-induction` [⌜stream(T)⌝;⌜λ2R.Trans(stream(T);s1,s2.s1 R s2)⌝;⌜λ2lex.λs1,s2. ((s-hd(s1) 
                                                                                                        R 
                                                                                                        s-hd(s2))
                                                                                                     ∧ ((s-hd(s1)
                                                                                                       = s-hd(s2)
                                                                                                       ∈ T)
                                                                                                       ⇒ (s-tl(s1) 
                                                                                                           lex 
                                                                                                           s-tl(s2))))⌝]\000C ⋅
   THEN Auto
   THEN Reduce 0) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.x R y)
4. AntiSym(T;x,y.x R y)
5. Rs : ℕ ⟶ stream(T) ⟶ stream(T) ⟶ ℙ
6. ∀n:ℕ. Trans(stream(T);s1,s2.s1 Rs[n] s2)
⊢ Trans(stream(T);s1,s2.s1 isect-rel(ℕ;n.Rs[n]) s2)

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.x R y)
4. AntiSym(T;x,y.x R y)
5. R@0 : stream(T) ⟶ stream(T) ⟶ ℙ
6. Trans(stream(T);s1,s2.s1 R@0 s2)
⊢ Trans(stream(T);s1,s2.(s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R@0 s-tl(s2))))

3
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.x R y)
4. AntiSym(T;x,y.x R y)
⊢ Trans(stream(T);s1,s2.True)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (Trans(T;x,y.x  R  y)  {}\mRightarrow{}  AntiSym(T;x,y.x  R  y)  {}\mRightarrow{}  Trans(stream(T);s1,s2.s1  stream-lex(T;R)  s2))


By

---

Latex:
(Auto
  THEN  Unfold  `stream-lex`  0
  THEN  InstLemma  `bigrel-induction`  [\mkleeneopen{}stream(T)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}R.Trans(stream(T);s1,s2.s1  R  s2)\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{}
  THEN  Auto
  THEN  Reduce  0)

---

Home Index