---

Step * of Lemma half-cubes-of_wf

∀[k:ℕ]. ∀[c:{c:ℚCube(k)| ↑Inhabited(c)} ].
  (half-cubes-of(k;c) ∈ {L:ℚCube(k) List| no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c)))} )
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}  ].
    (half-cubes-of(k;c)  \mmember{}  \{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:
ProveWfLemma

---

Home Index