---

Step * 1 1 1 1 of Lemma es-causle-retraction-squash


1. es : EO@i'
2. [T] : Type
3. strong-subtype(T;E)
4. f : T ─→ T@i
5. ∀x:T. f x c≤ x@i
6. f1 : E ─→ ℕ
7. ∀e,e':E.  ((e < e') ⇒ f1 e < f1 e')
8. x : T@i
⊢ ((f x) = x ∈ T) ∨ f1 (f x) < f1 x
BY
{ ((InstHyp [⌈x⌉] 5⋅ THENA Auto) THEN D -1) }

1
1. es : EO@i'
2. [T] : Type
3. strong-subtype(T;E)
4. f : T ─→ T@i
5. ∀x:T. f x c≤ x@i
6. f1 : E ─→ ℕ
7. ∀e,e':E.  ((e < e') ⇒ f1 e < f1 e')
8. x : T@i
9. (f x < x)
⊢ ((f x) = x ∈ T) ∨ f1 (f x) < f1 x

2
1. es : EO@i'
2. [T] : Type
3. strong-subtype(T;E)
4. f : T ─→ T@i
5. ∀x:T. f x c≤ x@i
6. f1 : E ─→ ℕ
7. ∀e,e':E.  ((e < e') ⇒ f1 e < f1 e')
8. x : T@i
9. (f x) = x ∈ E
⊢ ((f x) = x ∈ T) ∨ f1 (f x) < f1 x

---

Latex:



1.  es  :  EO@i'
2.  [T]  :  Type
3.  strong-subtype(T;E)
4.  f  :  T  {}\mrightarrow{}  T@i
5.  \mforall{}x:T.  f  x  c\mleq{}  x@i
6.  f1  :  E  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}e,e':E.    ((e  <  e')  {}\mRightarrow{}  f1  e  <  f1  e')
8.  x  :  T@i
\mvdash{}  ((f  x)  =  x)  \mvee{}  f1  (f  x)  <  f1  x


By

((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index