Step * of Lemma decidable__rel_exp

k,n:ℕ.  ∀[R:ℕn ⟶ ℕn ⟶ ℙ]. ((∀i,j:ℕn.  Dec(i j))  (∀i,j:ℕn.  Dec(i R^k j)))
BY
(InductionOnNat THEN RecUnfold `rel_exp` THEN Reduce 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