---

Step * 2 of Lemma poss-maj-length


1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀v1:ℤ. ∀v2:T.
     ((fst(accumulate (with value p and list item z):
            let n,x = p 
            in if eq z x then <n + 1, x>
               if (n =z 0) then <1, z>
               else <n - 1, x>
               fi 
           over list:
             v
           with starting value:
            <v1, v2>))) ≤ (||v|| + v1))
6. v1 : ℤ
7. v2 : T
8. ¬(u = v2 ∈ T)
9. v1 = 0 ∈ ℤ
⊢ (fst(accumulate (with value p and list item z):
        let n,x = p 
        in if eq z x then <n + 1, x>
           if (n =z 0) then <1, z>
           else <n - 1, x>
           fi 
       over list:
         v
       with starting value:
        <1, u>))) ≤ ((||v|| + 1) + v1)
BY
{ ((Subst ⌜(||v|| + 1) + v1 ~ ||v|| + 1⌝ 0⋅ THENA Auto') THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}v1:\mBbbZ{}.  \mforall{}v2:T.
          ((fst(accumulate  (with  value  p  and  list  item  z):
                        let  n,x  =  p 
                        in  if  eq  z  x  then  <n  +  1,  x>
                              if  (n  =\msubz{}  0)  then  ə,  z>
                              else  <n  -  1,  x>
                              fi 
                      over  list:
                          v
                      with  starting  value:
                        <v1,  v2>)))  \mleq{}  (||v||  +  v1))
6.  v1  :  \mBbbZ{}
7.  v2  :  T
8.  \mneg{}(u  =  v2)
9.  v1  =  0
\mvdash{}  (fst(accumulate  (with  value  p  and  list  item  z):
                let  n,x  =  p 
                in  if  eq  z  x  then  <n  +  1,  x>
                      if  (n  =\msubz{}  0)  then  ə,  z>
                      else  <n  -  1,  x>
                      fi 
              over  list:
                  v
              with  starting  value:
                ə,  u>)))  \mleq{}  ((||v||  +  1)  +  v1)


By

---

Latex:
((Subst  \mkleeneopen{}(||v||  +  1)  +  v1  \msim{}  ||v||  +  1\mkleeneclose{}  0\mcdot{}  THENA  Auto')  THEN  BackThruSomeHyp)

---

Home Index