---

Step * 2 of Lemma cantor2baire2cantor


1. a : ℕ ⟶ 𝔹
2. initF(a)
3. x : ℕ
4. ¬(x = 0 ∈ ℕ)
⊢ if (cantor2baire-aux(a;x) =z cantor2baire-aux(a;x-1)) then ff else tt fi  = a x
BY
{ ((InstLemma `cantor2baire-aux-pos` [⌜a⌝;⌜x⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  initF(a)
3.  x  :  \mBbbN{}
4.  \mneg{}(x  =  0)
\mvdash{}  if  (cantor2baire-aux(a;x)  =\msubz{}  cantor2baire-aux(a;x-1))  then  ff  else  tt  fi    =  a  x


By

---

Latex:
((InstLemma  `cantor2baire-aux-pos`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  AutoSplit)

---

Home Index