---

Step * 2 of Lemma rel_plus-weak-TI


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. weak-TI(T;x,y.R+ x y;x.Q[x])
4. Q : T ⟶ ℙ
⊢ weak-TI(T;x,y.R[x;y];x.Q[x])
BY
{ (D 0 THEN Auto THEN BackThruHyp' 3 THEN Auto THEN BackThruHyp' 5 THEN Auto THEN BackThruSomeHyp) }

1
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

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  weak-TI(T;x,y.R\msupplus{}  x  y;x.Q[x])
4.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
\mvdash{}  weak-TI(T;x,y.R[x;y];x.Q[x])


By

---

Latex:
(D  0  THEN  Auto  THEN  BackThruHyp'  3  THEN  Auto  THEN  BackThruHyp'  5  THEN  Auto  THEN  BackThruSomeHyp)

---

Home Index