---

Step * 2 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. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. F[b1] ≤ G[b2]
12. ∀j:ℕ. ∀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 
            ⊥ 
            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 
                    ⊥ 
                    as]))
⊢ F[rec-case(as) of
    [] => b1
    h::t =>
     r.H[h;t;r]] ≤ G[rec-case(as) of
                     [] => b2
                     h::t =>
                      r.J[h;t;r]]
BY
{ (RW (AddrC [1;2] UnfoldTopAbC) 0
   THEN OneFixpointLeast⋅
   THEN (InstHyp [⌜j⌝;⌜as⌝;⌜b1⌝;⌜b2⌝] (-2)⋅ THENA Auto)
   THEN SqLeTrans (-1)
   THEN Try (Trivial)
   THEN SqLeCD
   THEN Try (SqLeCD)
   THEN All Thin
   THEN Unfold `list_ind` 0
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Auto) }

---

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.  as  :  Base@i
9.  b1  :  Base@i
10.  b2  :  Base@i
11.  F[b1]  \mleq{}  G[b2]
12.  \mforall{}j:\mBbbN{}.  \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 
                        \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 
                                        \mbot{} 
                                        as]))
\mvdash{}  F[rec-case(as)  of
        []  =>  b1
        h::t  =>
          r.H[h;t;r]]  \mleq{}  G[rec-case(as)  of
                                          []  =>  b2
                                          h::t  =>
                                            r.J[h;t;r]]


By

---

Latex:
(RW  (AddrC  [1;2]  UnfoldTopAbC)  0
  THEN  OneFixpointLeast\mcdot{}
  THEN  (InstHyp  [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  SqLeTrans  (-1)
  THEN  Try  (Trivial)
  THEN  SqLeCD
  THEN  Try  (SqLeCD)
  THEN  All  Thin
  THEN  Unfold  `list\_ind`  0
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  Auto)

---

Home Index