---

Step * 1 3 of Lemma l-last-cons


1. u : Base
2. v : Base
3. is-exception(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 ⊥)
4. is-exception(v)
⊢ 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 ⊥ 
  ≤ 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 
BY
{ (ExceptionSqequal (-1)
   THEN RenameTo `zz' `v'
   THEN HypSubst'  (-1) 0
   THEN RW (SubC (TagC (mk_tag_term 100))) 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  Base
2.  v  :  Base
3.  is-exception(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{})
4.  is-exception(v)
\mvdash{}  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{} 
    \mleq{}  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 


By

---

Latex:
(ExceptionSqequal  (-1)
  THEN  RenameTo  `zz'  `v'
  THEN  HypSubst'    (-1)  0
  THEN  RW  (SubC  (TagC  (mk\_tag\_term  100)))  0
  THEN  Auto)

---

Home Index