---

Step * 1 1 1 2 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
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])
22. is-exception(F[⊥])
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)
⊢ F[⊥] ≤ G[⊥]
BY
{ OnMaybeHyp 2 (\h. (D h
                     THEN (SplitAndHyps THEN All Reduce)
                     THEN (FHyp (h+2) [-4] THENA Auto)
                     THEN Assert ⌜False⌝⋅
                     THEN Auto
                     THEN D -1
                     THEN BotDiv
                     THEN ImpossibleException (-1))) }

---

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
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.  (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[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[\mbot{}])
23.  (as)\mdownarrow{}
24.  \mforall{}a,b:Top.    (if  as  is  a  pair  then  a  otherwise  b  \msim{}  b)
25.  \mforall{}a,b:Top.    (if  as  =  Ax  then  a  otherwise  b  \msim{}  b)
\mvdash{}  F[\mbot{}]  \mleq{}  G[\mbot{}]


By

---

Latex:
OnMaybeHyp  2  (\mbackslash{}h.  (D  h
                                      THEN  (SplitAndHyps  THEN  All  Reduce)
                                      THEN  (FHyp  (h+2)  [-4]  THENA  Auto)
                                      THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                                      THEN  Auto
                                      THEN  D  -1
                                      THEN  BotDiv
                                      THEN  ImpossibleException  (-1)))

---

Home Index