---

Step * 1 of Lemma decidable__rel_plus


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. [R] : T ⟶ T ⟶ ℙ
4. f : T ⟶ ℕ@i
5. ∀[n:ℕ+]. ∀[x,y:T].  ((f x) + n) ≤ (f y) supposing x R^n y
⊢ rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀x,y:T.  Dec(x R+ y))
BY
{ (Assert ∀n:ℕ+. ∀x,y:T.  ((x R^n y) ⇒ (n ≤ (f y))) BY
         (RepeatFor 4 (ParallelLast) THEN Auto')) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. [R] : T ⟶ T ⟶ ℙ
4. f : T ⟶ ℕ@i
5. ∀[n:ℕ+]. ∀[x,y:T].  ((f x) + n) ≤ (f y) supposing x R^n y
6. ∀n:ℕ+. ∀x,y:T.  ((x R^n y) ⇒ (n ≤ (f y)))
⊢ rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀x,y:T.  Dec(x R+ y))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  f  :  T  {}\mrightarrow{}  \mBbbN{}@i
5.  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x,y:T].    ((f  x)  +  n)  \mleq{}  (f  y)  supposing  x  rel\_exp(T;  R;  n)  y
\mvdash{}  rel\_finite(T;R)  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  R  y))  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  R\msupplus{}  y))


By

---

Latex:
(Assert  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:T.    ((x  rel\_exp(T;  R;  n)  y)  {}\mRightarrow{}  (n  \mleq{}  (f  y)))  BY
              (RepeatFor  4  (ParallelLast)  THEN  Auto'))

---

Home Index