---

Step * 1 1 of Lemma cantor-interval-inclusion


1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : ℕ ⟶ 𝔹
5. n : ℕ
⊢ ((fst(cantor-interval(a;b;f;n))) ≤ (fst(cantor-interval(a;b;f;n + 1))))
∧ ((fst(cantor-interval(a;b;f;n + 1))) ≤ (snd(cantor-interval(a;b;f;n + 1))))
∧ ((snd(cantor-interval(a;b;f;n + 1))) ≤ (snd(cantor-interval(a;b;f;n))))
BY
{ ((Subst ⌜cantor-interval(a;b;f;n + 1) ~ let a',b' = cantor-interval(a;b;f;n) 
                                          in if f n then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi ⌝ 0⋅
    THENA (RW (AddrC [1] UnfoldTopAbC) 0
           THEN (RWO "primrec-unroll" 0 THENA Auto)
           THEN Fold `cantor-interval` 0
           THEN Reduce 0
           THEN AutoSplit)
    )
   THEN (GenConclTerm ⌜cantor-interval(a;b;f;n)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : ℕ ⟶ 𝔹
5. n : ℕ
6. v1 : ℝ
7. v2 : ℝ
8. cantor-interval(a;b;f;n) = <v1, v2> ∈ (ℝ × ℝ)
⊢ (v1 ≤ (fst(if f n then <(2 * v1 + v2)/3, v2> else <v1, (v1 + 2 * v2)/3> fi )))
∧ ((fst(if f n then <(2 * v1 + v2)/3, v2> else <v1, (v1 + 2 * v2)/3> fi )) ≤ (snd(if f n
  then <(2 * v1 + v2)/3, v2>
  else <v1, (v1 + 2 * v2)/3>
  fi )))
∧ ((snd(if f n then <(2 * v1 + v2)/3, v2> else <v1, (v1 + 2 * v2)/3> fi )) ≤ v2)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  \mleq{}  b
4.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
5.  n  :  \mBbbN{}
\mvdash{}  ((fst(cantor-interval(a;b;f;n)))  \mleq{}  (fst(cantor-interval(a;b;f;n  +  1))))
\mwedge{}  ((fst(cantor-interval(a;b;f;n  +  1)))  \mleq{}  (snd(cantor-interval(a;b;f;n  +  1))))
\mwedge{}  ((snd(cantor-interval(a;b;f;n  +  1)))  \mleq{}  (snd(cantor-interval(a;b;f;n))))


By

---

Latex:
((Subst  \mkleeneopen{}cantor-interval(a;b;f;n  +  1)  \msim{}  let  a',b'  =  cantor-interval(a;b;f;n) 
                                                                                in  if  f  n
                                                                                      then  <(2  *  a'  +  b')/3,  b'>
                                                                                      else  <a',  (a'  +  2  *  b')/3>
                                                                                      fi  \mkleeneclose{}  0\mcdot{}
    THENA  (RW  (AddrC  [1]  UnfoldTopAbC)  0
                  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                  THEN  Fold  `cantor-interval`  0
                  THEN  Reduce  0
                  THEN  AutoSplit)
    )
  THEN  (GenConclTerm  \mkleeneopen{}cantor-interval(a;b;f;n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index