---

Step * 1 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)
⊢ (∃x∈L1. ¬(x ∈ L2))
BY
{ ((Skolemize (-1) `f' THENA Auto) THEN (Assert Inj(ℕ||L1||;ℕ||filter(λy.(¬b(= y x));L2)||;f) BY (D 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)
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. a1 : ℕ||L1||@i
16. a2 : ℕ||L1||@i
17. (f a1) = (f a2) ∈ ℕ||filter(λy.(¬b(= y x));L2)||@i
⊢ a1 = a2 ∈ ℕ||L1||

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

---

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])
\mvdash{}  (\mexists{}x\mmember{}L1.  \mneg{}(x  \mmember{}  L2))


By

---

Latex:
((Skolemize  (-1)  `f'  THENA  Auto)
  THEN  (Assert  Inj(\mBbbN{}||L1||;\mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||;f)  BY
                          (D  0  THEN  Auto))
  )

---

Home Index