---

Step * of Lemma evalall-append-sqle

∀a,b:Top.  (evalall(a @ b) ≤ eval u = evalall(a) in eval v = evalall(b) in   evalall(u @ v))
BY
{ TACTIC:((Auto THEN SqLeTopToBase)
          THEN RW (AddrC [1] (UnfoldC `append`)) 0
          THEN Unfold `list_ind` 0
          THEN OneFixpointLeast
          THEN RepeatFor 2 (MoveToConcl 1)
          THEN NatInd 1
          THEN Reduce 0
          THEN Strictness
          THEN (UnivCD THENA Auto)
          THEN ((RWO "fun_exp_unroll_1" 0 THENA Auto) ORELSE Auto)
          THEN (RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Reduce 0)
          THEN (RW (AddrC [2;1] RecUnfoldTopAbC) 0 THEN Reduce 0)
          THEN RW (SubC (LiftC true)) 0
          THEN UseCbvSqle
          THEN HVimplies2 0 [1;1]
          THEN ((RWO "-1" 0 THENA Complete (Auto)) ORELSE (RW (SubC (LiftC true)) 0 THEN UseCbvSqle))) }

1
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
     (evalall(λlist_ind,L. eval v = L in
                           if v is a pair then let a,as' = v 
                                               in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1 
              ⊥ 
              a) ≤ eval u = evalall(a) in
                   eval v = evalall(b) in
                     evalall(u @ v))
4. a : Base
5. b : Base
6. 0 ≤ 0
7. a ~ <fst(a), snd(a)>
8. (evalall(fst(a)))↓
⊢ eval b' = evalall(λlist_ind,L. eval v = L in
                                 if v is a pair then let a,as' = v 
                                                     in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - \000C1 
                    ⊥ 
                    (snd(a))) in
  <evalall(fst(a)), b'> ≤ eval u = eval b' = evalall(snd(a)) in
                                   <evalall(fst(a)), b'> in
                          eval v = evalall(b) in
                            evalall(u @ v)

2
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
     (evalall(λlist_ind,L. eval v = L in
                           if v is a pair then let a,as' = v 
                                               in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1 
              ⊥ 
              a) ≤ eval u = evalall(a) in
                   eval v = evalall(b) in
                     evalall(u @ v))
4. a : Base
5. b : Base
6. (a)↓
7. ∀a@0,b:Top.  (if a is a pair then a@0 otherwise b ~ b)
⊢ eval v = if a = Ax then b otherwise ⊥ in
  if v is a pair then let a,b = v 
                      in eval a' = evalall(a) in
                         eval b' = evalall(b) in
                           <a', b'> otherwise if v is inl then eval y = evalall(outl(v)) in
                                                               inl y
                                              else if v is inr then eval y = evalall(outr(v)) in
                                                                    inr y 
                                                   else v ≤ eval u = if a is inl then eval y = evalall(outl(a)) in
                                                                                      inl y
                                                                     else if a is inr then eval y = evalall(outr(a)) in
                                                                                           inr y 
                                                                          else a in
                                                            eval v = evalall(b) in
                                                              evalall(u @ v)

---

Latex:

---

Latex:
\mforall{}a,b:Top.    (evalall(a  @  b)  \mleq{}  eval  u  =  evalall(a)  in  eval  v  =  evalall(b)  in      evalall(u  @  v))


By

---

Latex:
TACTIC:((Auto  THEN  SqLeTopToBase)
                THEN  RW  (AddrC  [1]  (UnfoldC  `append`))  0
                THEN  Unfold  `list\_ind`  0
                THEN  OneFixpointLeast
                THEN  RepeatFor  2  (MoveToConcl  1)
                THEN  NatInd  1
                THEN  Reduce  0
                THEN  Strictness
                THEN  (UnivCD  THENA  Auto)
                THEN  ((RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)  ORELSE  Auto)
                THEN  (RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Reduce  0)
                THEN  (RW  (AddrC  [2;1]  RecUnfoldTopAbC)  0  THEN  Reduce  0)
                THEN  RW  (SubC  (LiftC  true))  0
                THEN  UseCbvSqle
                THEN  HVimplies2  0  [1;1]
                THEN  ((RWO  "-1"  0  THENA  Complete  (Auto))  ORELSE  (RW  (SubC  (LiftC  true))  0  THEN  UseCbvSqle)))

---

Home Index