Step * 2 3 of Lemma evalall-append-nil


1. : ℤ
2. 0 < j
3. ∀l:Base
     ((fix((λevalall,t. eval in
                        if is pair then let a,b 
                                            in eval a' evalall in
                                               eval b' evalall in
                                                 <a', b'> otherwise if is inl then eval evalall outl(x) in
                                                                                     inl y
                                                                    else if is inr then eval evalall outr(x) in
                                                                                          inr 
                                                                         else x)) 
       (l []))↓
      evalall,t. eval in
                     if is pair then let a,b 
                                         in eval a' evalall in
                                            eval b' evalall in
                                              <a', b'> otherwise if is inl then eval evalall outl(x) in
                                                                                  inl y
                                                                 else if is inr then eval evalall outr(x) in
                                                                                       inr 
                                                                      else x^j 
         ⊥ 
         (l []))↓
      (l ≤ fix((λevalall,t. eval in
                              if is pair then let a,b 
                                                  in eval a' evalall in
                                                     eval b' evalall in
                                                       <a', b'> otherwise if is inl then eval evalall outl(x) in
                                                                                           inl y
                                                                          else if is inr
                                                                               eval evalall outr(x) in
                                                                               inr 
                                                                               else x)) 
             (l [])))
4. Base@i
5. (fix((λevalall,t. eval in
                     if is pair then let a,b 
                                         in eval a' evalall in
                                            eval b' evalall in
                                              <a', b'> otherwise if is inl then eval evalall outl(x) in
                                                                                  inl y
                                                                 else if is inr then eval evalall outr(x) in
                                                                                       inr 
                                                                      else x)) 
    (inr outr(l []) ))↓@i
6. (eval = λevalall,t. eval in
                         if is pair then let a,b 
                                             in eval a' evalall in
                                                eval b' evalall in
                                                  <a', b'> otherwise if is inl then eval evalall outl(x) in
                                                                                      inl y
                                                                     else if is inr then eval evalall outr(x) in
                                                                                           inr 
                                                                          else x^j 
             ⊥ 
             outr(l []) in
    inr )↓@i
7. 0 ≤ 0
8. ∀a,b:Top.  (b b)
9. ∀a,b:Top.  (b b)
10. [] inr outr(l []) 
⊢ l ≤ eval fix((λevalall,t. eval in
                                if is pair then let a,b 
                                                    in eval a' evalall in
                                                       eval b' evalall in
                                                         <a', b'> otherwise if is inl then eval evalall outl(x) in
                                                                                             inl y
                                                                            else if is inr then eval evalall 
                                                                                                           outr(x) in
                                                                                                  inr 
                                                                                 else x)) 
               outr(l []) in
      inr 
BY
((InstLemma `ispair-or-isaxiom-append-nil` [⌜l⌝]⋅ THENA (Auto THEN HypSubst (-1) THEN Auto))
   THEN HypSubst (-2) (-1)
   THEN Reduce (-1)
   THEN (-1)
   THEN Auto)⋅ }


Latex:


Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}l:Base
          ((fix((\mlambda{}evalall,t.  eval  x  =  t  in
                                                if  x  is  a  pair  then  let  a,b  =  x 
                                                                                        in  eval  a'  =  evalall  a  in
                                                                                              eval  b'  =  evalall  b  in
                                                                                                  <a',  b'>
                                                otherwise  if  x  is  inl  then  eval  y  =  evalall  outl(x)  in
                                                                                                      inl  y
                                                                    else  if  x  is  inr  then  eval  y  =  evalall  outr(x)  in
                                                                                                                inr  y 
                                                                              else  x)) 
              (l  @  []))\mdownarrow{}
          {}\mRightarrow{}  (\mlambda{}evalall,t.  eval  x  =  t  in
                                          if  x  is  a  pair  then  let  a,b  =  x 
                                                                                  in  eval  a'  =  evalall  a  in
                                                                                        eval  b'  =  evalall  b  in
                                                                                            <a',  b'>
                                          otherwise  if  x  is  inl  then  eval  y  =  evalall  outl(x)  in
                                                                                                inl  y
                                                              else  if  x  is  inr  then  eval  y  =  evalall  outr(x)  in
                                                                                                          inr  y 
                                                                        else  x\^{}j  -  1 
                  \mbot{} 
                  (l  @  []))\mdownarrow{}
          {}\mRightarrow{}  (l  \mleq{}  fix((\mlambda{}evalall,t.  eval  x  =  t  in
                                                            if  x  is  a  pair  then  let  a,b  =  x 
                                                                                                    in  eval  a'  =  evalall  a  in
                                                                                                          eval  b'  =  evalall  b  in
                                                                                                              <a',  b'>
                                                            otherwise  if  x  is  inl  then  eval  y  =  evalall  outl(x)  in
                                                                                                                  inl  y
                                                                                else  if  x  is  inr  then  eval  y  =  evalall  outr(x)  in
                                                                                                                            inr  y 
                                                                                          else  x)) 
                          (l  @  [])))
4.  l  :  Base@i
5.  (fix((\mlambda{}evalall,t.  eval  x  =  t  in
                                          if  x  is  a  pair  then  let  a,b  =  x 
                                                                                  in  eval  a'  =  evalall  a  in
                                                                                        eval  b'  =  evalall  b  in
                                                                                            <a',  b'>
                                          otherwise  if  x  is  inl  then  eval  y  =  evalall  outl(x)  in
                                                                                                inl  y
                                                              else  if  x  is  inr  then  eval  y  =  evalall  outr(x)  in
                                                                                                          inr  y 
                                                                        else  x)) 
        (inr  outr(l  @  [])  ))\mdownarrow{}@i
6.  (eval  y  =  \mlambda{}evalall,t.  eval  x  =  t  in
                                                  if  x  is  a  pair  then  let  a,b  =  x 
                                                                                          in  eval  a'  =  evalall  a  in
                                                                                                eval  b'  =  evalall  b  in
                                                                                                    <a',  b'>
                                                  otherwise  if  x  is  inl  then  eval  y  =  evalall  outl(x)  in
                                                                                                        inl  y
                                                                      else  if  x  is  inr  then  eval  y  =  evalall  outr(x)  in
                                                                                                                  inr  y 
                                                                                else  x\^{}j  -  1 
                          \mbot{} 
                          outr(l  @  [])  in
        inr  y  )\mdownarrow{}@i
7.  0  \mleq{}  0
8.  \mforall{}a,b:Top.    (b  \msim{}  b)
9.  \mforall{}a,b:Top.    (b  \msim{}  b)
10.  l  @  []  \msim{}  inr  outr(l  @  []) 
\mvdash{}  l  \mleq{}  eval  y  =  fix((\mlambda{}evalall,t.  eval  x  =  t  in
                                                                if  x  is  a  pair  then  let  a,b  =  x 
                                                                                                        in  eval  a'  =  evalall  a  in
                                                                                                              eval  b'  =  evalall  b  in
                                                                                                                  <a',  b'>
                                                                otherwise  if  x  is  inl  then  eval  y  =  evalall  outl(x)  in
                                                                                                                      inl  y
                                                                                    else  if  x  is  inr  then  eval  y  =  evalall  outr(x)  in
                                                                                                                                inr  y 
                                                                                              else  x)) 
                              outr(l  @  [])  in
            inr  y 


By


Latex:
((InstLemma  `ispair-or-isaxiom-append-nil`  [\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  HypSubst  (-1)  0  THEN  Auto))
  THEN  HypSubst  (-2)  (-1)
  THEN  Reduce  (-1)
  THEN  D  (-1)
  THEN  Auto)\mcdot{}




Home Index