---

Step * 1 of Lemma poss-maj-member


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
⊢ (snd(poss-maj(eq;L;x)) ∈ [x / L])
BY
{ Unfold `poss-maj` 0 }

1
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])

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
\mvdash{}  (snd(poss-maj(eq;L;x))  \mmember{}  [x  /  L])


By

---

Latex:
Unfold  `poss-maj`  0

---

Home Index