---

Step * of Lemma list-if-has-value-rev-append

∀[as,bs:Base].  as ∈ Base List supposing (rev(as) + bs)↓
BY
{ (Auto
   THEN RepUR ``rev-append list_accum`` (-1)
   THEN Compactness (-1)
   THEN Unhide
   THEN MoveToConcl (-1)
   THEN Repeat (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv
   THEN (RWO "fun_exp_unroll_1" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN HasValueD (-1)
   THEN HVimplies2 (-2) [1]) }

1
1. j : ℤ
2. 0 < j
3. ∀as,bs:Base.
     ((fix((λlist_accum,y,L. eval v = L in
                             if v is a pair then let h,t = v 
                                                 in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥)) 
       bs 
       as)↓
     ⇒ (λlist_accum,y,L. eval v = L in
                          if v is a pair then let h,t = v 
                                              in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1 
         ⊥ 
         bs 
         as)↓
     ⇒ (as ∈ Base List))
4. as : Base@i
5. bs : Base@i
6. (fix((λlist_accum,y,L. eval v = L in
                          if v is a pair then let h,t = v 
                                              in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥)) 
    bs 
    <fst(as), snd(as)>)↓@i
7. (λlist_accum,y,L. eval v = L in
                     if v is a pair then let h,t = v 
                                         in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1 
    ⊥ 
    [fst(as) / bs] 
    (snd(as)))↓@i
8. 0 ≤ 0
9. as ~ <fst(as), snd(as)>
⊢ <fst(as), snd(as)> ∈ Base List

2
1. j : ℤ
2. 0 < j
3. ∀as,bs:Base.
     ((fix((λlist_accum,y,L. eval v = L in
                             if v is a pair then let h,t = v 
                                                 in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥)) 
       bs 
       as)↓
     ⇒ (λlist_accum,y,L. eval v = L in
                          if v is a pair then let h,t = v 
                                              in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1 
         ⊥ 
         bs 
         as)↓
     ⇒ (as ∈ Base List))
4. as : Base@i
5. bs : Base@i
6. (fix((λlist_accum,y,L. eval v = L in
                          if v is a pair then let h,t = v 
                                              in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥)) 
    bs 
    as)↓@i
7. (if as = Ax then bs otherwise ⊥)↓@i
8. (as)↓
9. ∀a,b:Top.  (if as is a pair then a otherwise b ~ b)
⊢ as ∈ Base List

---

Latex:

---

Latex:
\mforall{}[as,bs:Base].    as  \mmember{}  Base  List  supposing  (rev(as)  +  bs)\mdownarrow{}


By

---

Latex:
(Auto
  THEN  RepUR  ``rev-append  list\_accum``  (-1)
  THEN  Compactness  (-1)
  THEN  Unhide
  THEN  MoveToConcl  (-1)
  THEN  Repeat  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1)
  THEN  HVimplies2  (-2)  [1])

---

Home Index