---

Step * of Lemma rel_plus_functionality_wrt_rel_implies

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1+ => R2+)
BY
{ (Unfolds ``rel_plus rel_implies`` 0
   THEN Reduce 0
   THEN Auto
   THEN (ParallelOp (-1))
   THEN (MoveToConcl (-1))
   THEN (MoveToConcl (-2))
   THEN (MoveToConcl (-2))
   THEN (All (Fold `rel_implies`))) }

1
1. [T] : Type
2. [R1] : T ⟶ T ⟶ ℙ
3. [R2] : T ⟶ T ⟶ ℙ
4. R1 => R2@i
5. n : ℕ+@i
⊢ R1^n => R2^n

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  R1\msupplus{}  =>  R2\msupplus{})


By

---

Latex:
(Unfolds  ``rel\_plus  rel\_implies``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  (ParallelOp  (-1))
  THEN  (MoveToConcl  (-1))
  THEN  (MoveToConcl  (-2))
  THEN  (MoveToConcl  (-2))
  THEN  (All  (Fold  `rel\_implies`)))

---

Home Index