---

Step * 3 of Lemma apply-alist-count-repeats


1. T : Type
2. eq : EqDecider(T)
3. x : T
⊢ ∀ys:T List. ∀y:T.
    ((apply-alist(eq;count-repeats(ys,eq);x) = if x ∈b ys then inl ||filter(λy.(eq y x);ys)|| else inr ⋅  fi  ∈ (ℕ+?))
    ⇒ (apply-alist(eq;count-repeats(ys @ [y],eq);x)
       = if x ∈b ys @ [y] then inl ||filter(λy.(eq y x);ys @ [y])|| else inr ⋅  fi 
       ∈ (ℕ+?)))
BY
{ ((D 0 THENA Auto)
   THEN (AutoSplit
         THENL [TACTIC:(Assert 0 < ||filter(λy.(eq y x);ys)|| BY
                              (BLemma `member-exists2`
                               THEN Auto
                               THEN (RWO "member_filter" 0 THENA Auto)
                               THEN Reduce 0
                               THEN Auto))
               ; TACTIC: Id]
   )
   THEN ((((D 0 THENA Auto) THEN AutoSplit)
          THENL [TACTIC:(RenameVar `y' (-2)
                         THEN (Assert 0 < ||filter(λy.(eq y x);ys @ [y])|| BY
                                     (BLemma `member-exists2`
                                      THEN Auto
                                      THEN (RWO "member_filter" 0 THENA Auto)
                                      THEN Reduce 0
                                      THEN Auto))
                         )
                ; TACTIC:Try ((D (-1) THEN Complete (Auto)))⋅]
         )
         THEN ((D 0 THENA Auto)
               THEN (Unfold `count-repeats` 0
                     THEN (RWO "list_accum_append" 0 THENA Auto)
                     THEN Fold `count-repeats` 0
                     THEN Reduce 0
                     THEN (RWO "apply-updated-alist" 0⋅ THENA Auto)
                     THEN (HypSubst (-1) 0 THENM Reduce 0)
                     THEN Auto
                     THEN (RWW "filter_append_sq" 0
                     THENM (Reduce 0 THEN (AutoSplit THENM RWW "length-append" 0 THENM Reduce 0))
                     )
                     THEN Auto
                     THEN Try ((D (-3) THEN Complete (Auto))))⋅
               )⋅
         )⋅) }

1
.....subterm..... T:t
1:n
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List@i
5. ¬(x ∈ ys)
6. y : T@i
7. (x ∈ ys @ [y])
8. 0 < ||filter(λy.(eq y x);ys @ [y])||
9. apply-alist(eq;count-repeats(ys,eq);x) = (inr ⋅ ) ∈ (ℕ+?)
10. y = x ∈ T
⊢ 1 = (||filter(λy.(eq y x);ys)|| + 1) ∈ ℕ+

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List@i
5. ¬(x ∈ ys)
6. y : T@i
7. ¬(y = x ∈ T)
8. (x ∈ ys @ [y])
9. 0 < ||filter(λy.(eq y x);ys @ [y])||
10. apply-alist(eq;count-repeats(ys,eq);x) = (inr ⋅ ) ∈ (ℕ+?)
⊢ (inr ⋅ ) = (inl (||filter(λy.(eq y x);ys)|| + 0)) ∈ (ℕ+?)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
\mvdash{}  \mforall{}ys:T  List.  \mforall{}y:T.
        ((apply-alist(eq;count-repeats(ys,eq);x)
        =  if  x  \mmember{}\msubb{}  ys  then  inl  ||filter(\mlambda{}y.(eq  y  x);ys)||  else  inr  \mcdot{}    fi  )
        {}\mRightarrow{}  (apply-alist(eq;count-repeats(ys  @  [y],eq);x)
              =  if  x  \mmember{}\msubb{}  ys  @  [y]  then  inl  ||filter(\mlambda{}y.(eq  y  x);ys  @  [y])||  else  inr  \mcdot{}    fi  ))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (AutoSplit
              THENL  [TACTIC:(Assert  0  <  ||filter(\mlambda{}y.(eq  y  x);ys)||  BY
                                                        (BLemma  `member-exists2`
                                                          THEN  Auto
                                                          THEN  (RWO  "member\_filter"  0  THENA  Auto)
                                                          THEN  Reduce  0
                                                          THEN  Auto))
                          ;  TACTIC:  Id]
  )
  THEN  ((((D  0  THENA  Auto)  THEN  AutoSplit)
                THENL  [TACTIC:(RenameVar  `y'  (-2)
                                              THEN  (Assert  0  <  ||filter(\mlambda{}y.(eq  y  x);ys  @  [y])||  BY
                                                                      (BLemma  `member-exists2`
                                                                        THEN  Auto
                                                                        THEN  (RWO  "member\_filter"  0  THENA  Auto)
                                                                        THEN  Reduce  0
                                                                        THEN  Auto))
                                              )
                            ;  TACTIC:Try  ((D  (-1)  THEN  Complete  (Auto)))\mcdot{}]
              )
              THEN  ((D  0  THENA  Auto)
                          THEN  (Unfold  `count-repeats`  0
                                      THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
                                      THEN  Fold  `count-repeats`  0
                                      THEN  Reduce  0
                                      THEN  (RWO  "apply-updated-alist"  0\mcdot{}  THENA  Auto)
                                      THEN  (HypSubst  (-1)  0  THENM  Reduce  0)
                                      THEN  Auto
                                      THEN  (RWW  "filter\_append\_sq"  0
                                      THENM  (Reduce  0  THEN  (AutoSplit  THENM  RWW  "length-append"  0  THENM  Reduce  0))
                                      )
                                      THEN  Auto
                                      THEN  Try  ((D  (-3)  THEN  Complete  (Auto))))\mcdot{}
                          )\mcdot{}
              )\mcdot{})

---

Home Index