---

Step * 1 1 1 1 1 1 1 1 1 of Lemma length-rat-complex-boundary-even


1. k : ℕ
2. v1 : ℚCube(k) List
3. v2 : ℚCube(k) List
4. F : ℚCube(k) List
5. no_repeats(ℚCube(k);v1)
6. no_repeats(ℚCube(k);v2)
7. ↑isEven(||v1||)
8. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ F))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ F)))
9. ↑isEven(||F||)
10. no_repeats(ℚCube(k);F)
11. d1 : ∀f:ℚCube(k). Dec((f ∈ F))
12. d2 : ∀f:ℚCube(k). Dec((f ∈ v2))
⊢ ↑isEven(||v2||)
BY
{ (InstLemma `filter-split-length` [⌜ℚCube(k)⌝;⌜λ2x.isl(d1 x)⌝;⌜v2⌝]⋅ THENA Auto) }

1
1. k : ℕ
2. v1 : ℚCube(k) List
3. v2 : ℚCube(k) List
4. F : ℚCube(k) List
5. no_repeats(ℚCube(k);v1)
6. no_repeats(ℚCube(k);v2)
7. ↑isEven(||v1||)
8. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ F))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ F)))
9. ↑isEven(||F||)
10. no_repeats(ℚCube(k);F)
11. d1 : ∀f:ℚCube(k). Dec((f ∈ F))
12. d2 : ∀f:ℚCube(k). Dec((f ∈ v2))
13. (||filter(λx.isl(d1 x);v2)|| + ||filter(λx.(¬bisl(d1 x));v2)||) = ||v2|| ∈ ℤ
⊢ ↑isEven(||v2||)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  v1  :  \mBbbQ{}Cube(k)  List
3.  v2  :  \mBbbQ{}Cube(k)  List
4.  F  :  \mBbbQ{}Cube(k)  List
5.  no\_repeats(\mBbbQ{}Cube(k);v1)
6.  no\_repeats(\mBbbQ{}Cube(k);v2)
7.  \muparrow{}isEven(||v1||)
8.  \mforall{}f:\mBbbQ{}Cube(k).  ((f  \mmember{}  v1)  \mLeftarrow{}{}\mRightarrow{}  ((f  \mmember{}  v2)  \mwedge{}  (\mneg{}(f  \mmember{}  F)))  \mvee{}  ((\mneg{}(f  \mmember{}  v2))  \mwedge{}  (f  \mmember{}  F)))
9.  \muparrow{}isEven(||F||)
10.  no\_repeats(\mBbbQ{}Cube(k);F)
11.  d1  :  \mforall{}f:\mBbbQ{}Cube(k).  Dec((f  \mmember{}  F))
12.  d2  :  \mforall{}f:\mBbbQ{}Cube(k).  Dec((f  \mmember{}  v2))
\mvdash{}  \muparrow{}isEven(||v2||)


By

---

Latex:
(InstLemma  `filter-split-length`  [\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.isl(d1  x)\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index