---

Step * 2 3 1 1 of Lemma padic-ring_wf


1. p : {2...}
2. X : basic-padic(p)@i
3. Y : basic-padic(p)@i
4. Z : basic-padic(p)@i
⊢ bpa-mul(p;bpa-mul(p;X;Y);Z) = bpa-mul(p;X;bpa-mul(p;Y;Z)) ∈ basic-padic(p)
BY
{ ((D -3 THEN D -2 THEN D -1) THEN RepUR ``bpa-mul basic-padic`` 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  X  :  basic-padic(p)@i
3.  Y  :  basic-padic(p)@i
4.  Z  :  basic-padic(p)@i
\mvdash{}  bpa-mul(p;bpa-mul(p;X;Y);Z)  =  bpa-mul(p;X;bpa-mul(p;Y;Z))


By

---

Latex:
((D  -3  THEN  D  -2  THEN  D  -1)  THEN  RepUR  ``bpa-mul  basic-padic``  0  THEN  EqCD  THEN  Auto)

---

Home Index