[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 53 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, buf1 = buf5, buf5 = buf5, n = ENCODED_VOLID_SIZE, n3 = (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE, n4 = vtbl1[v], 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, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf5, ENCODED_NAT_SIZE + # buf2, ENCODED_VOLID_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, #(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, ((ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) + encoding-size(vtbl1[v]) ≤ # buf5, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ [encode_nat#(vtbl1[v], (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE; buf5, n; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf5 = # buf1 ∧ subarray(buf5, 0, n3) = subarray(buf1, 0, n3) ∧ subarray(buf5, n3 + encoding-size(n4), # buf5 - n3 + encoding-size(n4)) = subarray(buf1, n3 + encoding-size(n4), # buf5 - n3 + encoding-size(n4)) ∧ (err = ESUCCESS → is-encoded(n4, subarray(buf5, n3, encoding-size(n4))) ∧ n = encoding-size(n4)) → ⟪n0 := ((ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) + n; vtbl0 := vtbl1 -- v⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf5 = # buf4 ∧ ( err = ESUCCESS → (∃ buf0, buf2, buf, vtbl3. buf5 = buf0 + buf2 + buf ∧ vtbl1 ∪ vtbl = vtbl0 ∪ vtbl3 ∧ vtbl0 ⊥ vtbl3 ∧ # buf0 + # buf2 = n0 ∧ # vtbl0 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf ∧ is-encoded(#(vtbl0 ∪ vtbl3), buf0) ∧ is-encoded-rec(vtbl3, buf2))) ∧ # vtbl0 < # vtbl1)), vtbl1 = ∅, v ∈ vtbl

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 54:
# buf5 = # buf4, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf0 = ENCODED_NAT_SIZE, # buf4 = (# buf2 + ENCODED_VOLID_SIZE + n2) + ENCODED_NAT_SIZE, # buf = # buf4, # buf3 = ENCODED_VOLID_SIZE + n2, buf1 = buf5, n = ENCODED_VOLID_SIZE, subarray(buf5, 0, ENCODED_NAT_SIZE + # buf2) = buf0 + buf2, subarray(buf5, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, n2) = subarray(buf3, ENCODED_VOLID_SIZE, n2), subarray(buf4, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2) = subarray(buf, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2), vtbl1 ≠ ∅, is-encoded(v, subarray(buf5, ENCODED_NAT_SIZE + # buf2, ENCODED_VOLID_SIZE)), is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, # vtbl1 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ ENCODED_VOLID_SIZE + n2, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + ENCODED_VOLID_SIZE + n2, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, vtbl1 ⊥ vtbl, ¬ v ∈ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ [encode_nat#(vtbl1[v], (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE; buf5, n; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf5 = # buf1 ∧ subarray(buf5, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) = subarray(buf1, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) ∧ subarray (buf5, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf5 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE) = subarray (buf1, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf5 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE) ∧ ( err = ESUCCESS → is-encoded(vtbl1[v], subarray(buf5, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)) ∧ n = ENCODED_NAT_SIZE) → ⟪n0 := ((ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) + n; vtbl0 := vtbl1 -- v⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf5 = # buf4 ∧ ( err = ESUCCESS → (∃ buf0, buf2, buf, vtbl3. buf5 = buf0 + buf2 + buf ∧ vtbl1 ∪ vtbl = vtbl0 ∪ vtbl3 ∧ vtbl0 ⊥ vtbl3 ∧ # buf0 + # buf2 = n0 ∧ # vtbl0 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf ∧ is-encoded(#(vtbl0 ∪ vtbl3), buf0) ∧ is-encoded-rec(vtbl3, buf2))) ∧ # vtbl0 < # vtbl1))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + m = 2 * m; (s)% ⊦ encoding-size(n) = ENCODED_NAT_SIZE; (s)