Step
*
1
1
of Lemma
sqle-list_accum
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. strict1(λx.G[x])
5. H : Base
6. J : Base
7. ∀a,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]]))
8. j : ℤ
9. 0 < j
10. ∀as,b1,b2:Base.
((F[b1] ≤ G[b2])
⇒ (F[λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum H[y;h] t otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
b1
as] ≤ G[λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum J[y;h] t otherwise if v = Ax then y otherwise ⊥^j\000C - 1
⊥
b2
as]))
11. as : Base@i
12. b1 : Base@i
13. b2 : Base@i
14. F[b1] ≤ G[b2]@i
⊢ F[λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum H[y;h] t otherwise if v = Ax then y otherwise ⊥^j
⊥
b1
as] ≤ G[λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum J[y;h] t otherwise if v = Ax then y otherwise ⊥^j
⊥
b2
as]
BY
{ ((RWO "fun_exp_unroll_1" 0 THENA Auto)
THEN Reduce 0
THEN ((InstLemma `lifting-strict-callbyvalue`
[⌜so_lambda(x,y,z,w.F[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWW "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-callbyvalue`
[⌜so_lambda(x,y,z,w.G[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWW "-1" 0 THENA Auto)
)
THEN UseCbvSqle
THEN ((InstLemma `lifting-strict-ispair`
[⌜so_lambda(x,y,z,w.F[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-ispair`
[⌜so_lambda(x,y,z,w.G[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-isaxiom`
[⌜so_lambda(x,y,z,w.F[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-isaxiom`
[⌜so_lambda(x,y,z,w.G[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)) }
1
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. strict1(λx.G[x])
5. H : Base
6. J : Base
7. ∀a,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]]))
8. j : ℤ
9. 0 < j
10. ∀as,b1,b2:Base.
((F[b1] ≤ G[b2])
⇒ (F[λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum H[y;h] t otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
b1
as] ≤ G[λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum J[y;h] t otherwise if v = Ax then y otherwise ⊥^j\000C - 1
⊥
b2
as]))
11. as : Base@i
12. b1 : Base@i
13. b2 : Base@i
14. F[b1] ≤ G[b2]@i
15. ∀[a,B:Top]. (F[eval x = a in B[x]] ~ eval x = a in F[B[x]])
16. ∀[a,B:Top]. (G[eval x = a in B[x]] ~ eval x = a in G[B[x]])
17. (as)↓@i
18. ∀[a,b,c:Top]. (F[if a is a pair then b otherwise c] ~ if a is a pair then F[b] otherwise F[c])
19. ∀[a,b,c:Top]. (G[if a is a pair then b otherwise c] ~ if a is a pair then G[b] otherwise G[c])
20. ∀[a,b,c:Top]. (F[if a = Ax then b otherwise c] ~ if a = Ax then F[b] otherwise F[c])
21. ∀[a,b,c:Top]. (G[if a = Ax then b otherwise c] ~ if a = Ax then G[b] otherwise G[c])
⊢ if as is a pair then F[let h,t = as
in λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum H[y;h] t
otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
H[b1;h]
t] otherwise if as = Ax then F[b1] otherwise F[⊥]
≤ if as is a pair then G[let h,t = as
in λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum J[y;h] t
otherwise if v = Ax then y otherwise ⊥^j - 1
⊥
J[b2;h]
t] otherwise if as = Ax then G[b2] otherwise G[⊥]
Latex:
Latex:
1. F : Base
2. strict1(\mlambda{}x.F[x])
3. G : Base
4. strict1(\mlambda{}x.G[x])
5. H : Base
6. J : Base
7. \mforall{}a,r1,r2:Base. ((F[r1] \mleq{} G[r2]) {}\mRightarrow{} (F[H[r1;a]] \mleq{} G[J[r2;a]]))
8. j : \mBbbZ{}
9. 0 < j
10. \mforall{}as,b1,b2:Base.
((F[b1] \mleq{} G[b2])
{}\mRightarrow{} (F[\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ H[y;h] t
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
b1
as] \mleq{} G[\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ J[y;h]\000C t
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
b2
as]))
11. as : Base@i
12. b1 : Base@i
13. b2 : Base@i
14. F[b1] \mleq{} G[b2]@i
\mvdash{} F[\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ H[y;h] t otherwise if \000Cv = Ax then y otherwise \mbot{}\^{}j
\mbot{}
b1
as] \mleq{} G[\mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}$ J[y;h] t
otherwise if v = Ax then y otherwise \mbot{}\^{}j
\mbot{}
b2
as]
By
Latex:
((RWO "fun\_exp\_unroll\_1" 0 THENA Auto)
THEN Reduce 0
THEN ((InstLemma `lifting-strict-callbyvalue`
[\mkleeneopen{}so\_lambda(x,y,z,w.F[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWW "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-callbyvalue`
[\mkleeneopen{}so\_lambda(x,y,z,w.G[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWW "-1" 0 THENA Auto)
)
THEN UseCbvSqle
THEN ((InstLemma `lifting-strict-ispair`
[\mkleeneopen{}so\_lambda(x,y,z,w.F[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-ispair`
[\mkleeneopen{}so\_lambda(x,y,z,w.G[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-isaxiom`
[\mkleeneopen{}so\_lambda(x,y,z,w.F[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-isaxiom`
[\mkleeneopen{}so\_lambda(x,y,z,w.G[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
THENA (Auto THEN BLemma `strict1-strict4` THEN Auto)
)
THENM (RWO "-1" 0 THENA Auto)
))
Home
Index