---

Step * of Lemma decidable__rel_exp

∀k,n:ℕ.  ∀[R:ℕn ⟶ ℕn ⟶ ℙ]. ((∀i,j:ℕn.  Dec(i R j)) ⇒ (∀i,j:ℕn.  Dec(i R^k j)))
BY
{ (InductionOnNat THEN RecUnfold `rel_exp` 0 THEN Reduce 0 THEN Auto THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}k,n:\mBbbN{}.    \mforall{}[R:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}i,j:\mBbbN{}n.    Dec(i  R  j))  {}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}n.    Dec(i  rel\_exp(\mBbbN{}n;  R;  k)  j)))


By

---

Latex:
(InductionOnNat  THEN  RecUnfold  `rel\_exp`  0  THEN  Reduce  0  THEN  Auto  THEN  AutoSplit)

---

Home Index