Step * 1 of Lemma evalall-atom1


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


Latex:


Latex:

1.  x  :  Atom1
\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\_callbyvalueAtom1  THEN  Auto))
  THEN  Repeat  (HVimplies  0  [2])
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}isatom1(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)




Home Index