Proof step 5 from proof prepost-replay-lpt (previous step)

Heuristic annotation applied rule annotation right

And obtained the following new goals

• Proof step 6:

  # lpt4 = # avol1, isbuf ↔ boolvar, avol0 = avol1, bleb = nobuffer, log = log1, log0 = nx, lpt = replay-lpt(lpt4, log0, n), lpt = lpt3, lpt0 = lpt1, lpt2 = lpt4, m = m1, m0 = LEB_SIZE, n = n0, n1 = 0, n < # lpt, avol-replay-lpt-unchanged(avol1, avol, lpt4, log0), awbuf-inv(avol1, nobuffer), awbuf-inv(avol, bleb), synced(avol1), synced(avol), n ≤ # lpt4 ⊦ ⟪if lpt[n].flags ≠ LP_FREE ∧ ¬ n ∈ log0 then {if lpt[n].flags = LP_INDEX_NODES then lpt[n].size := m0; if lpt[n].ref-size = 0 then {lpt[n].flags := LP_FREE; lpt[n].size := 0; awbuf_unmap#(n, adr, m, log, lpt0, ns, bleb, isbuf; avol)}}; n := n + 1⟫ ( ( n ≤ # lpt4 ∧ awbuf-inv(avol, bleb) ∧ bleb = nobuffer ∧ lpt = replay-lpt(lpt4, log0, n) ∧ # lpt4 = # avol1 ∧ avol-replay-lpt-unchanged(avol1, avol, lpt4, log0) ∧ synced(avol)) ∧ # lpt - n < # lpt3 - n0)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss)%avol-replay-lpt-unchanged-size: ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) → # avol1 = # avol0; (forward) from specification persistence-base%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)%n ≤ # lpt ⊦ # replay-lpt(lpt, nx, n) = # lpt; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m ≤ n → (n ≤ m ↔ m = n); (s)% ⊦ 0 ≤ m; (s)% ⊦ replay-lpt(lpt, nx, 0) = lpt; (s)% ⊦ avol-replay-lpt-unchanged(avol, avol, lpt, nx) ↔ # avol = # lpt; (s)% ⊦ awbuf-inv(avol, nobuffer) → (synced(avol) ↔ true); (ss) Used formulas: n ≤ # lpt` ∧ awbuf-inv(avol, bleb) ∧ bleb = nobuffer ∧ lpt = replay-lpt(lpt`, log0, n) ∧ # lpt` = # avol` ∧ avol-replay-lpt-unchanged(avol`, avol, lpt`, log0) ∧ synced(avol), # lpt - n = # lpt - n