---

Step * of Lemma add-nat-missing_wf

∀[i:ℕ]. ∀[s:nat-missing-type()].  (add-nat-missing(i;s) ∈ nat-missing-type())
BY
{ ProveWfLemma }

1
.....subterm..... T:t
2:n
1. i : ℕ
2. m : {m:ℤ| (-1) ≤ m} 
3. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
4. m <z i ∈ 𝔹
5. m < i
⊢ s1 @ [m + 1, i) ∈ {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < i)} 

2
.....subterm..... T:t
2:n
1. i : ℕ
2. m : {m:ℤ| (-1) ≤ m} 
3. m ≠ i
4. ¬m < i
5. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
6. ff ∈ 𝔹
7. ff ∈ 𝔹
⊢ remove-combine(λx.(x - i);s1) ∈ {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 

---

Latex:


\mforall{}[i:\mBbbN{}].  \mforall{}[s:nat-missing-type()].    (add-nat-missing(i;s)  \mmember{}  nat-missing-type())


By

ProveWfLemma

---

Home Index