---

Step * 1 of Lemma fixpoint-induction-bottom


1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. G : S ⟶ partial(E)
7. g : S ⟶ S
⊢ G fix(g) ∈ partial(E)
BY
{ ((Assert ⌜(λp.let G,g = p in G fix(g) ∈ partial(E)) <G, g>⌝⋅ THENM (Reduce (-1) THEN Auto))
   THEN GenConclAtAddr [2]
   THEN Thin (-1)
   THEN ThinVars [`G';`g']⋅
   THEN PointwiseFunctionality (-1)
   THEN Reduce 0
   THEN (Assert ⌜(fst(a) ∈ S ⟶ partial(E)) ∧ (fst(b) ∈ S ⟶ partial(E)) ∧ (snd(a) ∈ S ⟶ S) ∧ (snd(b) ∈ S ⟶ S)⌝⋅
         THENA (EqHD (-1) THEN Auto)
         )
   THEN RepD)⋅ }

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
⊢ let G,g = a 
  in G fix(g) ∈ partial(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
⊢ let G,g = a in G fix(g) ∈ partial(E) = let G,g = b in G fix(g) ∈ partial(E) ∈ Type

---

Latex:

---

Latex:

1.  E  :  Type
2.  S  :  Type
3.  value-type(E)
4.  mono(E)
5.  \mbot{}  \mmember{}  S
6.  G  :  S  {}\mrightarrow{}  partial(E)
7.  g  :  S  {}\mrightarrow{}  S
\mvdash{}  G  fix(g)  \mmember{}  partial(E)


By

---

Latex:
((Assert  \mkleeneopen{}(\mlambda{}p.let  G,g  =  p  in  G  fix(g)  \mmember{}  partial(E))  <G,  g>\mkleeneclose{}\mcdot{}  THENM  (Reduce  (-1)  THEN  Auto))
  THEN  GenConclAtAddr  [2]
  THEN  Thin  (-1)
  THEN  ThinVars  [`G';`g']\mcdot{}
  THEN  PointwiseFunctionality  (-1)
  THEN  Reduce  0
  THEN  (Assert  \mkleeneopen{}(fst(a)  \mmember{}  S  {}\mrightarrow{}  partial(E))
                              \mwedge{}  (fst(b)  \mmember{}  S  {}\mrightarrow{}  partial(E))
                              \mwedge{}  (snd(a)  \mmember{}  S  {}\mrightarrow{}  S)
                              \mwedge{}  (snd(b)  \mmember{}  S  {}\mrightarrow{}  S)\mkleeneclose{}\mcdot{}
              THENA  (EqHD  (-1)  THEN  Auto)
              )
  THEN  RepD)\mcdot{}

---

Home Index