---

Step * 1 2 of Lemma has-value-equality-fix


1. T : Type
2. E : Type
3. S : Type
4. value-type(E)
5. ⊥ ∈ T
6. a : Base
7. b : Base
8. (fst(a)) = (fst(b)) ∈ (T ⟶ partial(E))
9. (snd(a)) = (snd(b)) ∈ (T ⟶ T)
10. fst(a) ∈ T ⟶ partial(E)
11. fst(b) ∈ T ⟶ partial(E)
12. snd(a) ∈ T ⟶ T
13. snd(b) ∈ T ⟶ T
14. ((fst(b)) fix((snd(b))))↓
15. j : ℕ
16. ((fst(b)) (snd(b)^j ⊥))↓
17. (snd(a)^j ⊥) = (snd(b)^j ⊥) ∈ T
⊢ ((fst(a)) fix((snd(a))))↓
BY
{ ((RevHypSubst (-1) (-2) THENA Auto)
   THEN (RevHypSubst (-10) (-2) THENA Auto)
   THEN (Assert ⌜(fst(a)) (snd(a)^j ⊥) ≤ (fst(a)) fix((snd(a)))⌝⋅ THENA (Auto THEN BLemma `fixpoint_ub` THEN Auto))
   THEN FLemma `has-value-monotonic` [-3;-1]
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  E  :  Type
3.  S  :  Type
4.  value-type(E)
5.  \mbot{}  \mmember{}  T
6.  a  :  Base
7.  b  :  Base
8.  (fst(a))  =  (fst(b))
9.  (snd(a))  =  (snd(b))
10.  fst(a)  \mmember{}  T  {}\mrightarrow{}  partial(E)
11.  fst(b)  \mmember{}  T  {}\mrightarrow{}  partial(E)
12.  snd(a)  \mmember{}  T  {}\mrightarrow{}  T
13.  snd(b)  \mmember{}  T  {}\mrightarrow{}  T
14.  ((fst(b))  fix((snd(b))))\mdownarrow{}
15.  j  :  \mBbbN{}
16.  ((fst(b))  (snd(b)\^{}j  \mbot{}))\mdownarrow{}
17.  (snd(a)\^{}j  \mbot{})  =  (snd(b)\^{}j  \mbot{})
\mvdash{}  ((fst(a))  fix((snd(a))))\mdownarrow{}


By

---

Latex:
((RevHypSubst  (-1)  (-2)  THENA  Auto)
  THEN  (RevHypSubst  (-10)  (-2)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(fst(a))  (snd(a)\^{}j  \mbot{})  \mleq{}  (fst(a))  fix((snd(a)))\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  BLemma  `fixpoint\_ub`  THEN  Auto)
              )
  THEN  FLemma  `has-value-monotonic`  [-3;-1]
  THEN  Auto)\mcdot{}

---

Home Index