Step
*
2
of Lemma
transitive-closure-induction
1. [A] : Type
2. [P] : A ⟶ ℙ
3. [R] : A ⟶ A ⟶ ℙ
4. ∀x,y:A. ((x R y)
⇒ P[x]
⇒ P[y])
5. x : A
6. y : A
7. x TC(R) y
8. P[x]
9. TC(R) => λx,y. (P[x]
⇒ P[y])
⊢ P[y]
BY
{ ((With ⌜x⌝ (D (-1))⋅ THEN Reduce (-1)) THEN Auto) }
Latex:
Latex:
1. [A] : Type
2. [P] : A {}\mrightarrow{} \mBbbP{}
3. [R] : A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}
4. \mforall{}x,y:A. ((x R y) {}\mRightarrow{} P[x] {}\mRightarrow{} P[y])
5. x : A
6. y : A
7. x TC(R) y
8. P[x]
9. TC(R) => \mlambda{}x,y. (P[x] {}\mRightarrow{} P[y])
\mvdash{} P[y]
By
Latex:
((With \mkleeneopen{}x\mkleeneclose{} (D (-1))\mcdot{} THEN Reduce (-1)) THEN Auto)
Home
Index