Step
*
of Lemma
rev-append-property-top-sqle
∀[as,bs,cs:Top]. (rev(as) + bs @ cs ≤ rev(as) + bs @ cs)
BY
{ ((UnivCD THENA Auto)
THEN RepUR ``rev-append list_accum append list_ind`` 0
THEN SqLeTopToBase
THEN OneFixpointLeast
THEN Repeat (MoveToConcl (-2))
THEN NatInd (-1)
THEN Reduce 0
THEN Strictness
THEN UnivCD
THEN Try (Complete (Auto))
THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
THEN Reduce 0
THEN AssumeHasValue
THEN Try (((HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (SameException))) 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. (λ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)))↓
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. (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 ⊥))
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)
3
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)
Latex:
Latex:
\mforall{}[as,bs,cs:Top]. (rev(as) + bs @ cs \mleq{} rev(as) + bs @ cs)
By
Latex:
((UnivCD THENA Auto)
THEN RepUR ``rev-append list\_accum append list\_ind`` 0
THEN SqLeTopToBase
THEN OneFixpointLeast
THEN Repeat (MoveToConcl (-2))
THEN NatInd (-1)
THEN Reduce 0
THEN Strictness
THEN UnivCD
THEN Try (Complete (Auto))
THEN (RWO "fun\_exp\_unroll\_1" 0 THENA Auto)
THEN Reduce 0
THEN AssumeHasValue
THEN Try (((HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (SameException)))
THEN HVimplies2 0 [1]
)))
Home
Index