---

Step * 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)
⊢ ↑isEven(||v2||)
BY
{ (((Assert ∀f:ℚCube(k). Dec((f ∈ F)) BY Auto) THEN RenameVar `d1' (-1))
   THEN (Assert ∀f:ℚCube(k). Dec((f ∈ v2)) BY
               Auto)
   THEN RenameVar `d2' (-1)) }

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))
⊢ ↑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)
\mvdash{}  \muparrow{}isEven(||v2||)


By

---

Latex:
(((Assert  \mforall{}f:\mBbbQ{}Cube(k).  Dec((f  \mmember{}  F))  BY  Auto)  THEN  RenameVar  `d1'  (-1))
  THEN  (Assert  \mforall{}f:\mBbbQ{}Cube(k).  Dec((f  \mmember{}  v2))  BY
                          Auto)
  THEN  RenameVar  `d2'  (-1))

---

Home Index