---

Step * of Lemma stream-lex_transitivity-proof2

∀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 ((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
         )
   ) }

1
.....antecedent..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.x R y)
4. AntiSym(T;x,y.x R y)
⊢ rel-monotone{i:l}(stream(T);R@0.λs1,s2. ((s-hd(s1) R s-hd(s2))
                                         ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R@0 s-tl(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':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(\000CT;R))
⊢ Trans(stream(T);s1,s2.s1 stream-lex(T;R) s2)

---

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  ((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
              )
  )

---

Home Index