---

Step * 1 of Lemma sqle-list_ind-list_accum

.....assertion..... 
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. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. ∀x:Base. (G[x;b2] ≤ F[x])
⊢ ∀j:ℕ. ∀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 
         ⊥ 
         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 
                 ⊥ 
                 x 
                 as])
BY
{ ((ThinVar `as' THEN ThinVar `b1')
   THEN InductionOnNat
   THEN (UnivCD THENA Auto)
   THEN Reduce 0
   THEN Try ((Progress Strictness
              THEN OnMaybeHyp 4 (\h. ((InstHyp [⌜x⌝] h⋅ THENA Auto)
                                      THEN D -1
                                      THEN (SplitAndHyps THEN All Reduce)
                                      THEN AssumeHasValue
                                      THEN ((FHyp (-4) [-1] THEN Try (MemBase) THEN BotDiv)
                                      ORELSE (FHyp (-2) [-1]
                                              THEN Try (MemBase)
                                              THEN Assert ⌜False⌝⋅
                                              THEN Auto
                                              THEN D -1
                                              THEN (ImpossibleException (-1) ORELSE BotDiv ⋅))
                                      )))
              ))) }

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. x : Base@i
⊢ 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 
      ⊥ 
      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 
              ⊥ 
              x 
              as]

---

Latex:

---

Latex:
.....assertion..... 
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.  as  :  Base@i
9.  b1  :  Base@i
10.  b2  :  Base@i
11.  \mforall{}x:Base.  (G[x;b2]  \mleq{}  F[x])
\mvdash{}  \mforall{}j:\mBbbN{}.  \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 
                  \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]  t
                                                                  otherwise  if  v  =  Ax  then  y  otherwise  \mbot{}\^{}j 
                                  \mbot{} 
                                  x 
                                  as])


By

---

Latex:
((ThinVar  `as'  THEN  ThinVar  `b1')
  THEN  InductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  ((Progress  Strictness
                        THEN  OnMaybeHyp  4  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                                                        THEN  D  -1
                                                                        THEN  (SplitAndHyps  THEN  All  Reduce)
                                                                        THEN  AssumeHasValue
                                                                        THEN  ((FHyp  (-4)  [-1]  THEN  Try  (MemBase)  THEN  BotDiv)
                                                                        ORELSE  (FHyp  (-2)  [-1]
                                                                                        THEN  Try  (MemBase)
                                                                                        THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                                                                                        THEN  Auto
                                                                                        THEN  D  -1
                                                                                        THEN  (ImpossibleException  (-1)  ORELSE  BotDiv  \mcdot{}))
                                                                        )))
                        )))

---

Home Index