Step
*
1
6
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. 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 ⊥
BY
{ ExceptionCases (-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. is-exception(if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥)
5. (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 ⊥
2
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 ⊥)
5. is-exception(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. is-exception(if v is a pair then ff otherwise if v = Ax then tt otherwise \mbot{})
\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:
ExceptionCases (-1)
Home
Index