Step
*
3
of Lemma
rev-append-property-top-sqle
1. j : ℤ
2. 0 < j
3. ∀as,bs,cs:Base.
(λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
bs)
as ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
(fix((λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥))
bs
as))
4. as : Base@i
5. bs : Base@i
6. cs : Base@i
7. is-exception(eval v = as in
if v is a pair then let h,t = v
in λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t
otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
[h /
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')]
otherwise if v = Ax then cs otherwise ⊥))
bs)]
t otherwise if v = Ax then fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a /
(list_ind
as')]
otherwise if v = Ax then cs
otherwise ⊥))
bs otherwise ⊥)
⊢ eval v = as in
if v is a pair then let h,t = v
in λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t
otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
[h /
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')]
otherwise if v = Ax then cs otherwise ⊥))
bs)]
t otherwise if v = Ax then fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')]
otherwise if v = Ax then cs otherwise ⊥))
bs otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
if v is a pair
then let a,as' = v
in [a / (list_ind as')]
otherwise if v = Ax then cs
otherwise ⊥))
(fix((λlist_accum,y,L. eval v = L in
if v is a pair
then let h,t = v
in list_accum [h / y] t
otherwise if v = Ax then y
otherwise ⊥))
bs
as)
BY
{ (ExceptionCases (-1)
THEN Try (ComputeSameException 200)
THEN (CallByValueReduceOn ⌜as⌝ 0⋅ THENA Auto)
THEN HVimplies2 0 [1]) }
1
1. j : ℤ
2. 0 < j
3. ∀as,bs,cs:Base.
(λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
bs)
as ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
(fix((λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥))
bs
as))
4. as : Base@i
5. bs : Base@i
6. cs : Base@i
7. is-exception(λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - \000C1
⊥
[fst(as) /
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥)\000C)
bs)]
(snd(as)))
8. 0 ≤ 0
9. as ~ <fst(as), snd(as)>
⊢ λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
[fst(as) /
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
bs)]
(snd(as)) ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
(fix((λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥)\000C)
bs
<fst(as), snd(as)>)
2
1. j : ℤ
2. 0 < j
3. ∀as,bs,cs:Base.
(λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
bs)
as ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥))
(fix((λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥))
bs
as))
4. as : Base@i
5. bs : Base@i
6. cs : Base@i
7. is-exception(eval v = as in
if v is a pair then let h,t = v
in λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t
otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
[h /
(fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')]
otherwise if v = Ax then cs otherwise ⊥))
bs)]
t otherwise if v = Ax then fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a /
(list_ind
as')]
otherwise if v = Ax then cs
otherwise ⊥))
bs otherwise ⊥)
8. (as)↓
9. ∀a,b:Top. (if as is a pair then a otherwise b ~ b)
⊢ if as = Ax then fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then cs otherwise ⊥)\000C)
bs otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')]
otherwise if v = Ax then cs otherwise ⊥))
(fix((λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum [h / y] t
otherwise if v = Ax then y otherwise ⊥))
bs
as)
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}as,bs,cs:Base.
(\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ [h / y] t
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
(fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as')]
otherwise if v = Ax then cs otherwise \mbot{}))
bs)
as \mleq{} fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as')]
otherwise if v = Ax then cs otherwise \mbot{}))
(fix((\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ [h / y] t
otherwise if v = Ax then y otherwise \mbot{}))
bs
as))
4. as : Base@i
5. bs : Base@i
6. cs : Base@i
7. is-exception(eval v = as in
if v is a pair then let h,t = v
in \mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{acc\000Cum}$ [h / y] t
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
[h /
(fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$\mbackslash{}ff5\000Cf{ind}$ as')]
otherwise if v = Ax then cs otherwise \mbot{}))
bs)]
t
otherwise if v = Ax then fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$\mbackslash{}ff5\000Cf{ind}$ as')]
otherwise if v = Ax then cs otherwise \mbot{}))
bs otherwise \mbot{})
\mvdash{} eval v = as in
if v is a pair then let h,t = v
in \mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ [\000Ch / y] t
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
[h /
(fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}\000C$ as')]
otherwise if v = Ax then cs otherwise \mbot{}))
bs)]
t otherwise if v = Ax then fix((\mlambda{}list$_{ind}$,L. eval v\000C = L in
if v is a pair
then let a,as' = v
in [a / (list$_\mbackslash{}ff\000C7bind}$ as')]
otherwise if v = Ax then cs
otherwise \mbot{}))
bs otherwise \mbot{}
\mleq{} fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as')]
otherwise if v = Ax then cs otherwise \mbot{}))
(fix((\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ [h / y] t
otherwise if v = Ax then y otherwise \mbot{}))
bs
as)
By
Latex:
(ExceptionCases (-1)
THEN Try (ComputeSameException 200)
THEN (CallByValueReduceOn \mkleeneopen{}as\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN HVimplies2 0 [1])
Home
Index