---

Step * of Lemma stream-lex-monotonic

∀T:Type
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀R:T ⟶ T ⟶ ℙ
        (Trans(T;x,y.x R y)
        ⇒ AntiSym(T;x,y.x R y)
        ⇒ (∀f:T ⟶ T ⟶ T
              ((∀x,y,u,v:T.  ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v))))
              ⇒ (∀x,y,u,v:T.  ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T))))
              ⇒ (∀a,b,c,d:stream(T).
                    ((a stream-lex(T;R) b)
                    ⇒ (c stream-lex(T;R) d)
                    ⇒ (stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)))))))))
BY
{ (Auto
   THEN ((InstLemma `implies-bigrel` [⌜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))))⌝]⋅
         THENM Fold `stream-lex` (-1)
         )
         THENA (Auto THEN RepUR ``rel-monotone rel_implies`` 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. 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))
⊢ stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)

---

Latex:

---

Latex:
\mforall{}T:Type
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
                (Trans(T;x,y.x  R  y)
                {}\mRightarrow{}  AntiSym(T;x,y.x  R  y)
                {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
                            ((\mforall{}x,y,u,v:T.    ((x  R  y)  {}\mRightarrow{}  (u  R  v)  {}\mRightarrow{}  ((f  x  u)  R  (f  y  v))))
                            {}\mRightarrow{}  (\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)))))
                            {}\mRightarrow{}  (\mforall{}a,b,c,d:stream(T).
                                        ((a  stream-lex(T;R)  b)
                                        {}\mRightarrow{}  (c  stream-lex(T;R)  d)
                                        {}\mRightarrow{}  (stream-zip(f;a;c)  stream-lex(T;R)  stream-zip(f;b;d)))))))))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `implies-bigrel`  [\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{}
              THENM  Fold  `stream-lex`  (-1)
              )
              THENA  (Auto  THEN  RepUR  ``rel-monotone  rel\_implies``  0  THEN  Auto)
              )
  )

---

Home Index