---

Step * of Lemma has-value-equality-fix

∀[T,E,S:Type].  ∀[G:T ⟶ partial(E)]. ∀[g:T ⟶ T].  ((G fix(g))↓ ∈ ℙ) supposing value-type(E) ∧ (⊥ ∈ T)
BY
{ ((UnivCD THENA (Try (Complete (Auto)) THEN MemCD THEN Try (BLemma `bottom-member-prop`) THEN Auto))
   THEN (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 AllReduce
   THEN (Assert ⌜(fst(a) ∈ T ⟶ partial(E)) ∧ (fst(b) ∈ T ⟶ partial(E)) ∧ (snd(a) ∈ T ⟶ T) ∧ (snd(b) ∈ T ⟶ T)⌝⋅
         THENA Auto
         )
   THEN EqCDA)⋅ }

1
.....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))))↓ ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[T,E,S:Type].
    \mforall{}[G:T  {}\mrightarrow{}  partial(E)].  \mforall{}[g:T  {}\mrightarrow{}  T].    ((G  fix(g))\mdownarrow{}  \mmember{}  \mBbbP{})  supposing  value-type(E)  \mwedge{}  (\mbot{}  \mmember{}  T)


By

---

Latex:
((UnivCD  THENA  (Try  (Complete  (Auto))  THEN  MemCD  THEN  Try  (BLemma  `bottom-member-prop`)  THEN  Auto))
  THEN  (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  AllReduce
  THEN  (Assert  \mkleeneopen{}(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)\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  EqCDA)\mcdot{}

---

Home Index