---

Step * 1 1 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 ⟶ ℙ
5. ∀x:T. ((∀s:T. ((R+ x s) ⇒ Q[s])) ⇒ Q[x])
⊢ ∀x:T. Q[x]
BY
{ ((InstHyp [⌜λ2x.(∀s:T. ((R+ x s) ⇒ Q[s])) ∧ Q[x]⌝] 3⋅ THENA Auto) THEN D -1 THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. weak-TI(T;x,y.R[x;y];x.Q[x])
4. Q : T ⟶ ℙ
5. ∀x:T. ((∀s:T. ((R+ x s) ⇒ Q[s])) ⇒ Q[x])
6. x : T
7. ∀s@0:T. (R[x;s@0] ⇒ ((∀s:T. ((R+ s@0 s) ⇒ Q[s])) ∧ Q[s@0]))
8. s : T
9. R+ x s
⊢ Q[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[x;y];x.Q[x])
4.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:T.  ((\mforall{}s:T.  ((R\msupplus{}  x  s)  {}\mRightarrow{}  Q[s]))  {}\mRightarrow{}  Q[x])
\mvdash{}  \mforall{}x:T.  Q[x]


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x.(\mforall{}s:T.  ((R\msupplus{}  x  s)  {}\mRightarrow{}  Q[s]))  \mwedge{}  Q[x]\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index