---

Step * 2 1 of Lemma rel_plus-weak-TI


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. ((∀x:T. ((∀s:T. ((R+ x s) ⇒ Q[s])) ⇒ Q[x])) ⇒ (∀x:T. (Q x)))
4. Q : T ⟶ ℙ
5. ∀x:T. ((∀s:T. (R[x;s] ⇒ Q[s])) ⇒ Q[x])
6. x : T
7. x1 : T
8. ∀s:T. ((R+ x1 s) ⇒ Q[s])
9. s : T
10. R[x1;s]
⊢ R+ x1 s
BY
{ (BLemma `rel-rel-plus` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}x:T.  ((\mforall{}s:T.  ((R\msupplus{}  x  s)  {}\mRightarrow{}  Q[s]))  {}\mRightarrow{}  Q[x]))  {}\mRightarrow{}  (\mforall{}x:T.  (Q  x)))
4.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:T.  ((\mforall{}s:T.  (R[x;s]  {}\mRightarrow{}  Q[s]))  {}\mRightarrow{}  Q[x])
6.  x  :  T
7.  x1  :  T
8.  \mforall{}s:T.  ((R\msupplus{}  x1  s)  {}\mRightarrow{}  Q[s])
9.  s  :  T
10.  R[x1;s]
\mvdash{}  R\msupplus{}  x1  s


By

---

Latex:
(BLemma  `rel-rel-plus`  THEN  Auto)

---

Home Index