---

Step * of Lemma rel_plus_implies

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R+ y) ⇒ ((x R y) ∨ (∃z:T. ((x R+ z) ∧ (z R y)))))
BY
{ (Auto
   THEN (Unfold `rel_plus` (-1))
   THEN (Reduce (-1))
   THEN ExRepD
   THEN (MoveToConcl (-1))
   THEN (MoveToConcl (-2))
   THEN (MoveToConcl (-2))
   THEN (NatPlusInd (-1))
   THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. n : ℕ+
4. x : T
5. y : T
6. x R^1 y
⊢ (x R y) ∨ (∃z:T. ((x R+ z) ∧ (z R y)))

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. n : ℤ
4. 0 < n
5. ∀x,y:T.  ((x R^n y) ⇒ ((x R y) ∨ (∃z:T. ((x R+ z) ∧ (z R y)))))
6. x : T
7. y : T
8. x R^n + 1 y
⊢ (x R y) ∨ (∃z:T. ((x R+ z) ∧ (z R y)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    ((x  R\msupplus{}  y)  {}\mRightarrow{}  ((x  R  y)  \mvee{}  (\mexists{}z:T.  ((x  R\msupplus{}  z)  \mwedge{}  (z  R  y)))))


By

---

Latex:
(Auto
  THEN  (Unfold  `rel\_plus`  (-1))
  THEN  (Reduce  (-1))
  THEN  ExRepD
  THEN  (MoveToConcl  (-1))
  THEN  (MoveToConcl  (-2))
  THEN  (MoveToConcl  (-2))
  THEN  (NatPlusInd  (-1))
  THEN  Auto)

---

Home Index