| (((lls(rxs, null, x0) * ls(rys, x1 + y)) * del-list(to_delete, n0)))(H), ((ls(rxs, x0) * ls(rys, x1 + y) * del-list(to_delete, n0)))(H), ((ls(rxs, x0) * lls(rys, r, x1) * ls(r, y) * del-list(to_delete, n0)))(H), # x0 < h0, n0 + # x0 ≤ h0, # x0 + # x1 ≤ h0, n0 ≤ # x0 + # x1 + # y, x1 + y = [] ∨ # x1 + # y = h0 ⊦ x1 = prefixn(h0 - # x0, x1 + y), # x0 + # x1 < h0 ∧ r ≠ null |
Used simplifier rules: ⊦ m < n → m ≤ n; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ # x0 ≤ n → prefixn(n, x0 + x1) = x0 + prefixn(n - # x0, x1); (s)%a: ⊦ (x + y) + z = x + y + z; from specification list% ⊦ x = x + y ↔ y = []; (s)% ⊦ prefixn(n, x) = [] ↔ n = 0 ∨ x = []; (ss)% ⊦ m ≤ n → (n - m = 0 ↔ n = m); (s)% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ ls(null, x) = (emp ∧ ⌜x = []⌝ ); (s)% ⊦ ⌜false⌝ = false; (s)% ⊦ (false ∧ P) = false; (s)%and-ass: ⊦ ((P0 ∧ P1) ∧ P2) = (P0 ∧ P1 ∧ P2); from specification heap-sep%and-com: ⊦ (P0 ∧ P1) = (P1 ∧ P0); from specification heap-sep% ⊦ false * P = false; (s)%sep-ass: ⊦ (P0 * P1) * P2 = P0 * P1 * P2; from specification heap-sep%sep-com: ⊦ P0 * P1 = P1 * P0; from specification heap-sep% ⊦ ¬ false(H); (s)%n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s)% ⊦ m ≤ n → (n ≤ m ↔ m = n); (s)%n ≤ # x ⊦ prefixn(n, x + y) = prefixn(n, x); (s)%n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ m ≤ n → (n < m ↔ false); (s)%# x ≤ m ⊦ prefixn(m, x) = x; (s)%n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x0, h0, n