---

Step * of Lemma fun_exp-increasing

∀[T:Type]. ((T ⊆r ℤ) ⇒ (∀f:T ⟶ T. ((∀n:T. n < f n) ⇒ (∀n:T. ∀i,j:ℕ.  (i < j ⇒ f^i n < f^j n)))))
BY
{ (Auto
   THEN (Assert ∀d:ℕ. ∀n:T.  f^i n < f^(d + 1) + i n BY
               (ThinVar `n'
                THEN ThinVar `j'
                THEN InductionOnNat
                THEN Reduce 0
                THEN Try ((Subst' (d + 1) + i ~ 1 + ((d - 1) + 1) + i 0 THEN Auto))
                THEN (((RWO "fun_exp_add" 0 THEN Reduce 0) THEN Auto)
                      THEN (InstHyp [⌜n⌝] (-2)⋅ THENA Auto)
                      THEN InstHyp [⌜f^((d - 1) + 1) + i n⌝] 4⋅
                      THEN Auto)⋅))
   ) }

1
1. T : Type
2. T ⊆r ℤ
3. f : T ⟶ T
4. ∀n:T. n < f n
5. n : T
6. i : ℕ
7. j : ℕ
8. i < j
9. ∀d:ℕ. ∀n:T.  f^i n < f^(d + 1) + i n
⊢ f^i n < f^j n

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((T  \msubseteq{}r  \mBbbZ{})  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  ((\mforall{}n:T.  n  <  f  n)  {}\mRightarrow{}  (\mforall{}n:T.  \mforall{}i,j:\mBbbN{}.    (i  <  j  {}\mRightarrow{}  f\^{}i  n  <  f\^{}j  n)))))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}d:\mBbbN{}.  \mforall{}n:T.    f\^{}i  n  <  f\^{}(d  +  1)  +  i  n  BY
                          (ThinVar  `n'
                            THEN  ThinVar  `j'
                            THEN  InductionOnNat
                            THEN  Reduce  0
                            THEN  Try  ((Subst'  (d  +  1)  +  i  \msim{}  1  +  ((d  -  1)  +  1)  +  i  0  THEN  Auto))
                            THEN  (((RWO  "fun\_exp\_add"  0  THEN  Reduce  0)  THEN  Auto)
                                        THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                                        THEN  InstHyp  [\mkleeneopen{}f\^{}((d  -  1)  +  1)  +  i  n\mkleeneclose{}]  4\mcdot{}
                                        THEN  Auto)\mcdot{}))
  )

---

Home Index