---

Step * 1 of Lemma compose-strict-inc


1. s : ℕ ⟶ ℕ@i
2. ∀j:ℕ. ∀i:ℕj.  s i < s j@i
3. f : ℕ ⟶ ℕ@i
4. ∀j:ℕ. ∀i:ℕj.  f i < f j@i
5. j : ℕ@i
6. i : ℕj@i
⊢ (s o f) i < (s o f) j
BY
{ (Reduce 0 THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  s  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
2.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    s  i  <  s  j@i
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
4.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    f  i  <  f  j@i
5.  j  :  \mBbbN{}@i
6.  i  :  \mBbbN{}j@i
\mvdash{}  (s  o  f)  i  <  (s  o  f)  j


By

---

Latex:
(Reduce  0  THEN  BackThruSomeHyp)

---

Home Index