---

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


1. T : Type
2. E : Type
3. S : Type
4. value-type(E) ∧ (⊥ ∈ T)
5. G : T ⟶ bar(E)
6. g : T ⟶ T
⊢ (G fix(g))↓ ∈ ℙ
BY
{ ((Assert ⌜(λp.let G,g = p in (G fix(g))↓ ∈ ℙ) <G, g>⌝⋅ THENM (Reduce (-1) THEN Trivial))
   THEN (GenConclTerm ⌜<G, g>⌝⋅ THENA Auto)
   THEN ThinVar `G'
   THEN ThinVar `g'
   THEN PointwiseFunctionality (-1)
   THEN Try (Complete (AutoPairEta [2] 0))
   THEN AutoPairEta [2;2] 0
   THEN AutoPairEta [3;1] 0
   THEN AutoPairEta [2] (-1)
   THEN AutoPairEta [3] (-1)
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN (Assert ⌜(fst(a) ∈ T ⟶ bar(E)) ∧ (fst(b) ∈ T ⟶ bar(E)) ∧ (snd(a) ∈ T ⟶ T) ∧ (snd(b) ∈ T ⟶ T)⌝⋅ THENA Auto)
   THEN EqCD
   THEN Auto
   THEN (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)
         )) }

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 ⟶ bar(E))
9. (snd(a)) = (snd(b)) ∈ (T ⟶ T)
10. fst(a) ∈ T ⟶ bar(E)
11. fst(b) ∈ T ⟶ bar(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 ⟶ bar(E))
9. (snd(a)) = (snd(b)) ∈ (T ⟶ T)
10. fst(a) ∈ T ⟶ bar(E)
11. fst(b) ∈ T ⟶ bar(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:

1.  T  :  Type
2.  E  :  Type
3.  S  :  Type
4.  value-type(E)  \mwedge{}  (\mbot{}  \mmember{}  T)
5.  G  :  T  {}\mrightarrow{}  bar(E)
6.  g  :  T  {}\mrightarrow{}  T
\mvdash{}  (G  fix(g))\mdownarrow{}  \mmember{}  \mBbbP{}


By

---

Latex:
((Assert  \mkleeneopen{}(\mlambda{}p.let  G,g  =  p  in  (G  fix(g))\mdownarrow{}  \mmember{}  \mBbbP{})  <G,  g>\mkleeneclose{}\mcdot{}  THENM  (Reduce  (-1)  THEN  Trivial))
  THEN  (GenConclTerm  \mkleeneopen{}<G,  g>\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `G'
  THEN  ThinVar  `g'
  THEN  PointwiseFunctionality  (-1)
  THEN  Try  (Complete  (AutoPairEta  [2]  0))
  THEN  AutoPairEta  [2;2]  0
  THEN  AutoPairEta  [3;1]  0
  THEN  AutoPairEta  [2]  (-1)
  THEN  AutoPairEta  [3]  (-1)
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  (Assert  \mkleeneopen{}(fst(a)  \mmember{}  T  {}\mrightarrow{}  bar(E))
                              \mwedge{}  (fst(b)  \mmember{}  T  {}\mrightarrow{}  bar(E))
                              \mwedge{}  (snd(a)  \mmember{}  T  {}\mrightarrow{}  T)
                              \mwedge{}  (snd(b)  \mmember{}  T  {}\mrightarrow{}  T)\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  EqCD
  THEN  Auto
  THEN  (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)
              ))

---

Home Index