---

Step * 2 of Lemma equipollent-nat-union-nsub


1. k : ℕ+
2. b : ℕ + ℕk
⊢ ∃a:ℕ. (if a <z k then inr a  else inl (a - k) fi  = b ∈ (ℕ + ℕk))
BY
{ ((With ⌜case b of inl(x) => x + k | inr(y) => y⌝ (D 0)⋅ THEN Auto)
   THEN D -1
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  b  :  \mBbbN{}  +  \mBbbN{}k
\mvdash{}  \mexists{}a:\mBbbN{}.  (if  a  <z  k  then  inr  a    else  inl  (a  -  k)  fi    =  b)


By

---

Latex:
((With  \mkleeneopen{}case  b  of  inl(x)  =>  x  +  k  |  inr(y)  =>  y\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto')

---

Home Index