| # lpt4 = # avol1, lpt5[n].flags = LP_INDEX_NODES, isbuf ↔ boolvar, avol0 = avol1, bleb = nobuffer, log = log1, log0 = nx, lpt = lpt5[n, lpt5[n].size:= m0], lpt0 = lpt1, lpt2 = lpt4, lpt5 = lpt3, lpt5 = replay-lpt(lpt4, log0, n), m = m1, m0 = LEB_SIZE, n = n0, n1 = 0, n < # lpt5, n < # lpt, avol-replay-lpt-unchanged(avol1, avol, lpt4, log0), awbuf-inv(avol, bleb), awbuf-inv(avol1, nobuffer), synced(avol), synced(avol1), n ≤ # lpt4 ⊦ ⟪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), lpt5[n].flags = LP_FREE, lpt[n].ref-size = 0, n ∈ log0 |
Used simplifier rules: elim-lp-upd-size: ⊦ lp.size:= n = mklp(lp.ref-size, n, lp.flags, lp.gcheapidx);% ⊦ m ≤ m; (s)% ⊦ m < # lpt → lpt[m, lp][m] = lp; (s)% ⊦ mklp(n2, n3, lpf, m).ref-size = n2; (s)%n ≤ # lpt ⊦ # replay-lpt(lpt, nx, n) = # lpt; (s)% ⊦ # lpt[n, lp] = # lpt; (s)% ⊦ m < n → m ≤ n; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%avol-replay-lpt-unchanged-size: ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) → # avol1 = # avol0; (forward) from specification persistence-base% ⊦ m < n → n ≠ 0; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)%n ≤ m, m < # lpt ⊦ replay-lpt(lpt, nx, n)[m] = lpt[m]; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%transitivity: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification oelem[nat-set]% ⊦ m < n → ¬ n < m; (s)% ⊦ m + 1 ≤ n ↔ m < n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%n < # lpt ⊦ replay-lpt(lpt, nx, n + 1) = (lpt[n].flags = LP_FREE ∨ n ∈ nx ⊃ replay-lpt(lpt, nx, n) ;(lpt[n].flags = LP_INDEX_NODES ∧ lpt[n].ref-size ≠ 0 ⊃ replay-lpt(lpt, nx, n)[n, lpt[n].size:= LEB_SIZE] ;(lpt[n].ref-size = 0 ⊃ replay-lpt(lpt, nx, n) [n, mklp(0, 0, LP_FREE, lpt[n].gcheapidx) ] ;replay-lpt(lpt, nx, n) ) ) ); (s)% ⊦ awbuf-inv(avol, nobuffer) → (synced(avol) ↔ true); (ss)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ n < m → (m - n) + n = m; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ ¬ n < n; (s)