Step
*
1
1
1
of Lemma
sqle-list_ind-list_accum
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. ∀z:Base. strict1(λx.G[z;x])
5. H : Base
6. J : Base
7. ∀a,b,c:Base. (G[b;J[a;c]] ≤ G[H[b;a];c])
8. b2 : Base@i
9. ∀x:Base. (G[x;b2] ≤ F[x])
10. j : ℤ
11. 0 < j
12. ∀as,x:Base.
(G[x;λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j - 1
⊥
as] ≤ 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 \000C- 1
⊥
x
as])
13. as : Base@i
14. b1 : Base@i
15. ∀[a,B:Top]. (F[eval x = a in B[x]] ~ eval x = a in F[B[x]])
16. ∀[a,B:Top]. (G[b1;eval x = a in B[x]] ~ eval x = a in G[b1;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[b1;if a is a pair then b otherwise c] ~ if a is a pair then G[b1;b] otherwise G[b1;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[b1;if a = Ax then b otherwise c] ~ if a = Ax then G[b1;b] otherwise G[b1;c])
⊢ if as is a pair then G[b1;let h,t = as
in J[h;λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;list_ind t]
otherwise if v = Ax then b2 otherwise ⊥^j - 1
⊥
t]] otherwise if as = Ax then G[b1;b2] otherwise G[b1;⊥]
≤ 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[⊥]
BY
{ (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))
THEN Try (((InstHyp [⌜snd(as)⌝;⌜H[b1;fst(as)]⌝] 12⋅ THENA Auto)
THEN SqLeTrans (-1)
THEN Try (Trivial)
THEN BackThruSomeHyp))) }
1
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. ∀z:Base. strict1(λx.G[z;x])
5. H : Base
6. J : Base
7. ∀a,b,c:Base. (G[b;J[a;c]] ≤ G[H[b;a];c])
8. b2 : Base@i
9. ∀x:Base. (G[x;b2] ≤ F[x])
10. j : ℤ
11. 0 < j
12. ∀as,x:Base.
(G[x;λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j - 1
⊥
as] ≤ 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 \000C- 1
⊥
x
as])
13. as : Base@i
14. b1 : Base@i
15. ∀[a,B:Top]. (F[eval x = a in B[x]] ~ eval x = a in F[B[x]])
16. ∀[a,B:Top]. (G[b1;eval x = a in B[x]] ~ eval x = a in G[b1;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[b1;if a is a pair then b otherwise c] ~ if a is a pair then G[b1;b] otherwise G[b1;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[b1;if a = Ax then b otherwise c] ~ if a = Ax then G[b1;b] otherwise G[b1;c])
22. (G[b1;⊥])↓
23. (as)↓
24. ∀a,b:Top. (if as is a pair then a otherwise b ~ b)
25. ∀a,b:Top. (if as = Ax then a otherwise b ~ b)
⊢ G[b1;⊥] ≤ F[⊥]
2
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. ∀z:Base. strict1(λx.G[z;x])
5. H : Base
6. J : Base
7. ∀a,b,c:Base. (G[b;J[a;c]] ≤ G[H[b;a];c])
8. b2 : Base@i
9. ∀x:Base. (G[x;b2] ≤ F[x])
10. j : ℤ
11. 0 < j
12. ∀as,x:Base.
(G[x;λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j - 1
⊥
as] ≤ 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 \000C- 1
⊥
x
as])
13. as : Base@i
14. b1 : Base@i
15. ∀[a,B:Top]. (F[eval x = a in B[x]] ~ eval x = a in F[B[x]])
16. ∀[a,B:Top]. (G[b1;eval x = a in B[x]] ~ eval x = a in G[b1;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[b1;if a is a pair then b otherwise c] ~ if a is a pair then G[b1;b] otherwise G[b1;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[b1;if a = Ax then b otherwise c] ~ if a = Ax then G[b1;b] otherwise G[b1;c])
22. is-exception(G[b1;⊥])
23. (as)↓
24. ∀a,b:Top. (if as is a pair then a otherwise b ~ b)
25. ∀a,b:Top. (if as = Ax then a otherwise b ~ b)
⊢ G[b1;⊥] ≤ F[⊥]
Latex:
Latex:
1. F : Base
2. strict1(\mlambda{}x.F[x])
3. G : Base
4. \mforall{}z:Base. strict1(\mlambda{}x.G[z;x])
5. H : Base
6. J : Base
7. \mforall{}a,b,c:Base. (G[b;J[a;c]] \mleq{} G[H[b;a];c])
8. b2 : Base@i
9. \mforall{}x:Base. (G[x;b2] \mleq{} F[x])
10. j : \mBbbZ{}
11. 0 < j
12. \mforall{}as,x:Base.
(G[x;\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in J[h;list$_{ind}$ t] otherwise if v\000C = Ax then b2 otherwise \mbot{}\^{}j - 1
\mbot{}
as] \mleq{} 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] \000Ct
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
x
as])
13. as : Base@i
14. b1 : Base@i
15. \mforall{}[a,B:Top]. (F[eval x = a in B[x]] \msim{} eval x = a in F[B[x]])
16. \mforall{}[a,B:Top]. (G[b1;eval x = a in B[x]] \msim{} eval x = a in G[b1;B[x]])
17. (as)\mdownarrow{}@i
18. \mforall{}[a,b,c:Top]. (F[if a is a pair then b otherwise c] \msim{} if a is a pair then F[b] otherwise F[c])
19. \mforall{}[a,b,c:Top].
(G[b1;if a is a pair then b otherwise c] \msim{} if a is a pair then G[b1;b] otherwise G[b1;c])
20. \mforall{}[a,b,c:Top]. (F[if a = Ax then b otherwise c] \msim{} if a = Ax then F[b] otherwise F[c])
21. \mforall{}[a,b,c:Top]. (G[b1;if a = Ax then b otherwise c] \msim{} if a = Ax then G[b1;b] otherwise G[b1;c])
\mvdash{} if as is a pair then G[b1;let h,t = as
in J[h;\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in J[h;list$_{ind\mbackslash{}ff7\000Cd$ t]
otherwise if v = Ax then b2 otherwise \mbot{}\^{}j - 1
\mbot{}
t]] otherwise if as = Ax then G[b1;b2] otherwise G[b1;\mbot{}]
\mleq{} if as is a pair then F[let h,t = as
in \mlambda{}list$_{accum}$,y,L. eval v = L in
if v is a pair then let h,t = v
in list$_{accum}\mbackslash{}f\000Cf24 H[y;h] t
otherwise if v = Ax then y otherwise \mbot{}\^{}j - 1
\mbot{}
H[b1;h]
t] otherwise if as = Ax then F[b1] otherwise F[\mbot{}]
By
Latex:
(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))
THEN Try (((InstHyp [\mkleeneopen{}snd(as)\mkleeneclose{};\mkleeneopen{}H[b1;fst(as)]\mkleeneclose{}] 12\mcdot{} THENA Auto)
THEN SqLeTrans (-1)
THEN Try (Trivial)
THEN BackThruSomeHyp)))
Home
Index