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