---

Step * 1 of Lemma rel_exp_iff

.....basecase..... 
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀x,y:T.  (x R^0 y ⇐⇒ (∃z:T. (0 < 0 c∧ ((x R^0 - 1 z) ∧ (z R y)))) ∨ ((0 = 0 ∈ ℤ) ∧ (x = y ∈ T)))
BY
{ (Auto
   THEN SplitOrHyps
   THEN ExRepD
   THEN Auto
   THEN Try ((OrRight THEN Auto))
   THEN (All (\i. (RecUnfold `rel_exp` i THEN Reduce i THEN Try (Trivial))))⋅) }

---

Latex:

---

Latex:
.....basecase..... 
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,y:T.    (x  R\^{}0  y  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}z:T.  (0  <  0  c\mwedge{}  ((x  R\^{}0  -  1  z)  \mwedge{}  (z  R  y))))  \mvee{}  ((0  =  0)  \mwedge{}  (x  =  y)))


By

---

Latex:
(Auto
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  Auto
  THEN  Try  ((OrRight  THEN  Auto))
  THEN  (All  (\mbackslash{}i.  (RecUnfold  `rel\_exp`  i  THEN  Reduce  i  THEN  Try  (Trivial))))\mcdot{})

---

Home Index