---

Step * of Lemma bpa-norm-equiv

∀p:{2...}. ∀x:basic-padic(p).  bpa-equiv(p;x;bpa-norm(p;x))
BY
{ (Intros THEN D -1 THEN RepUR ``bpa-norm bpa-equiv`` 0 THEN Auto) }

1
1. p : {2...}
2. x1 : ℕ
3. x2 : p-adics(p)
⊢ let m,b = if (x1 =z 0) then <0, x2>
  if (x2 x1 =z 0) then <0, p-shift(p;x2;x1)>
  else let k,b = p-unitize(p;x2;x1) 
       in <x1 - k, b>
  fi  
  in p^m(p) * x2 = p^x1(p) * b ∈ p-adics(p)

---

Latex:

---

Latex:
\mforall{}p:\{2...\}.  \mforall{}x:basic-padic(p).    bpa-equiv(p;x;bpa-norm(p;x))


By

---

Latex:
(Intros  THEN  D  -1  THEN  RepUR  ``bpa-norm  bpa-equiv``  0  THEN  Auto)

---

Home Index