---

Step * of Lemma decidable__rel_exp_finite

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀[R:T ⟶ T ⟶ ℙ]. (rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀k:ℕ. ∀x,y:T.  Dec(x R^k y)))))
BY
{ (InductionOnNat
   THEN Try ((RecUnfold `rel_exp` 0 THEN Reduce 0 THEN Trivial))
   THEN Auto
   THEN Assert ⌜x R^k y ⇐⇒ ∃z:T. ((x R^k - 1 z) ∧ (z R y))⌝⋅) }

1
.....assertion..... 
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. [R] : T ⟶ T ⟶ ℙ
4. rel_finite(T;R)
5. ∀x,y:T.  Dec(x R y)
6. k : ℤ
7. [%4] : 0 < k
8. ∀x,y:T.  Dec(x R^k - 1 y)
9. x : T
10. y : T
⊢ x R^k y ⇐⇒ ∃z:T. ((x R^k - 1 z) ∧ (z R y))

2
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. [R] : T ⟶ T ⟶ ℙ
4. rel_finite(T;R)
5. ∀x,y:T.  Dec(x R y)
6. k : ℤ
7. [%4] : 0 < k
8. ∀x,y:T.  Dec(x R^k - 1 y)
9. x : T
10. y : T
11. x R^k y ⇐⇒ ∃z:T. ((x R^k - 1 z) ∧ (z R y))
⊢ Dec(x R^k y)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
                (rel\_finite(T;R)  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  R  y))  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  \mforall{}x,y:T.    Dec(x  rel\_exp(T;  R;  k)  y)))))


By

---

Latex:
(InductionOnNat
  THEN  Try  ((RecUnfold  `rel\_exp`  0  THEN  Reduce  0  THEN  Trivial))
  THEN  Auto
  THEN  Assert  \mkleeneopen{}x  rel\_exp(T;  R;  k)  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}z:T.  ((x  rel\_exp(T;  R;  k  -  1)  z)  \mwedge{}  (z  R  y))\mkleeneclose{}\mcdot{})

---

Home Index