Proof step 3 from proof content-read (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ σ = σ2 ↔ # σ = # σ2 ∧ (∀ n. ⌜n⌝ < # σ → σ[n] = σ2[n])

Rule argument

Additional information

Used simplifier rules: ⊦ # ⌜buf⌝ = ⌜# buf⌝ ; (s)% ⊦ # ⌜nf0 to n⌝ = ⌜n⌝ ; (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s)% ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)% ⊦ n < # buf → ⌜buf⌝ [n] = buf[n]; (s)% ⊦ ⌜dx⌝ [n] = dx[n]; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)%m < n ⊦ (nf0 to n)[m] = nf0(m); (s)% ⊦ ((nf0 from n))(m) = nf0(m + n); (s)% ⊦ VFS_PAGE_SIZE ≠ 0; (s)%n ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m; (s)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%n ≠ 0 ⊦ (m + n0 * n) % n = m % n; (s)% ⊦ m < n → m / n = 0; (s)% ⊦ n + 0 = n; (s)% ⊦ m < n → m % n = m; (s)% ⊦ # zeropage = VFS_PAGE_SIZE; (s) Used terms: ⌜ ( (λ n0. (n0 / VFS_PAGE_SIZE ∈ content ⊃ content[n0 / VFS_PAGE_SIZE] ;zeropage ) [n0 % VFS_PAGE_SIZE ]) from n * VFS_PAGE_SIZE) to VFS_PAGE_SIZE ⌝ , ⌜(n ∈ content ⊃ content[n];zeropage)⌝