Step * of Lemma evalall-atom2

[x:Atom2]. (evalall(x) x)
BY
(Auto
   THEN RW (AddrC [2] (RecUnfoldC `evalall`)) 0
   THEN (CallByValueReduce THENA (Unfold `has-value` THEN Refine_callbyvalueAtom2 THEN Auto))) }

1
1. Atom2
⊢ 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
∈ Atom2


Latex:


Latex:
\mforall{}[x:Atom2].  (evalall(x)  \msim{}  x)


By


Latex:
(Auto
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `evalall`))  0
  THEN  (CallByValueReduce  0  THENA  (Unfold  `has-value`  0  THEN  Refine\_callbyvalueAtom2  THEN  Auto)))




Home Index