---

Step * 1 2 of Lemma stream-lex-monotonic


1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. R : T ⟶ T ⟶ ℙ
4. Trans(T;x,y.x R y)
5. AntiSym(T;x,y.x R y)
6. f : T ⟶ T ⟶ T
7. ∀x,y,u,v:T.  ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v)))
8. ∀x,y,u,v:T.  ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T)))
9. a : stream(T)
10. b : stream(T)
11. c : stream(T)
12. d : stream(T)
13. a stream-lex(T;R) b
14. c stream-lex(T;R) d
15. ∀R':stream(T) ⟶ stream(T) ⟶ ℙ
      (R' => λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R' s-tl(s2)))) ⇒ R' => stream-lex\000C(T;R))
16. λs1,s2. ∃a,b,c,d:stream(T)
             ((s1 = stream-zip(f;a;c) ∈ stream(T))
             ∧ (s2 = stream-zip(f;b;d) ∈ stream(T))
             ∧ (a stream-lex(T;R) b)
             ∧ (c stream-lex(T;R) d)) => stream-lex(T;R)
⊢ stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)
BY
{ (RepUR ``rel_implies`` -1 THEN BHyp -1  THEN Auto) }

1
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. R : T ⟶ T ⟶ ℙ
4. Trans(T;x,y.x R y)
5. AntiSym(T;x,y.x R y)
6. f : T ⟶ T ⟶ T
7. ∀x,y,u,v:T.  ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v)))
8. ∀x,y,u,v:T.  ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T)))
9. a : stream(T)
10. b : stream(T)
11. c : stream(T)
12. d : stream(T)
13. a stream-lex(T;R) b
14. c stream-lex(T;R) d
15. ∀R':stream(T) ⟶ stream(T) ⟶ ℙ
      (R' => λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R' s-tl(s2)))) ⇒ R' => stream-lex\000C(T;R))
16. ∀x,y:stream(T).
      ((∃a,b,c,d:stream(T)
         ((x = stream-zip(f;a;c) ∈ stream(T))
         ∧ (y = stream-zip(f;b;d) ∈ stream(T))
         ∧ (a stream-lex(T;R) b)
         ∧ (c stream-lex(T;R) d)))
      ⇒ (x stream-lex(T;R) y))
⊢ ∃a1,b1,c1,d1:stream(T)
   ((stream-zip(f;a;c) = stream-zip(f;a1;c1) ∈ stream(T))
   ∧ (stream-zip(f;b;d) = stream-zip(f;b1;d1) ∈ stream(T))
   ∧ (a1 stream-lex(T;R) b1)
   ∧ (c1 stream-lex(T;R) d1))

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  Trans(T;x,y.x  R  y)
5.  AntiSym(T;x,y.x  R  y)
6.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
7.  \mforall{}x,y,u,v:T.    ((x  R  y)  {}\mRightarrow{}  (u  R  v)  {}\mRightarrow{}  ((f  x  u)  R  (f  y  v)))
8.  \mforall{}x,y,u,v:T.    ((x  R  y)  {}\mRightarrow{}  (u  R  v)  {}\mRightarrow{}  (\mneg{}((x  =  y)  \mwedge{}  (u  =  v)))  {}\mRightarrow{}  (\mneg{}((f  x  u)  =  (f  y  v))))
9.  a  :  stream(T)
10.  b  :  stream(T)
11.  c  :  stream(T)
12.  d  :  stream(T)
13.  a  stream-lex(T;R)  b
14.  c  stream-lex(T;R)  d
15.  \mforall{}R':stream(T)  {}\mrightarrow{}  stream(T)  {}\mrightarrow{}  \mBbbP{}
            (R'  =>  \mlambda{}s1,s2.  ((s-hd(s1)  R  s-hd(s2))  \mwedge{}  ((s-hd(s1)  =  s-hd(s2))  {}\mRightarrow{}  (s-tl(s1)  R'  s-tl(s2))))
            {}\mRightarrow{}  R'  =>  stream-lex(T;R))
16.  \mlambda{}s1,s2.  \mexists{}a,b,c,d:stream(T)
                          ((s1  =  stream-zip(f;a;c))
                          \mwedge{}  (s2  =  stream-zip(f;b;d))
                          \mwedge{}  (a  stream-lex(T;R)  b)
                          \mwedge{}  (c  stream-lex(T;R)  d))  =>  stream-lex(T;R)
\mvdash{}  stream-zip(f;a;c)  stream-lex(T;R)  stream-zip(f;b;d)


By

---

Latex:
(RepUR  ``rel\_implies``  -1  THEN  BHyp  -1    THEN  Auto)

---

Home Index