---

Step * 1 5 of Lemma l-last-cons


1. u : Base
2. v : Base
3. is-exception(case if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥
 of inl() =>
 u
 | inr() =>
 eval v = v in
 if v is a pair then let h,t = v 
                     in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then ⊥ otherwise ⊥)
4. if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥ ∈ Top + Top
⊢ if if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥
  then u
  else eval v = v in
       if v is a pair then let h,t = v 
                           in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then ⊥ otherwise ⊥
  fi  ≤ eval v = v in
        if v is a pair then let h,t = v 
                            in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then u otherwise ⊥
BY
{ ((Assert ⌜(if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥)↓⌝⋅ THENA Auto) THEN HasValueD (-1)) }

1
1. u : Base
2. v : Base
3. is-exception(case if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥
 of inl() =>
 u
 | inr() =>
 eval v = v in
 if v is a pair then let h,t = v 
                     in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then ⊥ otherwise ⊥)
4. if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥ ∈ Top + Top
5. (if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥)↓
6. (v)↓
⊢ if if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥
  then u
  else eval v = v in
       if v is a pair then let h,t = v 
                           in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then ⊥ otherwise ⊥
  fi  ≤ eval v = v in
        if v is a pair then let h,t = v 
                            in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then u otherwise ⊥

---

Latex:

---

Latex:

1.  u  :  Base
2.  v  :  Base
3.  is-exception(case  if  v  is  a  pair  then  ff  otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}
  of  inl()  =>
  u
  |  inr()  =>
  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{})
4.  if  v  is  a  pair  then  ff  otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}  \mmember{}  Top  +  Top
\mvdash{}  if  if  v  is  a  pair  then  ff  otherwise  if  v  =  Ax  then  tt  otherwise  \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    \mleq{}  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  u  otherwise  \mbot{}


By

---

Latex:
((Assert  \mkleeneopen{}(if  v  is  a  pair  then  ff  otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{})\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HasValueD  (-1)
  )

---

Home Index