---

Step * of Lemma transitive-closure-induction

∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[R:A ⟶ A ⟶ ℙ].
  ((∀x,y:A.  ((x R y) ⇒ P[x] ⇒ P[y])) ⇒ (∀x,y:A.  ((x TC(R) y) ⇒ P[x] ⇒ P[y])))
BY
{ TACTIC:(Auto THEN (InstLemma `transitive-closure-minimal` [⌜A⌝;⌜R⌝;⌜λx,y. (P[x] ⇒ P[y])⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
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]
⊢ Trans(A;x,y.x (λx,y. (P[x] ⇒ P[y])) y)

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:A.    ((x  R  y)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y]))  {}\mRightarrow{}  (\mforall{}x,y:A.    ((x  TC(R)  y)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y])))


By

---

Latex:
TACTIC:(Auto  THEN  (InstLemma  `transitive-closure-minimal`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (P[x]  {}\mRightarrow{}  P[y])\mkleeneclose{}]\mcdot{}  THENA  Au\000Cto))

---

Home Index