---

Step * 1 2 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
⊢ let G,g = a in G fix(g) ∈ partial(E) = let G,g = b in G fix(g) ∈ partial(E) ∈ Type
BY
{ (AutoPairEta [2;1] 0 THEN AutoPairEta [3;1] 0 THEN EqCD THEN Auto THEN (BLemma `base-equal-partial` THENA 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
⊢ value-type(E)

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
⊢ ((((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))))↓)
∧ (¬is-exception((fst(a)) fix((snd(a)))))
∧ (¬is-exception((fst(b)) fix((snd(b)))))

---

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{}  let  G,g  =  a  in  G  fix(g)  \mmember{}  partial(E)  =  let  G,g  =  b  in  G  fix(g)  \mmember{}  partial(E)


By

---

Latex:
(AutoPairEta  [2;1]  0
  THEN  AutoPairEta  [3;1]  0
  THEN  EqCD
  THEN  Auto
  THEN  (BLemma  `base-equal-partial`  THENA  Auto))\mcdot{}

---

Home Index