---

Step * of Lemma add-nat-missing-prop

∀s:nat-missing-type(). ∀x,y:ℕ.
  (↑member-nat-missing(x;add-nat-missing(y;s)) ⇐⇒ (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s)))
BY
{ Auto }

1
1. s : nat-missing-type()@i
2. x : ℕ@i
3. y : ℕ@i
4. ↑member-nat-missing(x;add-nat-missing(y;s))@i
⊢ (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s))

2
1. s : nat-missing-type()@i
2. x : ℕ@i
3. y : ℕ@i
4. (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s))@i
⊢ ↑member-nat-missing(x;add-nat-missing(y;s))

---

Latex:


\mforall{}s:nat-missing-type().  \mforall{}x,y:\mBbbN{}.
    (\muparrow{}member-nat-missing(x;add-nat-missing(y;s))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (\muparrow{}member-nat-missing(x;s)))


By

Auto

---

Home Index