---

Step * 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))
⊢ exception(u; v) ≤ evalall(t)
BY
{ (DupHyp (-1) THEN RW  (AddrC [2] RecUnfoldTopAbC) (-1) THEN ExceptionCases (-1)) }

1
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)

2
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. is-exception(evalall(t))
⊢ exception(u; v) ≤ evalall(t)

---

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))
\mvdash{}  exception(u;  v)  \mleq{}  evalall(t)


By

---

Latex:
(DupHyp  (-1)  THEN  RW    (AddrC  [2]  RecUnfoldTopAbC)  (-1)  THEN  ExceptionCases  (-1))

---

Home Index