---

Step * 1 1 1 2 1 1 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. x : stream(T)
10. y : stream(T)
11. a : stream(T)
12. b : stream(T)
13. c : stream(T)
14. stream-zip(f;a;c) ∈ stream(T)
15. d : stream(T)
16. stream-zip(f;b;d) ∈ stream(T)
17. s-hd(a) R s-hd(b)
18. (s-hd(a) = s-hd(b) ∈ T) ⇒ (s-tl(a) stream-lex(T;R) s-tl(b))
19. s-hd(c) R s-hd(d)
20. (s-hd(c) = s-hd(d) ∈ T) ⇒ (s-tl(c) stream-lex(T;R) s-tl(d))
21. (f s-hd(a) s-hd(c)) = (f s-hd(b) s-hd(d)) ∈ T
⊢ ∃a@0,b@0,c@0,d@0:stream(T)
   ((s-tl(stream-zip(f;a;c)) = stream-zip(f;a@0;c@0) ∈ stream(T))
   ∧ (s-tl(stream-zip(f;b;d)) = stream-zip(f;b@0;d@0) ∈ stream(T))
   ∧ (a@0 stream-lex(T;R) b@0)
   ∧ (c@0 stream-lex(T;R) d@0))
BY
{ (D (-2)
   THENA (SupposeNot
          THEN Assert ⌜¬((f s-hd(a) s-hd(c)) = (f s-hd(b) s-hd(d)) ∈ T)⌝⋅
          THEN Auto
          THEN (BackThruSomeHyp THEN Auto)
          THEN D 0
          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. x : stream(T)
10. y : stream(T)
11. a : stream(T)
12. b : stream(T)
13. c : stream(T)
14. stream-zip(f;a;c) ∈ stream(T)
15. d : stream(T)
16. stream-zip(f;b;d) ∈ stream(T)
17. s-hd(a) R s-hd(b)
18. (s-hd(a) = s-hd(b) ∈ T) ⇒ (s-tl(a) stream-lex(T;R) s-tl(b))
19. s-hd(c) R s-hd(d)
20. (f s-hd(a) s-hd(c)) = (f s-hd(b) s-hd(d)) ∈ T
21. s-tl(c) stream-lex(T;R) s-tl(d)
⊢ ∃a@0,b@0,c@0,d@0:stream(T)
   ((s-tl(stream-zip(f;a;c)) = stream-zip(f;a@0;c@0) ∈ stream(T))
   ∧ (s-tl(stream-zip(f;b;d)) = stream-zip(f;b@0;d@0) ∈ stream(T))
   ∧ (a@0 stream-lex(T;R) b@0)
   ∧ (c@0 stream-lex(T;R) d@0))

---

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.  x  :  stream(T)
10.  y  :  stream(T)
11.  a  :  stream(T)
12.  b  :  stream(T)
13.  c  :  stream(T)
14.  stream-zip(f;a;c)  \mmember{}  stream(T)
15.  d  :  stream(T)
16.  stream-zip(f;b;d)  \mmember{}  stream(T)
17.  s-hd(a)  R  s-hd(b)
18.  (s-hd(a)  =  s-hd(b))  {}\mRightarrow{}  (s-tl(a)  stream-lex(T;R)  s-tl(b))
19.  s-hd(c)  R  s-hd(d)
20.  (s-hd(c)  =  s-hd(d))  {}\mRightarrow{}  (s-tl(c)  stream-lex(T;R)  s-tl(d))
21.  (f  s-hd(a)  s-hd(c))  =  (f  s-hd(b)  s-hd(d))
\mvdash{}  \mexists{}a@0,b@0,c@0,d@0:stream(T)
      ((s-tl(stream-zip(f;a;c))  =  stream-zip(f;a@0;c@0))
      \mwedge{}  (s-tl(stream-zip(f;b;d))  =  stream-zip(f;b@0;d@0))
      \mwedge{}  (a@0  stream-lex(T;R)  b@0)
      \mwedge{}  (c@0  stream-lex(T;R)  d@0))


By

---

Latex:
(D  (-2)
  THENA  (SupposeNot
                THEN  Assert  \mkleeneopen{}\mneg{}((f  s-hd(a)  s-hd(c))  =  (f  s-hd(b)  s-hd(d)))\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  (BackThruSomeHyp  THEN  Auto)
                THEN  D  0
                THEN  Auto)
  )

---

Home Index