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