---

Step * of Lemma decidable__rel_plus

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀[R:T ⟶ T ⟶ ℙ]. (SWellFounded(x R y) ⇒ rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀x,y:T.  Dec(x R+ y)))))
BY
{ (InstLemma `strongwellfounded_rel_exp` []
   THEN ParallelLast'
   THEN (D 0 THENA Auto)
   THEN PromoteHyp (-1) 2
   THEN ParallelLast'
   THEN (D 0 THENA Auto)
   THEN RenameVar `swf' (-1)
   THEN (InstHyp [⌜swf⌝] (-2)⋅ THENA Auto)
   THEN Thin (-3)
   THEN D -2
   THEN Reduce (-1)
   THEN Thin (-2)) }

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
⊢ rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀x,y:T.  Dec(x R+ y))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
                (SWellFounded(x  R  y)
                {}\mRightarrow{}  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:
(InstLemma  `strongwellfounded\_rel\_exp`  []
  THEN  ParallelLast'
  THEN  (D  0  THENA  Auto)
  THEN  PromoteHyp  (-1)  2
  THEN  ParallelLast'
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `swf'  (-1)
  THEN  (InstHyp  [\mkleeneopen{}swf\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  D  -2
  THEN  Reduce  (-1)
  THEN  Thin  (-2))

---

Home Index