---

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


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)
13. f : i:ℕ||L1|| ─→ ℕ||filter(λy.(¬b(= y x));L2)||
14. ∀i:ℕ||L1||. (L1[i] = filter(λy.(¬b(= y x));L2)[f i] ∈ T)
15. Inj(ℕ||L1||;ℕ||filter(λy.(¬b(= y x));L2)||;f)
⊢ (∃x∈L1. ¬(x ∈ L2))
BY
{ (FLemma `pigeon-hole` [-1]
   THEN Auto
   THEN InstLemma `length-filter-decreases` [⌈T⌉;⌈λy.(¬b(= y x))⌉;⌈L2⌉]⋅
   THEN Auto
   THEN Reduce 0
   THEN (RW assert_pushdownC 0 THENA 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)
13. f : i:ℕ||L1|| ─→ ℕ||filter(λy.(¬b(= y x));L2)||
14. ∀i:ℕ||L1||. (L1[i] = filter(λy.(¬b(= y x));L2)[f i] ∈ T)
15. Inj(ℕ||L1||;ℕ||filter(λy.(¬b(= y x));L2)||;f)
16. ||L1|| ≤ ||filter(λy.(¬b(= y x));L2)||
⊢ (∃x@0∈L2. ¬¬(x@0 = x ∈ T))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  L1  :  T  List@i
4.  L2  :  T  List@i
5.  no\_repeats(T;L1)@i
6.  ||L1||  \mgeq{}  ||L2||  @i
7.  x  :  T@i
8.  (x  \mmember{}  L2)@i
9.  \mneg{}(x  \mmember{}  L1)@i
10.  \mforall{}x:T.  ((x  \mmember{}  L1)  {}\mRightarrow{}  (\mneg{}\mneg{}(x  \mmember{}  L2)))
11.  =  :  EqDecider(T)
12.  \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])
13.  f  :  i:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||
14.  \mforall{}i:\mBbbN{}||L1||.  (L1[i]  =  filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)[f  i])
15.  Inj(\mBbbN{}||L1||;\mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||;f)
\mvdash{}  (\mexists{}x\mmember{}L1.  \mneg{}(x  \mmember{}  L2))


By

---

Latex:
(FLemma  `pigeon-hole`  [-1]
  THEN  Auto
  THEN  InstLemma  `length-filter-decreases`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}y.(\mneg{}\msubb{}(=  y  x))\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index