---

Step * 2 1 1 of Lemma half-cubes-listable


1. k : ℤ
2. [%1] : 0 < k
3. c : {c:ℚCube(k)| ↑Inhabited(c)} 
4. ℚCube(k) ⊆r ℚCube(k - 1)
5. {c:ℚCube(k)| ↑Inhabited(c)}  ⊆r {c:ℚCube(k - 1)| ↑Inhabited(c)} 
6. L : ℚCube(k - 1) List
7. [%5] : no_repeats(ℚCube(k - 1);L) ∧ (∀h:ℚCube(k - 1). ((h ∈ L) ⇐⇒ ↑is-half-cube(k - 1;h;c)))
8. v1 : ℚ
9. v2 : ℚ
10. (c (k - 1)) = <v1, v2> ∈ ℚInterval
11. v1 < v2
⊢ ∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))]
BY
{ ((Assert λh,i. if i <z k - 1 then h i else <v1, qavg(v1;v2)> fi  ∈ ℚCube(k - 1) ⟶ ℚCube(k) BY
          (((FunExt THENM Reduce 0) THEN Unfold `rational-cube` 0) THEN Auto))
   THEN (Assert λh,i. if i <z k - 1 then h i else <qavg(v1;v2), v2> fi  ∈ ℚCube(k - 1) ⟶ ℚCube(k) BY
               (((FunExt THENM Reduce 0) THEN Unfold `rational-cube` 0) THEN Auto))
   ) }

1
1. k : ℤ
2. [%1] : 0 < k
3. c : {c:ℚCube(k)| ↑Inhabited(c)} 
4. ℚCube(k) ⊆r ℚCube(k - 1)
5. {c:ℚCube(k)| ↑Inhabited(c)}  ⊆r {c:ℚCube(k - 1)| ↑Inhabited(c)} 
6. L : ℚCube(k - 1) List
7. [%5] : no_repeats(ℚCube(k - 1);L) ∧ (∀h:ℚCube(k - 1). ((h ∈ L) ⇐⇒ ↑is-half-cube(k - 1;h;c)))
8. v1 : ℚ
9. v2 : ℚ
10. (c (k - 1)) = <v1, v2> ∈ ℚInterval
11. v1 < v2
12. λh,i. if i <z k - 1 then h i else <v1, qavg(v1;v2)> fi  ∈ ℚCube(k - 1) ⟶ ℚCube(k)
13. λh,i. if i <z k - 1 then h i else <qavg(v1;v2), v2> fi  ∈ ℚCube(k - 1) ⟶ ℚCube(k)
⊢ ∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))]

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  [\%1]  :  0  <  k
3.  c  :  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\} 
4.  \mBbbQ{}Cube(k)  \msubseteq{}r  \mBbbQ{}Cube(k  -  1)
5.  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    \msubseteq{}r  \{c:\mBbbQ{}Cube(k  -  1)|  \muparrow{}Inhabited(c)\} 
6.  L  :  \mBbbQ{}Cube(k  -  1)  List
7.  [\%5]  :  no\_repeats(\mBbbQ{}Cube(k  -  1);L)  \mwedge{}  (\mforall{}h:\mBbbQ{}Cube(k  -  1).  ((h  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}is-half-cube(k  -  1;h;c)))
8.  v1  :  \mBbbQ{}
9.  v2  :  \mBbbQ{}
10.  (c  (k  -  1))  =  <v1,  v2>
11.  v1  <  v2
\mvdash{}  \mexists{}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:
((Assert  \mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  <v1,  qavg(v1;v2)>  fi    \mmember{}  \mBbbQ{}Cube(k  -  1)  {}\mrightarrow{}  \mBbbQ{}Cube(k)  BY
                (((FunExt  THENM  Reduce  0)  THEN  Unfold  `rational-cube`  0)  THEN  Auto))
  THEN  (Assert  \mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  <qavg(v1;v2),  v2>  fi    \mmember{}  \mBbbQ{}Cube(k  -  1)  {}\mrightarrow{}  \mBbbQ{}Cube(k)  BY
                          (((FunExt  THENM  Reduce  0)  THEN  Unfold  `rational-cube`  0)  THEN  Auto))
  )

---

Home Index