---

Step * of Lemma sqle-list_ind

∀[F:Base]
  ∀[G:Base]
    ∀[H,J:Base].
      ∀as,b1,b2:Base.
        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]] 
        supposing F[b1] ≤ G[b2] 
      supposing ∀x,y,r1,r2:Base.  ((F[r1] ≤ G[r2]) ⇒ (F[H[x;y;r1]] ≤ G[J[x;y;r2]])) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])
BY
{ ((UnivCD THENA Auto)
   THEN Assert ⌜∀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]))⌝⋅
   ) }

1
.....assertion..... 
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]
⊢ ∀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]))

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

---

Latex:

---

Latex:
\mforall{}[F:Base]
    \mforall{}[G:Base]
        \mforall{}[H,J:Base].
            \mforall{}as,b1,b2:Base.
                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]] 
                supposing  F[b1]  \mleq{}  G[b2] 
            supposing  \mforall{}x,y,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[x;y;r1]]  \mleq{}  G[J[x;y;r2]])) 
        supposing  strict1(\mlambda{}x.G[x]) 
    supposing  strict1(\mlambda{}x.F[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\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}\mbackslash{}f\000Cf24  t]
                                                                                    otherwise  if  v  =  Ax  then  b2  otherwise  \mbot{}\^{}j 
                                                            \mbot{} 
                                                            as]))\mkleeneclose{}\mcdot{}
  )

---

Home Index