---

Step * of Lemma equipollent-nat-union-nsub

∀k:ℕ+. ℕ ~ ℕ + ℕk
BY
{ xxx(Auto
      THEN With ⌜λn.if n <z k then inr n  else inl (n - k) fi ⌝ (D 0)⋅
      THEN Auto
      THEN RepeatFor 2 (D 0⋅)
      THEN (Reduce 0 THENA Auto))xxx }

1
1. k : ℕ+
2. a1 : ℕ
⊢ ∀a2:ℕ
    ((if a1 <z k then inr a1  else inl (a1 - k) fi  = if a2 <z k then inr a2  else inl (a2 - k) fi  ∈ (ℕ + ℕk))
    ⇒ (a1 = a2 ∈ ℕ))

2
1. k : ℕ+
2. b : ℕ + ℕk
⊢ ∃a:ℕ. (if a <z k then inr a  else inl (a - k) fi  = b ∈ (ℕ + ℕk))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}\msupplus{}.  \mBbbN{}  \msim{}  \mBbbN{}  +  \mBbbN{}k


By

---

Latex:
xxx(Auto
        THEN  With  \mkleeneopen{}\mlambda{}n.if  n  <z  k  then  inr  n    else  inl  (n  -  k)  fi  \mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  RepeatFor  2  (D  0\mcdot{})
        THEN  (Reduce  0  THENA  Auto))xxx

---

Home Index