| # ns1 = 2 + m0, # buf3 = m0 * ENCODED_NAT_SIZE, # ns = m0 + 1, # buf2 = ENCODED_NAT_SIZE, # buf1 = ENCODED_NAT_SIZE, m0 + 1 = #((ns -- n1) ++ n), n0 ≠ n1 ∧ n0 ∈ ns1 ↔ n0 = n ∨ n0 ≠ n1 ∧ n0 ∈ ns, is-encoded(ns -- n1, buf3), is-encoded(n1, buf2), is-encoded((ns -- n1) ++ n, buf3 + buf1), is-encoded(n, buf1), n ∈ ns1, n1 ∈ ns1, n1 ∈ ns, ∀ ns0, buf0, ns, buf1, n. # ns0 < (m0 + 1) + 1 → # buf0 = # ns * ENCODED_NAT_SIZE ∧ # buf1 = ENCODED_NAT_SIZE ∧ is-encoded(n, buf1) ∧ is-encoded(ns, buf0) → (is-encoded(ns0, buf0 + buf1) ↔ ns0 = ns ++ n) ∨ n ∈ ns ⊦ n0 ∈ ns1 ↔ n0 = n ∨ n0 ∈ ns, ns = ∅, ns1 = ∅, n ∈ ns |