Step
*
1
of Lemma
sqle-list_ind
.....assertion.....
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. strict1(λx.G[x])
5. H : Base
6. J : Base
7. ∀x,y,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[x;y;r1]] ≤ G[J[x;y;r2]]))
8. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. F[b1] ≤ G[b2]
⊢ ∀j:ℕ. ∀as,b1,b2:Base.
((F[b1] ≤ G[b2])
⇒ (F[λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in H[h;t;list_ind t] otherwise if v = Ax then b1 otherwise ⊥^j
⊥
as] ≤ G[λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;t;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j
⊥
as]))
BY
{ (RepeatFor 4 (Thin (-1))
THEN InductionOnNat
THEN (UnivCD THENA Auto)
THEN (Reduce 0
THEN Try ((Progress Strictness
THEN OnMaybeHyp 2 (\h. (D h
THEN (SplitAndHyps THEN All Reduce)
THEN AssumeHasValue
THEN Try ((FHyp h [-1] THEN BotDiv THEN Auto))
THEN Assert ⌜False⌝⋅
THEN Try (FalseHD (-1))
THEN Try ((FHyp (h+2) [-1] THENA Auto))
THEN (RepeatFor 2 (D -1) THEN BotDiv)
THEN FLemma `exception-not-bottom` [-1]
THEN Auto))
))
)
THEN skip{((RWO "fun_exp_unroll_1" 0 THENA Auto)
THEN Reduce 0
THEN skip{(((InstLemma `lifting-strict-callbyvalue`
[⌜so_lambda(x,y,z,w.F[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto
THEN BLemma `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\h. (ParallelOp h
THEN RepUR ``so_lambda so_apply`` 0
THEN NthHyp h)))
)
THENM (RWW "-1" 0 THENA Auto)
)
THEN skip{(((InstLemma `lifting-strict-callbyvalue`
[⌜so_lambda(x,y,z,w.G[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto
THEN BLemma `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\h. (ParallelOp h
THEN RepUR ``so_lambda so_apply`` 0
THEN NthHyp h)))
)
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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\h. (ParallelOp h
THEN RepUR ``so_lambda so_apply`` 0
THEN NthHyp h)))
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-ispair`
[⌜so_lambda(x,y,z,w.G[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto
THEN BLemma `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\h. (ParallelOp h
THEN RepUR ``so_lambda so_apply`` 0
THEN NthHyp h)))
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-isaxiom`
[⌜so_lambda(x,y,z,w.F[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto
THEN BLemma `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\h. (ParallelOp h
THEN RepUR ``so_lambda so_apply`` 0
THEN NthHyp h)))
)
THENM (RWO "-1" 0 THENA Auto)
)
THEN ((InstLemma `lifting-strict-isaxiom`
[⌜so_lambda(x,y,z,w.G[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
THENA (Auto
THEN BLemma `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\h. (ParallelOp h
THEN RepUR ``so_lambda so_apply`` 0
THEN NthHyp h)))
)
THENM ((RWO "-1" 0 THENA Auto)
THEN AssumeHasValue
THEN (HasValueD (-1)
ORELSE (ExceptionCases (-1) THEN Try (Complete (SameException)))
)
THEN (HVimplies2 0 [1] THEN (RWO "-1" 0 THENA MemTop) THEN Reduce 0)
THEN Try ((HVimplies2 0 [1] THEN (RWO "-1" 0 THENA MemTop) THEN Reduce 0)))
))}
)})}) }
1
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. strict1(λx.G[x])
5. H : Base
6. J : Base
7. ∀x,y,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[x;y;r1]] ≤ G[J[x;y;r2]]))
8. j : ℤ
9. 0 < j
10. ∀as,b1,b2:Base.
((F[b1] ≤ G[b2])
⇒ (F[λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in H[h;t;list_ind t] otherwise if v = Ax then b1 otherwise ⊥^j - 1
⊥
as] ≤ G[λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;t;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j - 1
⊥
as]))
11. as : Base@i
12. b1 : Base@i
13. b2 : Base@i
14. F[b1] ≤ G[b2]@i
⊢ F[λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in H[h;t;list_ind t] otherwise if v = Ax then b1 otherwise ⊥^j
⊥
as] ≤ G[λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;t;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j
⊥
as]
Latex:
Latex:
.....assertion.....
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{}x,y,r1,r2:Base. ((F[r1] \mleq{} G[r2]) {}\mRightarrow{} (F[H[x;y;r1]] \mleq{} G[J[x;y;r2]]))
8. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. F[b1] \mleq{} G[b2]
\mvdash{} \mforall{}j:\mBbbN{}. \mforall{}as,b1,b2:Base.
((F[b1] \mleq{} G[b2])
{}\mRightarrow{} (F[\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in H[h;t;list$_{ind}$ t]
otherwise if v = Ax then b1 otherwise \mbot{}\^{}j
\mbot{}
as] \mleq{} G[\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in J[h;t;list$_{ind}$ t]
otherwise if v = Ax then b2 otherwise \mbot{}\^{}j
\mbot{}
as]))
By
Latex:
(RepeatFor 4 (Thin (-1))
THEN InductionOnNat
THEN (UnivCD THENA Auto)
THEN (Reduce 0
THEN Try ((Progress Strictness
THEN OnMaybeHyp 2 (\mbackslash{}h. (D h
THEN (SplitAndHyps THEN All Reduce)
THEN AssumeHasValue
THEN Try ((FHyp h [-1] THEN BotDiv THEN Auto))
THEN Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{}
THEN Try (FalseHD (-1))
THEN Try ((FHyp (h+2) [-1] THENA Auto))
THEN (RepeatFor 2 (D -1) THEN BotDiv)
THEN FLemma `exception-not-bottom` [-1]
THEN Auto))
))
)
THEN skip\{((RWO "fun\_exp\_unroll\_1" 0 THENA Auto)
THEN Reduce 0
THEN skip\{(((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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\mbackslash{}h. (ParallelOp h
THEN RepUR ``so\_lambda so\_apply`` 0
THEN NthHyp h)))
)
THENM (RWW "-1" 0 THENA Auto)
)
THEN skip\{(((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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\mbackslash{}h.
(ParallelOp h
THEN RepUR ``so\_lambda so\_apply`` 0
THEN NthHyp h)))
)
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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\mbackslash{}h.
(ParallelOp h
THEN RepUR ``so\_lambda so\_apply`` 0
THEN NthHyp h)))
)
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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\mbackslash{}h.
(ParallelOp h
THEN RepUR ``so\_lambda so\_apply`` 0
THEN NthHyp h)))
)
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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\mbackslash{}h.
(ParallelOp h
THEN RepUR ``so\_lambda so\_apply`` 0
THEN NthHyp h)))
)
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 `strict-strict4`
THEN Auto
THEN OnMaybeHyp 2 (\mbackslash{}h.
(ParallelOp h
THEN RepUR ``so\_lambda so\_apply`` 0
THEN NthHyp h)))
)
THENM ((RWO "-1" 0 THENA Auto)
THEN AssumeHasValue
THEN (HasValueD (-1)
ORELSE (ExceptionCases (-1)
THEN Try (Complete (SameException))
)
)
THEN (HVimplies2 0 [1]
THEN (RWO "-1" 0 THENA MemTop)
THEN Reduce 0)
THEN Try ((HVimplies2 0 [1]
THEN (RWO "-1" 0 THENA MemTop)
THEN Reduce 0)))
))\}
)\})\})
Home
Index