---

Step * 1 of Lemma evalall-atom2


1. x : Atom2
⊢ if x is a pair then let a,b = x 
                      in eval a' = evalall(a) in
                         eval b' = evalall(b) in
                           <a', b'> otherwise if x is inl then eval y = evalall(outl(x)) in
                                                               inl y
                                              else if x is inr then eval y = evalall(outr(x)) in
                                                                    inr y 
                                                   else x
= x
∈ Atom2
BY
{ ((Assert ⌜(x)↓⌝⋅ THENA (Unfold `has-value` 0 THEN Refine_callbyvalueAtom2 THEN Auto))
   THEN Repeat (HVimplies 0 [2])
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN (Assert ⌜isatom2(x) ~ tt⌝⋅ THENA (Reduce 0 THEN Auto))
   THEN HypSubst (-2) (-1)
   THEN Reduce (-1)
   THEN InstLemma `not-btrue-sqeq-bfalse` []
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x  :  Atom2
\mvdash{}  if  x  is  a  pair  then  let  a,b  =  x 
                                            in  eval  a'  =  evalall(a)  in
                                                  eval  b'  =  evalall(b)  in
                                                      <a',  b'>  otherwise  if  x  is  inl  then  eval  y  =  evalall(outl(x))  in
                                                                                                                              inl  y
                                                                                            else  if  x  is  inr  then  eval  y  =  evalall(outr(x))  in
                                                                                                                                        inr  y 
                                                                                                      else  x
=  x


By

---

Latex:
((Assert  \mkleeneopen{}(x)\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  (Unfold  `has-value`  0  THEN  Refine\_callbyvalueAtom2  THEN  Auto))
  THEN  Repeat  (HVimplies  0  [2])
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}isatom2(x)  \msim{}  tt\mkleeneclose{}\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  HypSubst  (-2)  (-1)
  THEN  Reduce  (-1)
  THEN  InstLemma  `not-btrue-sqeq-bfalse`  []
  THEN  Auto)\mcdot{}

---

Home Index