---

Step * of Lemma poss-maj-length

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T].  ((fst(poss-maj(eq;L;x))) ≤ ||L||)
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``poss-maj`` 0
   THEN GenConclAtAddr [1;1;2]
   THEN (Subst ⌜||L|| ~ ||L|| + (fst(v))⌝ 0⋅
         THENA (DProdsAndUnions THEN (EqHD (-1) THENA Auto) THEN AllReduce THEN TACTIC:(Subst ⌜v1 ~ 0⌝ 0⋅ THEN Auto))
         )
   THEN ThinVar `x'
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN UnivCD
   THEN Try (Complete (Auto))
   THEN Repeat (AutoSplit)) }

1
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
⊢ (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 + 1, v2>))) ≤ ((||v|| + 1) + v1)

2
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)

3
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. v1 ≠ 0
8. v2 : T
9. ¬(u = 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 - 1, v2>))) ≤ ((||v|| + 1) + v1)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[x:T].    ((fst(poss-maj(eq;L;x)))  \mleq{}  ||L||)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``poss-maj``  0
  THEN  GenConclAtAddr  [1;1;2]
  THEN  (Subst  \mkleeneopen{}||L||  \msim{}  ||L||  +  (fst(v))\mkleeneclose{}  0\mcdot{}
              THENA  (DProdsAndUnions
                            THEN  (EqHD  (-1)  THENA  Auto)
                            THEN  AllReduce
                            THEN  TACTIC:(Subst  \mkleeneopen{}v1  \msim{}  0\mkleeneclose{}  0\mcdot{}  THEN  Auto))
              )
  THEN  ThinVar  `x'
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  UnivCD
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (AutoSplit))

---

Home Index