Step
*
3
1
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(λ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)>)
BY
{ ((InstHyp [⌜snd(as)⌝;⌜[fst(as) / bs]⌝;⌜cs⌝] 3⋅ THENA Auto)
THEN RW (AddrC [1;1;2] UnrollLoopsC) (-1)
THEN Reduce (-1)
THEN RW (AddrC [2;2] UnrollLoopsC) 0
THEN Reduce 0
THEN Trivial) }
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(\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{}
[fst(as) /
(fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as'\000C)]
otherwise if v = Ax then cs otherwise \mbot{}))
bs)]
(snd(as)))
8. 0 \mleq{} 0
9. as \msim{} <fst(as), snd(as)>
\mvdash{} \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\000C = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
[fst(as) /
(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)]
(snd(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\000C] t
otherwise if v = Ax then y otherwise \mbot{}))
bs
<fst(as), snd(as)>)
By
Latex:
((InstHyp [\mkleeneopen{}snd(as)\mkleeneclose{};\mkleeneopen{}[fst(as) / bs]\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{}] 3\mcdot{} THENA Auto)
THEN RW (AddrC [1;1;2] UnrollLoopsC) (-1)
THEN Reduce (-1)
THEN RW (AddrC [2;2] UnrollLoopsC) 0
THEN Reduce 0
THEN Trivial)
Home
Index