---

Step * of Lemma stream-pointwise_transitivity

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (Trans(T;x,y.x R y) ⇒ Trans(stream(T);s1,s2.s1 stream-pointwise(R) s2))
BY
{ (Auto
   THEN Unfold `stream-pointwise` 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-tl(s1) 
                                                                                                        lex 
                                                                                                        s-tl(s2)))⌝] ⋅
   THEN Auto
   THEN Reduce 0) }

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

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

3
1. T : Type@i'
2. R : T ⟶ T ⟶ ℙ@i'
3. Trans(T;x,y.x R y)@i
⊢ 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{}  Trans(stream(T);s1,s2.s1  stream-pointwise(R)  s2))


By

---

Latex:
(Auto
  THEN  Unfold  `stream-pointwise`  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-tl(s1)  lex  s-tl(s2)))\mkleeneclose{}]  \mcdot{}
  THEN  Auto
  THEN  Reduce  0)

---

Home Index