---

Step * of Lemma has-value-try

∀[t,n,B:Base].
  ↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)) 
  supposing (t?n:v.B[v])↓
BY
{ (Assert ∀[t,n,B:Base].
            ↓((t)↓ ∧ (t?n:v.B[v] ~ if n=2 n then t else ⊥))
             ∨ (∃m,u:Base. ((t ~ exception(m; u)) ∧ (t?n:v.B[v] ~ if n=2 m then B[u] else (exception(m; u))))) 
            supposing (t?n:v.B[v])↓ BY
         (Auto
          THEN UseWitness ⌜Ax⌝⋅
          THEN Unfold `member` 0
          THEN ((Refine_callbyvalueTry `m' `u' `x' `y' ⌜t⌝ ⌜n⌝ `v' ⌜B[v]⌝⋅
                 THEN Try (Complete (Auto))
                 THEN Fold `member` 0
                 THEN MemTypeCD)
                THENL [(OrLeft THEN Auto); (OrRight THEN Auto)]
          ))) }

1
1. ∀[t,n,B:Base].
     ↓((t)↓ ∧ (t?n:v.B[v] ~ if n=2 n then t else ⊥))
      ∨ (∃m,u:Base. ((t ~ exception(m; u)) ∧ (t?n:v.B[v] ~ if n=2 m then B[u] else (exception(m; u))))) 
     supposing (t?n:v.B[v])↓
⊢ ∀[t,n,B:Base].
    ↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)) 
    supposing (t?n:v.B[v])↓

---

Latex:

---

Latex:
\mforall{}[t,n,B:Base].
    \mdownarrow{}((t)\mdownarrow{}  \mwedge{}  (t?n:v.B[v]  \msim{}  t))  \mvee{}  (\mexists{}u:Base.  ((t  \msim{}  exception(n;  u))  \mwedge{}  (t?n:v.B[v]  \msim{}  B[u])  \mwedge{}  (B[u])\mdownarrow{})) 
    supposing  (t?n:v.B[v])\mdownarrow{}


By

---

Latex:
(Assert  \mforall{}[t,n,B:Base].
                    \mdownarrow{}((t)\mdownarrow{}  \mwedge{}  (t?n:v.B[v]  \msim{}  if  n=2  n  then  t  else  \mbot{}))
                      \mvee{}  (\mexists{}m,u:Base
                              ((t  \msim{}  exception(m;  u))  \mwedge{}  (t?n:v.B[v]  \msim{}  if  n=2  m  then  B[u]  else  (exception(m;  u))))) 
                    supposing  (t?n:v.B[v])\mdownarrow{}  BY
              (Auto
                THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                THEN  Unfold  `member`  0
                THEN  ((Refine\_callbyvalueTry  `m'  `u'  `x'  `y'  \mkleeneopen{}t\mkleeneclose{}  \mkleeneopen{}n\mkleeneclose{}  `v'  \mkleeneopen{}B[v]\mkleeneclose{}\mcdot{}
                              THEN  Try  (Complete  (Auto))
                              THEN  Fold  `member`  0
                              THEN  MemTypeCD)
                            THENL  [(OrLeft  THEN  Auto);  (OrRight  THEN  Auto)]
                )))

---

Home Index