Proof step 7 from proof inv-set-iblock-refsize (previous step)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat% ⊦ ¬ n < n; (s)%⊦ lpt-free-unref(lpt) → ( lpt-free-unref(lpt[n, lp]) ↔ n < # lpt ∧ lp.flags = LP_FREE → lp.ref-size = 0); (s)% ⊦ (lp.ref-size:= m).flags = lp.flags; (s)% ⊦ (lp.ref-size:= m).ref-size = m; (s)% ⊦ mklp(n2, n3, lpf, m).flags = lpf; (s)% ⊦ mklp(m, m0, lpf, m1).ref-size:= m2 = mklp(m2, m0, lpf, m1); (s)%lpt[n].flags = lp.flags ⊦ bufs-log-only(bleb, nx, lpt) → bufs-log-only(bleb, nx, lpt[n, lp]); (s)% ⊦ # lpt[n, lp] = # lpt; (s)% ⊦ LP_GROUP_NODES ≠ LP_INDEX_NODES; (s)%n < # lpt, lpf ≠ LP_GROUP_NODES ⊦ lpt[n] = mklp(n0, n1, lpf, n2) ∧ log-group-block(nx, lpt) → log-group-block(nx, lpt[n, lp]); (s)%⊦ lpt-leb-size(lpt) → (lpt-leb-size(lpt[n, lp]) ↔ # lpt ≤ n ∨ lp.size ≤ LEB_SIZE); (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ (lp.ref-size:= m).size = lp.size; (s)% ⊦ LP_FREE ≠ LP_INDEX_NODES; (s)%⊦ freelist-cons(lpt, freelist) ∧ lpt[n] = mklp(m0, m1, lpf, m2) → freelist-cons(lpt[n, mklp(n0, n1, lpf, n2)], freelist); (s)%n < # lpt ⊦ lpt[n] = mklp(m0, m1, lpf0, m2) → ( bin-heap-inv(gch, lpt[n, mklp(n0, n1, lpf1, m2)]) ↔ bin-heap-inv(gch, lpt)); (s)%lpf0 ≠ LP_GROUP_NODES, lpf1 ≠ LP_GROUP_NODES, n < # lpt ⊦ lpt[n] = mklp(m0, m1, lpf0, m2) → gc-heap(lpt[n, mklp(n0, n1, lpf1, n2)], nx) = gc-heap(lpt, nx); (s)%⊦ lpt[n] = mklp(m0, n1, lpf0, m1) → ( buf-ro-rw-mode (boolvar, bleb, lpt[n, mklp(n0, n1, lpf1, n2)], avol) ↔ buf-ro-rw-mode(boolvar, bleb, lpt, avol)); (s)% ⊦ mklp(n2, n3, lpf, m).size = n3; (s)%n < # lpt, lpf ≠ LP_GROUP_NODES ⊦ lpt-ram-flash(lpt, lpt0, nx) → lpt-ram-flash(lpt[n, mklp(n0, n1, lpf, n2)], lpt0, nx); (ss)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%n < # lpt ⊦ lpt[n] = mklp(n0, n1, lpf, n2) ∧ lpt-leb-size(lpt) → ¬ LEB_SIZE < n1; (s)