---

Step * of Lemma decomp-map-if-has-value

∀[t,f:Base].  if ispair(t) then t ~ <fst(t), snd(t)> else t ~ Ax fi  supposing (map(f;t))↓
BY
{ ((UnivCD THENA Auto)
   THEN (FLemma `has-value-if-has-value-map` [-1] THENA Auto)
   THEN Try (Complete ((BLemma `ispair-bool-if-has-value` THEN Auto)))
   THEN RepUR ``map`` (-2)
   THEN RecUnfold `list_ind` (-2)
   THEN HasValueD (-2)
   THEN Thin (-1)) }

1
1. t : Base
2. f : Base
3. (if t is a pair then let h,t = t 
                        in [f h / rec-case(t) of [] => [] | h::t => r.[f h / r]]
    otherwise if t = Ax then [] otherwise ⊥)↓
4. (t)↓
⊢ if ispair(t) then t ~ <fst(t), snd(t)> else t ~ Ax fi 

---

Latex:

---

Latex:
\mforall{}[t,f:Base].    if  ispair(t)  then  t  \msim{}  <fst(t),  snd(t)>  else  t  \msim{}  Ax  fi    supposing  (map(f;t))\mdownarrow{}


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (FLemma  `has-value-if-has-value-map`  [-1]  THENA  Auto)
  THEN  Try  (Complete  ((BLemma  `ispair-bool-if-has-value`  THEN  Auto)))
  THEN  RepUR  ``map``  (-2)
  THEN  RecUnfold  `list\_ind`  (-2)
  THEN  HasValueD  (-2)
  THEN  Thin  (-1))

---

Home Index