---

Step * of Lemma length-eq-lists-diff-elts

∀[T:Type]
  ∀eq:∀x,y:T.  Dec(x = y ∈ T). ∀L1,L2:T List.
    (no_repeats(T;L1) ⇒ (||L1|| ≥ ||L2|| ) ⇒ (∃x:T. ((x ∈ L2) ∧ (¬(x ∈ L1)))) ⇒ (∃x:T. ((x ∈ L1) ∧ (¬(x ∈ L2)))))
BY
{ (Auto
   THEN (Assert Dec((∃x∈L1. ¬(x ∈ L2))) BY
               (BLemma `decidable__l_exists` THEN Auto))
   THEN D -1
   THEN BLemma `l_exists_iff`
   THEN Auto
   THEN (RWO "not-l_exists" (-1) THENA Auto)
   THEN (RWO "l_all_iff" (-1) THENA Auto)
   THEN ExRepD
   THEN (FLemma `deq-exists` [2] THENA Auto)
   THEN RenameVar `=' (-1)
   THEN (Assert ∀i:ℕ||L1||. ∃j:ℕ||filter(λy.(¬b(= y x));L2)||. (L1[i] = filter(λy.(¬b(= y x));L2)[j] ∈ T) BY
               (Auto
                THEN (InstHyp [⌜L1[i]⌝] (-3)⋅ THENA Auto)
                THEN (Assert Dec((L1[i] ∈ filter(λy.(¬b(= y x));L2))) BY
                            (BLemma `decidable__l_member` THEN Auto))
                THEN D -1
                THEN Auto
                THEN Try ((RepeatFor 2 (D -1) THEN Complete (Auto)))
                THEN D -2
                THEN (D 0 THENA Auto)
                THEN D -2
                THEN BLemma `member_filter`
                THEN Reduce 0
                THEN Auto))) }

1
1. [T] : Type
2. eq : ∀x,y:T.  Dec(x = y ∈ T)@i
3. L1 : T List@i
4. L2 : T List@i
5. no_repeats(T;L1)@i
6. ||L1|| ≥ ||L2|| @i
7. x : T@i
8. (x ∈ L2)@i
9. ¬(x ∈ L1)@i
10. ∀x:T. ((x ∈ L1) ⇒ (¬¬(x ∈ L2)))
11. = : EqDecider(T)
12. ∀i:ℕ||L1||. ∃j:ℕ||filter(λy.(¬b(= y x));L2)||. (L1[i] = filter(λy.(¬b(= y x));L2)[j] ∈ T)
⊢ (∃x∈L1. ¬(x ∈ L2))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:\mforall{}x,y:T.    Dec(x  =  y).  \mforall{}L1,L2:T  List.
        (no\_repeats(T;L1)
        {}\mRightarrow{}  (||L1||  \mgeq{}  ||L2||  )
        {}\mRightarrow{}  (\mexists{}x:T.  ((x  \mmember{}  L2)  \mwedge{}  (\mneg{}(x  \mmember{}  L1))))
        {}\mRightarrow{}  (\mexists{}x:T.  ((x  \mmember{}  L1)  \mwedge{}  (\mneg{}(x  \mmember{}  L2)))))


By

---

Latex:
(Auto
  THEN  (Assert  Dec((\mexists{}x\mmember{}L1.  \mneg{}(x  \mmember{}  L2)))  BY
                          (BLemma  `decidable\_\_l\_exists`  THEN  Auto))
  THEN  D  -1
  THEN  BLemma  `l\_exists\_iff`
  THEN  Auto
  THEN  (RWO  "not-l\_exists"  (-1)  THENA  Auto)
  THEN  (RWO  "l\_all\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (FLemma  `deq-exists`  [2]  THENA  Auto)
  THEN  RenameVar  `='  (-1)
  THEN  (Assert  \mforall{}i:\mBbbN{}||L1||
                                \mexists{}j:\mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||.  (L1[i]  =  filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)[j])  BY
                          (Auto
                            THEN  (InstHyp  [\mkleeneopen{}L1[i]\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
                            THEN  (Assert  Dec((L1[i]  \mmember{}  filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)))  BY
                                                    (BLemma  `decidable\_\_l\_member`  THEN  Auto))
                            THEN  D  -1
                            THEN  Auto
                            THEN  Try  ((RepeatFor  2  (D  -1)  THEN  Complete  (Auto)))
                            THEN  D  -2
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -2
                            THEN  BLemma  `member\_filter`
                            THEN  Reduce  0
                            THEN  Auto)))

---

Home Index