Step * 1 4 1 1 of Lemma l-last-cons


1. Base
2. Base
3. (if ⊥
then u
else eval in
     if is pair then let h,t 
                         in rec-case(t) of [] => λx.x h::t => r.λx.(r h) otherwise if Ax then ⊥ otherwise ⊥
fi )↓
4. ⊥ ∈ Top Top
5. (⊥)↓
6. (v)↓
7. ∀a,b:Top.  (if is pair then otherwise b)
8. ∀a,b:Top.  (if Ax then otherwise b)
⊢ if ⊥ then else ⊥ fi  ≤ ⊥
BY
Strictness }


Latex:


Latex:

1.  u  :  Base
2.  v  :  Base
3.  (if  \mbot{}
then  u
else  eval  v  =  v  in
          if  v  is  a  pair  then  let  h,t  =  v 
                                                  in  rec-case(t)  of  []  =>  \mlambda{}x.x  |  h::t  =>  r.\mlambda{}x.(r  h)  h
          otherwise  if  v  =  Ax  then  \mbot{}  otherwise  \mbot{}
fi  )\mdownarrow{}
4.  \mbot{}  \mmember{}  Top  +  Top
5.  (\mbot{})\mdownarrow{}
6.  (v)\mdownarrow{}
7.  \mforall{}a,b:Top.    (if  v  is  a  pair  then  a  otherwise  b  \msim{}  b)
8.  \mforall{}a,b:Top.    (if  v  =  Ax  then  a  otherwise  b  \msim{}  b)
\mvdash{}  if  \mbot{}  then  u  else  \mbot{}  fi    \mleq{}  \mbot{}


By


Latex:
Strictness




Home Index