---

Step * of Lemma rel-preserving-star-reachable

No Annotations
∀[T1,T2:Type]. ∀[i2:T2]. ∀[R1:T1 ⟶ T1 ⟶ Type]. ∀[R2:T2 ⟶ T2 ⟶ Type].
  ∀f:T2 ⟶ T1
    ((∀x,y:{s:T2| i2 (R2^*) s} .  ((x R2 y) ⇒ ((f x) (R1^*) (f y))))
    ⇒ {∀x,y:{s:T2| i2 (R2^*) s} .  ((x (R2^*) y) ⇒ ((f x) (R1^*) (f y)))})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN All (Unfold `rel-preserving`)
   THEN Auto
   THEN (Unfolds ``infix_ap rel_star`` -1 THEN Reduce (-1))
   THEN ExRepD) }

1
1. [T1] : Type
2. [T2] : Type
3. [i2] : T2
4. [R1] : T1 ⟶ T1 ⟶ Type
5. [R2] : T2 ⟶ T2 ⟶ Type
6. f : T2 ⟶ T1
7. ∀x,y:{s:T2| i2 (R2^*) s} .  ((x R2 y) ⇒ ((f x) (R1^*) (f y)))
8. x : {s:T2| i2 (R2^*) s} 
9. y : {s:T2| i2 (R2^*) s} 
10. n : ℕ
11. x R2^n y
⊢ (f x) (R1^*) (f y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T1,T2:Type].  \mforall{}[i2:T2].  \mforall{}[R1:T1  {}\mrightarrow{}  T1  {}\mrightarrow{}  Type].  \mforall{}[R2:T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  Type].
    \mforall{}f:T2  {}\mrightarrow{}  T1
        ((\mforall{}x,y:\{s:T2|  i2  rel\_star(T2;  R2)  s\}  .    ((x  R2  y)  {}\mRightarrow{}  ((f  x)  rel\_star(T1;  R1)  (f  y))))
        {}\mRightarrow{}  \{\mforall{}x,y:\{s:T2|  i2  (R2\^{}*)  s\}  .
                    ((x  (R2\^{}*)  y)  {}\mRightarrow{}  ((f  x)  (R1\^{}*)  (f  y)))\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  All  (Unfold  `rel-preserving`)
  THEN  Auto
  THEN  (Unfolds  ``infix\_ap  rel\_star``  -1  THEN  Reduce  (-1))
  THEN  ExRepD)

---

Home Index