---

Step * 1 of Lemma strict-majority-property


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. ||L|| < 2 * ||filter(λy.(eq y x);L)||
⊢ if null(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)))
then inr ⋅ 
else inl (fst(hd(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)))))
fi 
= (inl x)
∈ (T?)
BY
{ ((InstLemma `decidable-equal-deq` [⌜T⌝]⋅ THENA Auto)
   THEN (Assert (x ∈ L) BY
               (SupposeNot
                THEN (RWO "filter_is_nil" (-3) THEN Reduce (-3) THEN Auto')
                THEN RepUR ``so_apply`` 0
                THEN Reduce 0
                THEN BLemma `l_all_iff`
                THEN Auto
                THEN ParallelOp -3⋅
                THEN RW assert_pushdownC (-1)
                THEN Auto))
   ) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. ||L|| < 2 * ||filter(λy.(eq y x);L)||
6. ∀x,y:T.  Dec(x = y ∈ T)
7. (x ∈ L)
⊢ if null(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)))
then inr ⋅ 
else inl (fst(hd(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)))))
fi 
= (inl x)
∈ (T?)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  ||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||
\mvdash{}  if  null(filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq)))
then  inr  \mcdot{} 
else  inl  (fst(hd(filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq)))))
fi 
=  (inl  x)


By

---

Latex:
((InstLemma  `decidable-equal-deq`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (x  \mmember{}  L)  BY
                          (SupposeNot
                            THEN  (RWO  "filter\_is\_nil"  (-3)  THEN  Reduce  (-3)  THEN  Auto')
                            THEN  RepUR  ``so\_apply``  0
                            THEN  Reduce  0
                            THEN  BLemma  `l\_all\_iff`
                            THEN  Auto
                            THEN  ParallelOp  -3\mcdot{}
                            THEN  RW  assert\_pushdownC  (-1)
                            THEN  Auto))
  )

---

Home Index