Step * 1 1 of Lemma decidable__rel_plus


1. [T] Type
2. ∀x,y:T.  Dec(x y ∈ T)@i
3. [R] T ⟶ T ⟶ ℙ
4. T ⟶ ℕ@i
5. ∀[n:ℕ+]. ∀[x,y:T].  ((f x) n) ≤ (f y) supposing R^n y
6. ∀n:ℕ+. ∀x,y:T.  ((x R^n y)  (n ≤ (f y)))
⊢ rel_finite(T;R)  (∀x,y:T.  Dec(x y))  (∀x,y:T.  Dec(x R+ y))
BY
(Auto
   THEN ((Assert R+ ⇐⇒ ∃k:{1..(f y) 1-}. (x R^k y) BY
                (RepUR ``rel_plus`` THEN Auto THEN ParallelLast THEN Auto THEN Assert ⌜n ≤ (f y)⌝⋅ THEN Auto))
         THEN (RWO "-1" THENM BLemma `decidable__exists_int_seg`)
         THEN Auto
         THEN BLemma `decidable__rel_exp_finite`⋅
         THEN Auto)⋅
   }


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
6.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:T.    ((x  rel\_exp(T;  R;  n)  y)  {}\mRightarrow{}  (n  \mleq{}  (f  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:
(Auto
  THEN  ((Assert  x  R\msupplus{}  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}k:\{1..(f  y)  +  1\msupminus{}\}.  (x  rel\_exp(T;  R;  k)  y)  BY
                            (RepUR  ``rel\_plus``  0
                              THEN  Auto
                              THEN  ParallelLast
                              THEN  Auto
                              THEN  Assert  \mkleeneopen{}n  \mleq{}  (f  y)\mkleeneclose{}\mcdot{}
                              THEN  Auto))
              THEN  (RWO  "-1"  0  THENM  BLemma  `decidable\_\_exists\_int\_seg`)
              THEN  Auto
              THEN  BLemma  `decidable\_\_rel\_exp\_finite`\mcdot{}
              THEN  Auto)\mcdot{}
  )




Home Index