Step
*
2
1
of Lemma
retraction-fun-path-squash
1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (↓((f x) = x ∈ T) ∨ h (f x) < h x)
5. u : T
6. v : T List
7. ∀x,y:T. ↓(x = y ∈ T) ∨ h y < h x supposing y=f*(x) via v
8. x : T
9. y : T
10. y = u ∈ T
11. ((u = (f hd(v)) ∈ T) ∧ (¬(u = hd(v) ∈ T))) ∧ hd(v)=f*(x) via v supposing 0 < ||v||
12. x = u ∈ T supposing ¬0 < ||v||
⊢ ↓(x = y ∈ T) ∨ h y < h x
BY
{ ((Decide ⌜0 < ||v||⌝⋅ THENA Auto) THEN ThinTrivial THEN Auto) }
1
1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (↓((f x) = x ∈ T) ∨ h (f x) < h x)
5. u : T
6. v : T List
7. ∀x,y:T. ↓(x = y ∈ T) ∨ h y < h x supposing y=f*(x) via v
8. x : T
9. y : T
10. y = u ∈ T
11. x = u ∈ T supposing ¬0 < ||v||
12. 0 < ||v||
13. u = (f hd(v)) ∈ T
14. ¬(u = hd(v) ∈ T)
15. hd(v)=f*(x) via v
⊢ ↓(x = y ∈ T) ∨ h y < h x
Latex:
Latex:
1. T : Type
2. f : T {}\mrightarrow{} T
3. h : T {}\mrightarrow{} \mBbbN{}
4. \mforall{}x:T. (\mdownarrow{}((f x) = x) \mvee{} h (f x) < h x)
5. u : T
6. v : T List
7. \mforall{}x,y:T. \mdownarrow{}(x = y) \mvee{} h y < h x supposing y=f*(x) via v
8. x : T
9. y : T
10. y = u
11. ((u = (f hd(v))) \mwedge{} (\mneg{}(u = hd(v)))) \mwedge{} hd(v)=f*(x) via v supposing 0 < ||v||
12. x = u supposing \mneg{}0 < ||v||
\mvdash{} \mdownarrow{}(x = y) \mvee{} h y < h x
By
Latex:
((Decide \mkleeneopen{}0 < ||v||\mkleeneclose{}\mcdot{} THENA Auto) THEN ThinTrivial THEN Auto)
Home
Index