[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 58 from proof encode (previous step)

# buf3 = ENCODED_VOLID_SIZE + n2, # buf = # buf4, # buf4 = (# buf2 + ENCODED_VOLID_SIZE + n2) + ENCODED_NAT_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf5 = # buf4, # buf6 = # buf4, subarray(buf4, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2) = subarray(buf, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2), subarray(buf5, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, n2) = subarray(buf3, ENCODED_VOLID_SIZE, n2), subarray(buf5, 0, ENCODED_NAT_SIZE + # buf2) = buf0 + buf2, subarray(buf6, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf4 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE) = subarray(buf5, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf4 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE), subarray(buf6, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) = subarray(buf5, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE), is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf5, ENCODED_NAT_SIZE + # buf2, ENCODED_VOLID_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + ENCODED_VOLID_SIZE + n2, # vtbl1 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ ENCODED_VOLID_SIZE + n2, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err = ESUCCESS → is-encoded(vtbl1[v], subarray(buf6, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)) ∧ n3 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ , err = ESUCCESS ∨ ⌊err⌋ ⊦ vtbl1 = ∅, v ∈ vtbl, (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → (∃ buf0, buf1, buf, vtbl3. buf6 = buf0 + buf1 + buf ∧ vtbl1 ∪ vtbl = (vtbl1 -- v) ∪ vtbl3 ∧ vtbl1 -- v ⊥ vtbl3 ∧ # buf0 + # buf1 = ((ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) + n3 ∧ #(vtbl1 -- v) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf ∧ is-encoded(#((vtbl1 -- v) ∪ vtbl3), buf0) ∧ is-encoded-rec(vtbl3, buf1))) ∧ #(vtbl1 -- v) < # vtbl1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 59:
# buf3 = ENCODED_VOLID_SIZE + n2, # buf = # buf4, # buf4 = (# buf2 + ENCODED_VOLID_SIZE + n2) + ENCODED_NAT_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf5 = # buf4, # buf6 = # buf4, subarray(buf4, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2) = subarray(buf, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2), subarray(buf5, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, n2) = subarray(buf3, ENCODED_VOLID_SIZE, n2), subarray(buf5, 0, ENCODED_NAT_SIZE + # buf2) = buf0 + buf2, subarray(buf6, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf4 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE) = subarray(buf5, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf4 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE), subarray(buf6, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) = subarray(buf5, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE), is-encoded(vtbl1[v], subarray(buf6, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf5, ENCODED_NAT_SIZE + # buf2, ENCODED_VOLID_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + ENCODED_VOLID_SIZE + n2, # vtbl1 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ ENCODED_VOLID_SIZE + n2, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, v ∈ vtbl, ∃ buf1, buf7, buf8, vtbl0. buf6 = buf1 + buf7 + buf8 ∧ vtbl1 ∪ vtbl = (vtbl1 -- v) ∪ vtbl0 ∧ vtbl1 -- v ⊥ vtbl0 ∧ # buf1 + # buf7 = 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ∧ (# vtbl1 - 1) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf8 ∧ is-encoded(#((vtbl1 -- v) ∪ vtbl0), buf1) ∧ is-encoded-rec(vtbl0, buf7)

Rule argument

Additional information

Used simplifier rules: ⊦ m + m = 2 * m; (s)% ⊦ # subarray(buf, m, n) = n; (s)%is-encoded-size: ⊦ is-encoded(n, buf) → # buf = ENCODED_NAT_SIZE; (forward) from specification encoding-fixed-size[encoding-nat]%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ ¬ n < n; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ # vtbl = 0 ↔ vtbl = ∅; (s)% ⊦ m < 1 ↔ m = 0; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ n -1 = n - 1; (s)% ⊦ v ∈ vtbl → #(vtbl -- v) = (# vtbl)-1; (s)