---

Step * 1 2 1 1 of Lemma has-value-try


1. t : Base
2. n : Base
3. B : Base
4. m : Base
5. u : Base
6. t ~ exception(m; u)
7. t?n:v.B[v] ~ if n=2 m
                 then B[u]
                 else (exception(m; u))
8. (if n=2 m
     then B[u]
     else (exception(m; u)))↓
⊢ (t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓
BY
{ Assert ⌜(m ~ n) ∧ (if n=2 m then B[u] else (exception(m; u)) ~ B[u])⌝⋅ }

1
.....assertion..... 
1. t : Base
2. n : Base
3. B : Base
4. m : Base
5. u : Base
6. t ~ exception(m; u)
7. t?n:v.B[v] ~ if n=2 m
                 then B[u]
                 else (exception(m; u))
8. (if n=2 m
     then B[u]
     else (exception(m; u)))↓
⊢ (m ~ n) ∧ (if n=2 m then B[u] else (exception(m; u)) ~ B[u])

2
1. t : Base
2. n : Base
3. B : Base
4. m : Base
5. u : Base
6. t ~ exception(m; u)
7. t?n:v.B[v] ~ if n=2 m
                 then B[u]
                 else (exception(m; u))
8. (if n=2 m
     then B[u]
     else (exception(m; u)))↓
9. (m ~ n) ∧ (if n=2 m then B[u] else (exception(m; u)) ~ B[u])
⊢ (t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓

---

Latex:

---

Latex:

1.  t  :  Base
2.  n  :  Base
3.  B  :  Base
4.  m  :  Base
5.  u  :  Base
6.  t  \msim{}  exception(m;  u)
7.  t?n:v.B[v]  \msim{}  if  n=2  m
                                  then  B[u]
                                  else  (exception(m;  u))
8.  (if  n=2  m
          then  B[u]
          else  (exception(m;  u)))\mdownarrow{}
\mvdash{}  (t  \msim{}  exception(n;  u))  \mwedge{}  (t?n:v.B[v]  \msim{}  B[u])  \mwedge{}  (B[u])\mdownarrow{}


By

---

Latex:
Assert  \mkleeneopen{}(m  \msim{}  n)  \mwedge{}  (if  n=2  m  then  B[u]  else  (exception(m;  u))  \msim{}  B[u])\mkleeneclose{}\mcdot{}

---

Home Index