---

Step * of Lemma member-rat-complex-subdiv

∀k:ℕ. ∀K:{c:ℚCube(k)| ↑Inhabited(c)}  List. ∀c:ℚCube(k).
  ((c ∈ (K)') ⇐⇒ ∃a:ℚCube(k). ((a ∈ K) ∧ (↑is-half-cube(k;c;a))))
BY
{ (Auto
   THEN ((Unfold `rat-complex-subdiv` -1
          THEN (RWO "member-concat" (-1) THENA Auto)
          THEN (RWO "member_map" (-1) THENA Auto)
          THEN Reduce -1)
         ORELSE (Unfold `rat-complex-subdiv` 0
                 THEN (RWO "member-concat" 0 THENA Auto)
                 THEN (RWO "member_map" 0 THENA Auto)
                 THEN Reduce 0)
         ORELSE ProveWfLemma)
   ) }

1
1. k : ℕ
2. K : {c:ℚCube(k)| ↑Inhabited(c)}  List
3. c : ℚCube(k)
4. ∃l:ℚCube(k) List
    ((∃y:{c:ℚCube(k)| ↑Inhabited(c)} . ((y ∈ K) ∧ (l = half-cubes-of(k;y) ∈ (ℚCube(k) List)))) ∧ (c ∈ l))
⊢ ∃a:ℚCube(k). ((a ∈ K) ∧ (↑is-half-cube(k;c;a)))

2
1. k : ℕ
2. K : {c:ℚCube(k)| ↑Inhabited(c)}  List
3. c : ℚCube(k)
4. ∃a:ℚCube(k). ((a ∈ K) ∧ (↑is-half-cube(k;c;a)))
⊢ ∃l:ℚCube(k) List. ((∃y:{c:ℚCube(k)| ↑Inhabited(c)} . ((y ∈ K) ∧ (l = half-cubes-of(k;y) ∈ (ℚCube(k) List)))) ∧ (c ∈ l)\000C)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}K:\{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    List.  \mforall{}c:\mBbbQ{}Cube(k).
    ((c  \mmember{}  (K)')  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\mBbbQ{}Cube(k).  ((a  \mmember{}  K)  \mwedge{}  (\muparrow{}is-half-cube(k;c;a))))


By

---

Latex:
(Auto
  THEN  ((Unfold  `rat-complex-subdiv`  -1
                THEN  (RWO  "member-concat"  (-1)  THENA  Auto)
                THEN  (RWO  "member\_map"  (-1)  THENA  Auto)
                THEN  Reduce  -1)
              ORELSE  (Unfold  `rat-complex-subdiv`  0
                              THEN  (RWO  "member-concat"  0  THENA  Auto)
                              THEN  (RWO  "member\_map"  0  THENA  Auto)
                              THEN  Reduce  0)
              ORELSE  ProveWfLemma)
  )

---

Home Index