---

Step * 1 2 2 1 of Lemma fixpoint-induction-bottom


1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
⊢ (((fst(a)) fix((snd(a))))↓ ⇐⇒ ((fst(b)) fix((snd(b))))↓)
∧ ((fst(a)) fix((snd(a)))) = ((fst(b)) fix((snd(b)))) ∈ E supposing ((fst(a)) fix((snd(a))))↓
BY
{ (((RepeatFor 2 (D 0) THENM Try (D 0)) THENA (Try (UniverseIsType) THEN BLemma `has-value_wf_base` THEN Auto))
   THEN (Compactness (-1) THEN Unhide THEN Auto)⋅
   ) }

1
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
13. ((fst(a)) fix((snd(a))))↓
14. j : ℕ
15. ((fst(a)) (snd(a)^j ⊥))↓
⊢ ((fst(b)) fix((snd(b))))↓

2
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
13. ((fst(b)) fix((snd(b))))↓
14. j : ℕ
15. ((fst(b)) (snd(b)^j ⊥))↓
⊢ ((fst(a)) fix((snd(a))))↓

3
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
13. ((fst(a)) fix((snd(a))))↓
14. j : ℕ
15. ((fst(a)) (snd(a)^j ⊥))↓
⊢ ((fst(a)) fix((snd(a)))) = ((fst(b)) fix((snd(b)))) ∈ E

---

Latex:

---

Latex:

1.  E  :  Type
2.  S  :  Type
3.  value-type(E)
4.  mono(E)
5.  \mbot{}  \mmember{}  S
6.  a  :  Base
7.  b  :  Base
8.  c  :  a  =  b
9.  fst(a)  \mmember{}  S  {}\mrightarrow{}  partial(E)
10.  fst(b)  \mmember{}  S  {}\mrightarrow{}  partial(E)
11.  snd(a)  \mmember{}  S  {}\mrightarrow{}  S
12.  snd(b)  \mmember{}  S  {}\mrightarrow{}  S
\mvdash{}  (((fst(a))  fix((snd(a))))\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  ((fst(b))  fix((snd(b))))\mdownarrow{})
\mwedge{}  ((fst(a))  fix((snd(a))))  =  ((fst(b))  fix((snd(b))))  supposing  ((fst(a))  fix((snd(a))))\mdownarrow{}


By

---

Latex:
(((RepeatFor  2  (D  0)  THENM  Try  (D  0))
    THENA  (Try  (UniverseIsType)  THEN  BLemma  `has-value\_wf\_base`  THEN  Auto)
    )
  THEN  (Compactness  (-1)  THEN  Unhide  THEN  Auto)\mcdot{}
  )

---

Home Index