---

Step * 1 2 2 1 3 1 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
13. j : ℕ
14. ((fst(a)) (snd(a)^j ⊥))↓
15. (snd(a)^j ⊥) = (snd(b)^j ⊥) ∈ S
16. ((fst(a)) (snd(a)^j ⊥)) = ((fst(b)) (snd(b)^j ⊥)) ∈ partial(E)
17. ((fst(b)) (snd(b)^j ⊥))↓
⊢ ((fst(a)) fix((snd(a)))) = ((fst(b)) fix((snd(b)))) ∈ E
BY
{ ((Assert ⌜(fst(a)) (snd(a)^j ⊥) ∈ E⌝⋅ THENA (BLemma `termination` THEN Auto))
   THEN (Assert ⌜(fst(b)) (snd(b)^j ⊥) ∈ E⌝⋅ THENA (BLemma `termination` THEN Auto))
   THEN (Assert ⌜((fst(a)) (snd(a)^j ⊥)) = ((fst(a)) fix((snd(a)))) ∈ E⌝⋅
         THENA (UnfoldTopAb 4
                THEN BHyp 4
                THEN Auto
                THEN UnfoldTopAb 0
                THEN InstConcl [⌜(fst(a)) (snd(a)^j ⊥)⌝]⋅
                THEN Try (Complete (Auto))
                THEN Try ((MemCD THEN Try (BLemma `equal-wf-base`) THEN Auto))
                THEN Auto
                THEN BLemma `fixpoint_ub`
                THEN Auto)
         )
   THEN (Assert ⌜((fst(b)) (snd(b)^j ⊥)) = ((fst(b)) fix((snd(b)))) ∈ E⌝⋅
         THENA (UnfoldTopAb 4
                THEN BHyp 4
                THEN Auto
                THEN UnfoldTopAb 0
                THEN InstConcl [⌜(fst(b)) (snd(b)^j ⊥)⌝]⋅
                THEN Try (Complete (Auto))
                THEN Try ((MemCD THEN Try (BLemma `equal-wf-base`) THEN Auto))
                THEN Auto
                THEN BLemma `fixpoint_ub`
                THEN Auto)
         )
   THEN (RevHypSubst (-1) 0 THENA Auto)
   THEN (RevHypSubst (-2) 0 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
13. j : ℕ
14. ((fst(a)) (snd(a)^j ⊥))↓
15. (snd(a)^j ⊥) = (snd(b)^j ⊥) ∈ S
16. ((fst(a)) (snd(a)^j ⊥)) = ((fst(b)) (snd(b)^j ⊥)) ∈ partial(E)
17. ((fst(b)) (snd(b)^j ⊥))↓
18. (fst(a)) (snd(a)^j ⊥) ∈ E
19. (fst(b)) (snd(b)^j ⊥) ∈ E
20. ((fst(a)) (snd(a)^j ⊥)) = ((fst(a)) fix((snd(a)))) ∈ E
21. ((fst(b)) (snd(b)^j ⊥)) = ((fst(b)) fix((snd(b)))) ∈ E
⊢ ((fst(a)) (snd(a)^j ⊥)) = ((fst(b)) (snd(b)^j ⊥)) ∈ 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
13.  j  :  \mBbbN{}
14.  ((fst(a))  (snd(a)\^{}j  \mbot{}))\mdownarrow{}
15.  (snd(a)\^{}j  \mbot{})  =  (snd(b)\^{}j  \mbot{})
16.  ((fst(a))  (snd(a)\^{}j  \mbot{}))  =  ((fst(b))  (snd(b)\^{}j  \mbot{}))
17.  ((fst(b))  (snd(b)\^{}j  \mbot{}))\mdownarrow{}
\mvdash{}  ((fst(a))  fix((snd(a))))  =  ((fst(b))  fix((snd(b))))


By

---

Latex:
((Assert  \mkleeneopen{}(fst(a))  (snd(a)\^{}j  \mbot{})  \mmember{}  E\mkleeneclose{}\mcdot{}  THENA  (BLemma  `termination`  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}(fst(b))  (snd(b)\^{}j  \mbot{})  \mmember{}  E\mkleeneclose{}\mcdot{}  THENA  (BLemma  `termination`  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}((fst(a))  (snd(a)\^{}j  \mbot{}))  =  ((fst(a))  fix((snd(a))))\mkleeneclose{}\mcdot{}
              THENA  (UnfoldTopAb  4
                            THEN  BHyp  4
                            THEN  Auto
                            THEN  UnfoldTopAb  0
                            THEN  InstConcl  [\mkleeneopen{}(fst(a))  (snd(a)\^{}j  \mbot{})\mkleeneclose{}]\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  Try  ((MemCD  THEN  Try  (BLemma  `equal-wf-base`)  THEN  Auto))
                            THEN  Auto
                            THEN  BLemma  `fixpoint\_ub`
                            THEN  Auto)
              )
  THEN  (Assert  \mkleeneopen{}((fst(b))  (snd(b)\^{}j  \mbot{}))  =  ((fst(b))  fix((snd(b))))\mkleeneclose{}\mcdot{}
              THENA  (UnfoldTopAb  4
                            THEN  BHyp  4
                            THEN  Auto
                            THEN  UnfoldTopAb  0
                            THEN  InstConcl  [\mkleeneopen{}(fst(b))  (snd(b)\^{}j  \mbot{})\mkleeneclose{}]\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  Try  ((MemCD  THEN  Try  (BLemma  `equal-wf-base`)  THEN  Auto))
                            THEN  Auto
                            THEN  BLemma  `fixpoint\_ub`
                            THEN  Auto)
              )
  THEN  (RevHypSubst  (-1)  0  THENA  Auto)
  THEN  (RevHypSubst  (-2)  0  THENA  Auto))\mcdot{}

---

Home Index