---

Step * of Lemma least-equiv-induction

∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[R:A ⟶ A ⟶ ℙ].
  ((∀x,y:A.  ((x R y) ⇒ (P[x] ⇐⇒ P[y]))) ⇒ (∀x,y:A.  ((x least-equiv(A;R) y) ⇒ P[x] ⇒ P[y])))
BY
{ (Auto
   THEN All (Unfold `infix_ap`)
   THEN RepUR ``least-equiv transitive-reflexive-closure`` -2
   THEN D -2
   THEN Auto
   THEN InstLemma `transitive-closure-induction` 
   [⌜A⌝;⌜P⌝;⌜λx,y. ((R x y) ∨ (R y x))⌝;⌜x⌝;⌜y⌝]⋅
   THEN Auto) }

1
1. [A] : Type
2. [P] : A ⟶ ℙ
3. [R] : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((R x y) ⇒ (P[x] ⇐⇒ P[y]))
5. x : A
6. y : A
7. TC(λx,y. ((R x y) ∨ (R y x))) x y
8. P[x]
9. x1 : A
10. y1 : A
11. x1 (λx,y. ((R x y) ∨ (R y x))) y1
12. P[x1]
⊢ P[y1]

---

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]  \mLeftarrow{}{}\mRightarrow{}  P[y])))  {}\mRightarrow{}  (\mforall{}x,y:A.    ((x  least-equiv(A;R)  y)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y])))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `infix\_ap`)
  THEN  RepUR  ``least-equiv  transitive-reflexive-closure``  -2
  THEN  D  -2
  THEN  Auto
  THEN  InstLemma  `transitive-closure-induction` 
  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  ((R  x  y)  \mvee{}  (R  y  x))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index