---

Step * of Lemma pa-sep-or

∀[p:{2...}]. ∀x,y:basic-padic(p).  (pa-sep(p;x;y) ⇒ (∀z:basic-padic(p). (pa-sep(p;z;x) ∨ pa-sep(p;z;y))))
BY
{ (Auto
   THEN DVar`x'
   THEN DVar
   `y'⋅
   THEN DVar `z'
   THEN All  (RepUR ``pa-sep``)
   THEN D -3
   THEN Decide ⌜z1 = y1 ∈ ℤ⌝⋅
   THEN Auto
   THEN Decide ⌜z1 = x1 ∈ ℤ⌝⋅
   THEN Auto) }

1
1. [p] : {2...}
2. x1 : ℕ
3. x2 : p-adics(p)
4. y1 : ℕ
5. y2 : p-adics(p)
6. p-sep(x2;y2)
7. z1 : ℕ
8. z2 : p-adics(p)
9. z1 = y1 ∈ ℤ
10. z1 = x1 ∈ ℤ
⊢ ((¬(z1 = x1 ∈ ℤ)) ∨ p-sep(z2;x2)) ∨ (¬(z1 = y1 ∈ ℤ)) ∨ p-sep(z2;y2)

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}]
    \mforall{}x,y:basic-padic(p).    (pa-sep(p;x;y)  {}\mRightarrow{}  (\mforall{}z:basic-padic(p).  (pa-sep(p;z;x)  \mvee{}  pa-sep(p;z;y))))


By

---

Latex:
(Auto
  THEN  DVar`x'
  THEN  DVar
  `y'\mcdot{}
  THEN  DVar  `z'
  THEN  All    (RepUR  ``pa-sep``)
  THEN  D  -3
  THEN  Decide  \mkleeneopen{}z1  =  y1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Decide  \mkleeneopen{}z1  =  x1\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index