[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 45 from proof decode (previous step)

# vtbl1 = m0 + 1, is-encoded(m, subarray(buf, (ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)) + ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded(v, subarray(buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), ENCODED_VOLID_SIZE)), is-encoded(vtbl0, buf), is-encoded((m0 + 1) + # vtbl, subarray(buf, 0, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, subarray(buf, ENCODED_NAT_SIZE, # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))), is-encoded-rec (vtbl1, subarray (buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * m0 + ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)), 2 * ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) + ENCODED_VOLID_SIZE ≤ # buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) + ENCODED_VOLID_SIZE ≤ # buf, 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * (m0 + # vtbl) + ENCODED_VOLID_SIZE ≤ # buf, vtbl ⊥ vtbl1, err0 = ESUCCESS → ENCODED_NAT_SIZE ≤ # buf ∧ n3 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, # vtbl[v, m] = 1 + # vtbl ∧ #(vtbl1 -- v) = m0 ∧ ENCODED_NAT_SIZE + (#(vtbl1 -- v) + # vtbl[v, m]) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) ≤ # buf ∧ is-encoded-rec(vtbl[v, m], subarray(buf, ENCODED_NAT_SIZE, # vtbl[v, m] * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))) ∧ is-encoded-rec (vtbl1 -- v, subarray (buf, ENCODED_NAT_SIZE + # vtbl[v, m] * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), #(vtbl1 -- v) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)))

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 46:
vtbl ≠ ∅ ⊦ is-encoded-rec(vtbl, buf) ↔ (∃ v, buf0, buf1, buf2. v ∈ vtbl ∧ buf = buf0 + buf1 + buf2 ∧ is-encoded(v, buf0) ∧ is-encoded(vtbl[v], buf1) ∧ is-encoded-rec(vtbl -- v, buf2))
Proof step 47:
# vtbl1 = m0 + 1, is-encoded((m0 + 1) + # vtbl, subarray(buf, 0, ENCODED_NAT_SIZE)), is-encoded(vtbl0, buf), is-encoded(v, subarray(buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), ENCODED_VOLID_SIZE)), is-encoded(m, subarray(buf, (ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)) + ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, subarray(buf, ENCODED_NAT_SIZE, # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))), 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * (m0 + # vtbl) + ENCODED_VOLID_SIZE ≤ # buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) + ENCODED_VOLID_SIZE ≤ # buf, 2 * ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) + ENCODED_VOLID_SIZE ≤ # buf, vtbl ⊥ vtbl1, err0 = ESUCCESS → ENCODED_NAT_SIZE ≤ # buf ∧ n3 = ENCODED_NAT_SIZE, ∃ v, buf0, buf1, buf2. v ∈ vtbl1 ∧ subarray (buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * m0 + ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) = buf0 + buf1 + buf2 ∧ is-encoded(v, buf0) ∧ is-encoded(vtbl1[v], buf1) ∧ is-encoded-rec(vtbl1 -- v, buf2), err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, # vtbl[v, m] = 1 + # vtbl ∧ #(vtbl1 -- v) = m0 ∧ ENCODED_NAT_SIZE + (#(vtbl1 -- v) + # vtbl[v, m]) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) ≤ # buf ∧ is-encoded-rec(vtbl[v, m], subarray(buf, ENCODED_NAT_SIZE, # vtbl[v, m] * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))) ∧ is-encoded-rec (vtbl1 -- v, subarray (buf, ENCODED_NAT_SIZE + # vtbl[v, m] * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), #(vtbl1 -- v) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)))

Rule argument

spec: <toplevel> name: is-encoded-rec seq: vtbl ≠ ∅ ⊦ is-encoded-rec(vtbl, buf) ↔ (∃ v, buf0, buf1, buf2. v ∈ vtbl ∧ buf = buf0 + buf1 + buf2 ∧ is-encoded(v, buf0) ∧ is-encoded(vtbl[v], buf1) ∧ is-encoded-rec(vtbl -- v, buf2)) subst: [buf, vtbl] → [subarray (buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * m0 + ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), vtbl1] flags: <all paths>

Additional information

Used terms: subarray (buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * m0 + ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), vtbl1