---

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


1. k : ℕ
2. u : ℚCube(k)
3. j : ℕ
4. v1 : ℚCube(k) List
5. no_repeats(ℚCube(k);v1)
6. (∀c,d∈v1.  Compatible(c;d))
7. (∀c∈v1.dim(c) = j ∈ ℤ)
8. v2 : ℚCube(k) List
9. no_repeats(ℚCube(k);v2)
10. (∀c,d∈v2.  Compatible(c;d))
11. (∀c∈v2.dim(c) = j ∈ ℤ)
12. dim(u) = (j + 1) ∈ ℤ
13. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬f ≤ u)) ∨ ((¬(f ∈ v2)) ∧ f ≤ u ∧ (dim(f) = (dim(u) - 1) ∈ ℤ)))
14. ↑isEven(||v1||)
15. ↑Inhabited(u)
16. ∀f:ℚCube(k). ((f ∈ rat-cube-faces(k;u)) ⇐⇒ f ≤ u ∧ (dim(f) = (dim(u) - 1) ∈ ℤ))
17. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ rat-cube-faces(k;u)))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ rat-cube-faces(k;u))))
18. ↑isEven(||rat-cube-faces(k;u)||)
19. no_repeats(ℚCube(k);rat-cube-faces(k;u))
⊢ ↑isEven(||v2||)
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN (GenConcl ⌜rat-cube-faces(k;u) = F ∈ (ℚCube(k) List)⌝⋅ THENA Auto)
   THEN Lemmaize [-5;5;9]) }

1
∀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||)))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  u  :  \mBbbQ{}Cube(k)
3.  j  :  \mBbbN{}
4.  v1  :  \mBbbQ{}Cube(k)  List
5.  no\_repeats(\mBbbQ{}Cube(k);v1)
6.  (\mforall{}c,d\mmember{}v1.    Compatible(c;d))
7.  (\mforall{}c\mmember{}v1.dim(c)  =  j)
8.  v2  :  \mBbbQ{}Cube(k)  List
9.  no\_repeats(\mBbbQ{}Cube(k);v2)
10.  (\mforall{}c,d\mmember{}v2.    Compatible(c;d))
11.  (\mforall{}c\mmember{}v2.dim(c)  =  j)
12.  dim(u)  =  (j  +  1)
13.  \mforall{}f:\mBbbQ{}Cube(k)
            ((f  \mmember{}  v1)  \mLeftarrow{}{}\mRightarrow{}  ((f  \mmember{}  v2)  \mwedge{}  (\mneg{}f  \mleq{}  u))  \mvee{}  ((\mneg{}(f  \mmember{}  v2))  \mwedge{}  f  \mleq{}  u  \mwedge{}  (dim(f)  =  (dim(u)  -  1))))
14.  \muparrow{}isEven(||v1||)
15.  \muparrow{}Inhabited(u)
16.  \mforall{}f:\mBbbQ{}Cube(k).  ((f  \mmember{}  rat-cube-faces(k;u))  \mLeftarrow{}{}\mRightarrow{}  f  \mleq{}  u  \mwedge{}  (dim(f)  =  (dim(u)  -  1)))
17.  \mforall{}f:\mBbbQ{}Cube(k)
            ((f  \mmember{}  v1)
            \mLeftarrow{}{}\mRightarrow{}  ((f  \mmember{}  v2)  \mwedge{}  (\mneg{}(f  \mmember{}  rat-cube-faces(k;u))))  \mvee{}  ((\mneg{}(f  \mmember{}  v2))  \mwedge{}  (f  \mmember{}  rat-cube-faces(k;u))))
18.  \muparrow{}isEven(||rat-cube-faces(k;u)||)
19.  no\_repeats(\mBbbQ{}Cube(k);rat-cube-faces(k;u))
\mvdash{}  \muparrow{}isEven(||v2||)


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}rat-cube-faces(k;u)  =  F\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Lemmaize  [-5;5;9])

---

Home Index