---

Step * of Lemma half-cubes_wf

∀[k:ℕ]
  (half-cubes(k) ∈ c:{c:ℚCube(k)| ↑Inhabited(c)}  ⟶ {L:ℚCube(k) List| 
                                   no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c)))} )
BY
{ (Fold `all` 0
   THEN Fold `sq_exists` 0
   THEN (D 0 THENA Auto)
   THEN (Subst' half-cubes(k) ~ TERMOF{half-cubes-listable-ext:o, \\v:l} k 0 THENA Computation)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}]
    (half-cubes(k)  \mmember{}  c:\{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    {}\mrightarrow{}  \{L:\mBbbQ{}Cube(k)  List| 
                                                                      no\_repeats(\mBbbQ{}Cube(k);L)
                                                                      \mwedge{}  (\mforall{}h:\mBbbQ{}Cube(k).  ((h  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}is-half-cube(k;h;c)))\}  )


By

---

Latex:
(Fold  `all`  0
  THEN  Fold  `sq\_exists`  0
  THEN  (D  0  THENA  Auto)
  THEN  (Subst'  half-cubes(k)  \msim{}  TERMOF\{half-cubes-listable-ext:o,  \mbackslash{}\mbackslash{}v:l\}  k  0  THENA  Computation)
  THEN  Auto)

---

Home Index