---

Step * 2 1 2 1 of Lemma cbv-reduce-strict


1. F : Base
2. a : Base
3. B : Base
4. ∀x:Base. ((F[x])↓ ⇒ (x)↓)
5. ∀u,v,x:Base.  ((F[x] ~ exception(u; v)) ⇒ (↓(x ~ exception(u; v)) ∨ (x)↓))
6. ∀u,v:Base.  (B[exception(u; v)] ~ exception(u; v))
7. is-exception(F[eval x = a in
                  B[x]])
8. u : Base
9. v : Base
10. F eval x = a in B x ~ exception(u; v)
11. eval x = a in
    B x ~ exception(u; v)
12. is-exception(eval x = a in
                 B x)
13. is-exception(a)
14. u1 : Base
15. v1 : Base
16. a ~ exception(u1; v1)
⊢ eval x = exception(u1; v1) in
  B[x] ≤ B[exception(u1; v1)]
BY
{ TACTIC:RW (AddrC [1] (TagC (mk_tag_term 1))) 0 }

1
1. F : Base
2. a : Base
3. B : Base
4. ∀x:Base. ((F[x])↓ ⇒ (x)↓)
5. ∀u,v,x:Base.  ((F[x] ~ exception(u; v)) ⇒ (↓(x ~ exception(u; v)) ∨ (x)↓))
6. ∀u,v:Base.  (B[exception(u; v)] ~ exception(u; v))
7. is-exception(F[eval x = a in
                  B[x]])
8. u : Base
9. v : Base
10. F eval x = a in B x ~ exception(u; v)
11. eval x = a in
    B x ~ exception(u; v)
12. is-exception(eval x = a in
                 B x)
13. is-exception(a)
14. u1 : Base
15. v1 : Base
16. a ~ exception(u1; v1)
⊢ exception(u1; v1) ≤ B[exception(u1; v1)]

---

Latex:

---

Latex:

1.  F  :  Base
2.  a  :  Base
3.  B  :  Base
4.  \mforall{}x:Base.  ((F[x])\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{})
5.  \mforall{}u,v,x:Base.    ((F[x]  \msim{}  exception(u;  v))  {}\mRightarrow{}  (\mdownarrow{}(x  \msim{}  exception(u;  v))  \mvee{}  (x)\mdownarrow{}))
6.  \mforall{}u,v:Base.    (B[exception(u;  v)]  \msim{}  exception(u;  v))
7.  is-exception(F[eval  x  =  a  in
                                    B[x]])
8.  u  :  Base
9.  v  :  Base
10.  F  eval  x  =  a  in  B  x  \msim{}  exception(u;  v)
11.  eval  x  =  a  in
        B  x  \msim{}  exception(u;  v)
12.  is-exception(eval  x  =  a  in
                                  B  x)
13.  is-exception(a)
14.  u1  :  Base
15.  v1  :  Base
16.  a  \msim{}  exception(u1;  v1)
\mvdash{}  eval  x  =  exception(u1;  v1)  in
    B[x]  \mleq{}  B[exception(u1;  v1)]


By

---

Latex:
TACTIC:RW  (AddrC  [1]  (TagC  (mk\_tag\_term  1)))  0

---

Home Index