---

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


∀k:ℕ. ∀v1,v2,F:ℚCube(k) List.
  (no_repeats(ℚCube(k);v1)
  ⇒ no_repeats(ℚCube(k);v2)
  ⇒ (↑isEven(||v1||))
  ⇒ (∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ F))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ F))))
  ⇒ (↑isEven(||F||))
  ⇒ no_repeats(ℚCube(k);F)
  ⇒ (↑isEven(||v2||)))
BY
{ 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)
⊢ ↑isEven(||v2||)

---

Latex:

---

Latex:

\mforall{}k:\mBbbN{}.  \mforall{}v1,v2,F:\mBbbQ{}Cube(k)  List.
    (no\_repeats(\mBbbQ{}Cube(k);v1)
    {}\mRightarrow{}  no\_repeats(\mBbbQ{}Cube(k);v2)
    {}\mRightarrow{}  (\muparrow{}isEven(||v1||))
    {}\mRightarrow{}  (\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))))
    {}\mRightarrow{}  (\muparrow{}isEven(||F||))
    {}\mRightarrow{}  no\_repeats(\mBbbQ{}Cube(k);F)
    {}\mRightarrow{}  (\muparrow{}isEven(||v2||)))


By

---

Latex:
Auto

---

Home Index