---

Step * 1 of Lemma l-last-cons


1. u : Top
2. v : Top
⊢ 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
{ (SqEqualTopToBase THEN SqequalSqle THEN AssumeHasValue THEN (HasValueD (-1) ORELSE ExceptionCases (-1))) }

1
1. u : Base
2. v : Base
3. (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. (v)↓
⊢ 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 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 

2
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. (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 

3
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 

4
1. u : Base
2. v : Base
3. (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 )↓
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 ⊥

5
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 ⊥

6
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. is-exception(if v is a pair then ff otherwise if v = Ax then tt 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  ≤ 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  :  Top
2.  v  :  Top
\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{} 
\msim{}  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:
(SqEqualTopToBase
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  (HasValueD  (-1)  ORELSE  ExceptionCases  (-1)))

---

Home Index