---

Step * 1 1 1 of Lemma evalall-evalall


1. t : Base
2. is-exception(evalall(evalall(t)))
3. u : Base
4. v : Base
5. exception(u; v) ≤ evalall(evalall(t))
6. exception(u; v) ≤ eval x = evalall(t) in
                     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
7. is-exception(eval x = evalall(t) in
                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)
8. (evalall(t))↓
⊢ exception(u; v) ≤ evalall(t)
BY
{ (Thin (-2)
   THEN (FLemma `evalall-sqequal` [-1] THENA Auto)
   THEN HypSubst' (-1) (-4)
   THEN HypSubst' (-1) 0
   THEN Hypothesis) }

---

Latex:

---

Latex:

1.  t  :  Base
2.  is-exception(evalall(evalall(t)))
3.  u  :  Base
4.  v  :  Base
5.  exception(u;  v)  \mleq{}  evalall(evalall(t))
6.  exception(u;  v)  \mleq{}  eval  x  =  evalall(t)  in
                                          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
7.  is-exception(eval  x  =  evalall(t)  in
                                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)
8.  (evalall(t))\mdownarrow{}
\mvdash{}  exception(u;  v)  \mleq{}  evalall(t)


By

---

Latex:
(Thin  (-2)
  THEN  (FLemma  `evalall-sqequal`  [-1]  THENA  Auto)
  THEN  HypSubst'  (-1)  (-4)
  THEN  HypSubst'  (-1)  0
  THEN  Hypothesis)

---

Home Index