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. 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))
BY
{ (Auto
   THEN ((Assert x R+ y 
⇐⇒ ∃k:{1..(f y) + 1-}. (x R^k y) BY
                (RepUR ``rel_plus`` 0 THEN Auto THEN ParallelLast THEN Auto THEN Assert ⌜n ≤ (f y)⌝⋅ THEN Auto))
         THEN (RWO "-1" 0 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