---

Step * 1 of Lemma sqle-list_accum

.....assertion..... 
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. 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_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
{ (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))
              ))) }

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
⊢ 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]

---

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{}a,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[r1;a]]  \mleq{}  G[J[r2;a]]))
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$_{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 
                    \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:
(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))
                        )))

---

Home Index