---

Step * 1 1 of Lemma poss-maj-member


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
⊢ (snd(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:
         L
       with starting value:
        <0, x>)) ∈ [x / L])
BY
{ Assert ⌜∀m:ℕ
            (snd(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:
                   L
                 with starting value:
                  <m, x>)) ∈ [x / L])⌝⋅ }

1
.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
⊢ ∀m:ℕ
    (snd(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:
           L
         with starting value:
          <m, x>)) ∈ [x / L])

2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. ∀m:ℕ
     (snd(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:
            L
          with starting value:
           <m, x>)) ∈ [x / L])
⊢ (snd(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:
         L
       with starting value:
        <0, x>)) ∈ [x / L])

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
\mvdash{}  (snd(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:
                  L
              with  starting  value:
                ɘ,  x>))  \mmember{}  [x  /  L])


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}
                    (snd(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:
                                  L
                              with  starting  value:
                                <m,  x>))  \mmember{}  [x  /  L])\mkleeneclose{}\mcdot{}

---

Home Index