---

Step * 2 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]])
⊢ F[eval x = a in
    B[x]] ≤ F[B[a]]
BY
{ TACTIC:(ExceptionSqequal (-1)
          THEN Unfold `so_apply` -1
          THEN (FHyp 5 [-1] THENA Auto)
          THEN UseWitness ⌜Ax⌝⋅
          THEN D -1
          THEN Unfold `member` 0
          THEN Refine_axiomSqleEquality
          THEN D -1) }

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)
⊢ F[eval x = a in
    B[x]] ≤ F[B[a]]

2
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)↓
⊢ F[eval x = a in
    B[x]] ≤ F[B[a]]

---

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]])
\mvdash{}  F[eval  x  =  a  in
        B[x]]  \mleq{}  F[B[a]]


By

---

Latex:
TACTIC:(ExceptionSqequal  (-1)
                THEN  Unfold  `so\_apply`  -1
                THEN  (FHyp  5  [-1]  THENA  Auto)
                THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                THEN  D  -1
                THEN  Unfold  `member`  0
                THEN  Refine\_axiomSqleEquality
                THEN  D  -1)

---

Home Index