Step * 2 of Lemma cantor2baire2cantor


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