---

Step * of Lemma rel_plus-weak-TI

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (∀Q:T ⟶ ℙ. weak-TI(T;x,y.R[x;y];x.Q[x]) ⇐⇒ ∀Q:T ⟶ ℙ. weak-TI(T;x,y.R+ x y;x.Q[x]))
BY
{ 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 ⟶ ℙ
⊢ weak-TI(T;x,y.R+ x y;x.Q[x])

2
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])

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  weak-TI(T;x,y.R[x;y];x.Q[x])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  weak-TI(T;x,y.R\msupplus{}  x  y;x.Q[x]))


By

---

Latex:
Auto

---

Home Index