Step
*
1
1
3
of Lemma
sqle-list_ind
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
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. 0 ≤ 0@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])
22. is-exception(F[H[fst(as);snd(as);λ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
⊥
(snd(as))]])
23. 0 ≤ 0
24. as ~ <fst(as), snd(as)>
⊢ F[H[fst(as);snd(as);λ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 - \000C1
⊥
(snd(as))]] ≤ G[J[fst(as);snd(as);λ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
⊥
(snd(as))]]
BY
{ ((InstHyp [⌜fst(as)⌝;⌜snd(as)⌝;⌜λ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
⊥
(snd(as))⌝;⌜λ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
⊥
(snd(as))⌝] 7⋅
THENA (Try (MemBase) THEN BackThruSomeHyp THEN Auto)
)
THENM (SqLeTrans (-1) THEN Try (Hypothesis) THEN Try (Complete (SqLeCD)))
) }
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{}x,y,r1,r2:Base. ((F[r1] \mleq{} G[r2]) {}\mRightarrow{} (F[H[x;y;r1]] \mleq{} G[J[x;y;r2]]))
8. j : \mBbbZ{}
9. 0 < j
10. \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 - 1
\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 - 1
\mbot{}
as]))
11. as : Base@i
12. b1 : Base@i
13. b2 : Base@i
14. F[b1] \mleq{} G[b2]@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[eval x = a in B[x]] \msim{} eval x = a in G[B[x]])
17. 0 \mleq{} 0@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[if a is a pair then b otherwise c] \msim{} if a is a pair then G[b] otherwise G[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[if a = Ax then b otherwise c] \msim{} if a = Ax then G[b] otherwise G[c])
22. is-exception(F[H[fst(as);snd(as);\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in H[h;t;list$_{ind\000C}$ t]
otherwise if v = Ax then b1 otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(as))]])
23. 0 \mleq{} 0
24. as \msim{} <fst(as), snd(as)>
\mvdash{} F[H[fst(as);snd(as);\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 - 1
\mbot{}
(snd(as))]]
\mleq{} G[J[fst(as);snd(as);\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 - 1
\mbot{}
(snd(as))]]
By
Latex:
((InstHyp [\mkleeneopen{}fst(as)\mkleeneclose{};\mkleeneopen{}snd(as)\mkleeneclose{};\mkleeneopen{}\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in H[h;t;list$_{ind}\000C$ t]
otherwise if v = Ax then b1 otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(as))\mkleeneclose{};\mkleeneopen{}\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let h,t = v
in J[h;t;list$_\mbackslash{}\000Cff7bind}$ t]
otherwise if v = Ax then b2 otherwise \mbot{}\^{}j - \000C1
\mbot{}
(snd(as))\mkleeneclose{}] 7\mcdot{}
THENA (Try (MemBase) THEN BackThruSomeHyp THEN Auto)
)
THENM (SqLeTrans (-1) THEN Try (Hypothesis) THEN Try (Complete (SqLeCD)))
)
Home
Index