Step
*
1
1
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])
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. y : T
10. x R y
11. y (R^*) s
⊢ Q[s]
BY
{ (InstHyp [⌜y⌝] (-5)⋅ THENA 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. y : T
10. x R y
11. y (R^*) s
12. (∀s:T. ((R+ y s) 
⇒ Q[s])) ∧ Q[y]
⊢ 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])
6.  x  :  T
7.  \mforall{}s@0:T.  (R[x;s@0]  {}\mRightarrow{}  ((\mforall{}s:T.  ((R\msupplus{}  s@0  s)  {}\mRightarrow{}  Q[s]))  \mwedge{}  Q[s@0]))
8.  s  :  T
9.  y  :  T
10.  x  R  y
11.  y  rel\_star(T;  R)  s
\mvdash{}  Q[s]
By
Latex:
(InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
Home
Index