---

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


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 
BY
{ (RepeatFor 2 ((HasValueImplies (-2) [1]
                 THEN Try (Complete ((HypSubst (-1) 0 THEN Reduce 0 THEN Auto)))
                 THEN HypSubst (-1) (-3)
                 THEN Thin (-1)))
   THEN BotDiv
   )⋅ }

---

Latex:

---

Latex:

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  \mbot{})\mdownarrow{}
4.  (t)\mdownarrow{}
\mvdash{}  if  ispair(t)  then  t  \msim{}  <fst(t),  snd(t)>  else  t  \msim{}  Ax  fi 


By

---

Latex:
(RepeatFor  2  ((HasValueImplies  (-2)  [1]
                              THEN  Try  (Complete  ((HypSubst  (-1)  0  THEN  Reduce  0  THEN  Auto)))
                              THEN  HypSubst  (-1)  (-3)
                              THEN  Thin  (-1)))
  THEN  BotDiv
  )\mcdot{}

---

Home Index