---

Step * 1 of Lemma has-value-equality-fix

.....subterm..... T:t
2:n
1. T : Type
2. E : Type
3. S : Type
4. value-type(E) ∧ (⊥ ∈ T)
5. a : Base
6. b : Base
7. (fst(a)) = (fst(b)) ∈ (T ⟶ partial(E))
8. (snd(a)) = (snd(b)) ∈ (T ⟶ T)
9. (fst(a) ∈ T ⟶ partial(E)) ∧ (fst(b) ∈ T ⟶ partial(E)) ∧ (snd(a) ∈ T ⟶ T) ∧ (snd(b) ∈ T ⟶ T)
⊢ ((fst(a)) fix((snd(a))))↓ = ((fst(b)) fix((snd(b))))↓ ∈ ℙ
BY
{ ((BLemma `has-value-extensionality` THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA (GenConclAtAddrType ⌜Base⌝ [1;1]⋅ THEN Auto))
   THEN Compactness (-1)
   THEN SqUnhide
   THEN (Assert ⌜(snd(a)^j ⊥) = (snd(b)^j ⊥) ∈ T⌝⋅
         THENA (Thin (-1)
                THEN NatInd (-1)
                THEN Reduce 0
                THEN Auto
                THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
                THEN Reduce 0
                THEN Auto)
         )
   THEN ExRepD) }

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

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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  T  :  Type
2.  E  :  Type
3.  S  :  Type
4.  value-type(E)  \mwedge{}  (\mbot{}  \mmember{}  T)
5.  a  :  Base
6.  b  :  Base
7.  (fst(a))  =  (fst(b))
8.  (snd(a))  =  (snd(b))
9.  (fst(a)  \mmember{}  T  {}\mrightarrow{}  partial(E))  \mwedge{}  (fst(b)  \mmember{}  T  {}\mrightarrow{}  partial(E))  \mwedge{}  (snd(a)  \mmember{}  T  {}\mrightarrow{}  T)  \mwedge{}  (snd(b)  \mmember{}  T  {}\mrightarrow{}  T)
\mvdash{}  ((fst(a))  fix((snd(a))))\mdownarrow{}  =  ((fst(b))  fix((snd(b))))\mdownarrow{}


By

---

Latex:
((BLemma  `has-value-extensionality`  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  (GenConclAtAddrType  \mkleeneopen{}Base\mkleeneclose{}  [1;1]\mcdot{}  THEN  Auto))
  THEN  Compactness  (-1)
  THEN  SqUnhide
  THEN  (Assert  \mkleeneopen{}(snd(a)\^{}j  \mbot{})  =  (snd(b)\^{}j  \mbot{})\mkleeneclose{}\mcdot{}
              THENA  (Thin  (-1)
                            THEN  NatInd  (-1)
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  Auto)
              )
  THEN  ExRepD)

---

Home Index