---

Step * 1 1 1 1 of Lemma poss-maj-member


1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀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:
            v
          with starting value:
           <m, x>)) ∈ [x / v])
6. x : T
7. 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:
         v
       with starting value:
        if eq u x then <m + 1, x>
        if (m =z 0) then <1, u>
        else <m - 1, x>
        fi )) ∈ [x; [u / v]])
BY
{ (SplitOnConclITE THENA Auto) }

1
.....truecase..... 
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀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:
            v
          with starting value:
           <m, x>)) ∈ [x / v])
6. x : T
7. m : ℕ
8. u = 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:
         v
       with starting value:
        <m + 1, x>)) ∈ [x; [u / v]])

2
.....falsecase..... 
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀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:
            v
          with starting value:
           <m, x>)) ∈ [x / v])
6. x : T
7. m : ℕ
8. ¬(u = 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:
         v
       with starting value:
        if (m =z 0) then <1, u> else <m - 1, x> fi )) ∈ [x; [u / v]])

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}x:T.  \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:
                        v
                    with  starting  value:
                      <m,  x>))  \mmember{}  [x  /  v])
6.  x  :  T
7.  m  :  \mBbbN{}
\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:
                  v
              with  starting  value:
                if  eq  u  x  then  <m  +  1,  x>
                if  (m  =\msubz{}  0)  then  ə,  u>
                else  <m  -  1,  x>
                fi  ))  \mmember{}  [x;  [u  /  v]])


By

---

Latex:
(SplitOnConclITE  THENA  Auto)

---

Home Index