[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 84 from proof encode (previous step)

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

User applied rule exists right

And obtained the following new goals

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

Rule argument

pos: right 3 terms: buf0, buf2 + subarray(buf9, 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE), subarray (buf9, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE, # buf9 - ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE), vtbl[v, vtbl1[v]] abort: F discard: T computed: F

Additional information

Used terms: buf0, buf2 + subarray(buf9, 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE), subarray (buf9, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE, # buf9 - ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE), vtbl[v, vtbl1[v]]