---

Step * of Lemma least-equiv-implies

∀[A:Type]. ∀[R,E:A ⟶ A ⟶ ℙ].  (R => E ⇒ EquivRel(A;x,y.E x y) ⇒ least-equiv(A;R) => E)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``least-equiv transitive-reflexive-closure`` -1
   THEN D -1
   THEN Try ((RWO  "-1" 0 THEN Auto))
   THEN InstLemma `transitive-closure-induction` [⌜A⌝;⌜λ2y.x E y⌝;⌜λx,y. ((R x y) ∨ (R y x))⌝;⌜x⌝;⌜y⌝]⋅
   THEN Auto) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. [E] : A ⟶ A ⟶ ℙ
4. R => E
5. EquivRel(A;x,y.E x y)
6. x : A
7. y : A
8. TC(λx,y. ((R x y) ∨ (R y x))) x y
9. x@0 : A
10. y1 : A
11. x@0 (λx,y. ((R x y) ∨ (R y x))) y1
12. x E x@0
⊢ x E y1

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R,E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R  =>  E  {}\mRightarrow{}  EquivRel(A;x,y.E  x  y)  {}\mRightarrow{}  least-equiv(A;R)  =>  E)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``least-equiv  transitive-reflexive-closure``  -1
  THEN  D  -1
  THEN  Try  ((RWO    "-1"  0  THEN  Auto))
  THEN  InstLemma  `transitive-closure-induction`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}y.x  E  y\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  ((R  x  y)  \mvee{}  (R  y  x))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\000C\mcdot{}
  THEN  Auto)

---

Home Index