---

Step * of Lemma l_intersection-size

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:T List].
  (no_repeats(T;a) ⇒ no_repeats(T;b) ⇒ a ⊆ c ⇒ b ⊆ c ⇒ ((||a|| + ||b||) ≤ (||c|| + ||(a ⋂ b)||)))
BY
{ TACTIC:(Auto
          THEN (Assert no_repeats(T;(a ⋂ b)) BY
                      (Unfold `l_intersection` 0 THEN Auto))
          THEN (Assert ∃f:ℕ||a|| ⟶ ℕ||c||. ∀i:ℕ||a||. (a[i] = c[f i] ∈ T) BY
                      (RepUR ``l_contains l_all l_member`` 8
                       THEN (Skolemize  8 `f' THENA Auto)
                       THEN With ⌜f⌝ (D 0)⋅
                       THEN Auto
                       THEN ExtWith [`i'] [⌜i@0:ℕ||a|| ⟶ ℕ⌝]⋅
                       THEN Auto))
          THEN (Assert ∃g:ℕ||b|| ⟶ ℕ||c||. ∀i:ℕ||b||. (b[i] = c[g i] ∈ T) BY
                      (RepUR ``l_contains l_all l_member`` 9
                       THEN (Skolemize  9 `g' THENA Auto)
                       THEN With ⌜g⌝ (D 0)⋅
                       THEN Auto
                       THEN ExtWith [`i'] [⌜i@0:ℕ||b|| ⟶ ℕ⌝]⋅
                       THEN Auto))
          THEN (InstLemma `no_repeats_l_index-inj` [⌜T⌝;⌜eq⌝;⌜(a ⋂ b)⌝]⋅ THENA Auto)
          THEN ExRepD) }

1
1. T : Type
2. eq : EqDecider(T)
3. a : T List
4. b : T List
5. c : T List
6. no_repeats(T;a)
7. no_repeats(T;b)
8. a ⊆ c
9. b ⊆ c
10. no_repeats(T;(a ⋂ b))
11. f : ℕ||a|| ⟶ ℕ||c||
12. ∀i:ℕ||a||. (a[i] = c[f i] ∈ T)
13. g : ℕ||b|| ⟶ ℕ||c||
14. ∀i:ℕ||b||. (b[i] = c[g i] ∈ T)
15. Inj({x:T| (x ∈ (a ⋂ b))} ;ℕ||(a ⋂ b)||;λx.index((a ⋂ b);x))
⊢ (||a|| + ||b||) ≤ (||c|| + ||(a ⋂ b)||)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b,c:T  List].
    (no\_repeats(T;a)
    {}\mRightarrow{}  no\_repeats(T;b)
    {}\mRightarrow{}  a  \msubseteq{}  c
    {}\mRightarrow{}  b  \msubseteq{}  c
    {}\mRightarrow{}  ((||a||  +  ||b||)  \mleq{}  (||c||  +  ||(a  \mcap{}  b)||)))


By

---

Latex:
TACTIC:(Auto
                THEN  (Assert  no\_repeats(T;(a  \mcap{}  b))  BY
                                        (Unfold  `l\_intersection`  0  THEN  Auto))
                THEN  (Assert  \mexists{}f:\mBbbN{}||a||  {}\mrightarrow{}  \mBbbN{}||c||.  \mforall{}i:\mBbbN{}||a||.  (a[i]  =  c[f  i])  BY
                                        (RepUR  ``l\_contains  l\_all  l\_member``  8
                                          THEN  (Skolemize    8  `f'  THENA  Auto)
                                          THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}
                                          THEN  Auto
                                          THEN  ExtWith  [`i']  [\mkleeneopen{}i@0:\mBbbN{}||a||  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}]\mcdot{}
                                          THEN  Auto))
                THEN  (Assert  \mexists{}g:\mBbbN{}||b||  {}\mrightarrow{}  \mBbbN{}||c||.  \mforall{}i:\mBbbN{}||b||.  (b[i]  =  c[g  i])  BY
                                        (RepUR  ``l\_contains  l\_all  l\_member``  9
                                          THEN  (Skolemize    9  `g'  THENA  Auto)
                                          THEN  With  \mkleeneopen{}g\mkleeneclose{}  (D  0)\mcdot{}
                                          THEN  Auto
                                          THEN  ExtWith  [`i']  [\mkleeneopen{}i@0:\mBbbN{}||b||  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}]\mcdot{}
                                          THEN  Auto))
                THEN  (InstLemma  `no\_repeats\_l\_index-inj`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}(a  \mcap{}  b)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD)

---

Home Index