Proof step 72 from proof truncate-empty (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 73:

  ⊦ m ≤ n ∧ ¬ # σ1 < ⌜n⌝ → (σ1 to n) + σ2 from m = ((σ1 from m) to (n - m)) + σ2

• Proof step 74:

  VFS_PAGE_SIZE = n2 + n1, files1[ino0] = mkfile(m, md0, # links(ino0, dirs), content0), n1 < VFS_PAGE_SIZE, afs-cons(dirs, files1), ino0 ∈ files1, m0 ∈ content0, m0 * VFS_PAGE_SIZE + n1 ≤ m0 * VFS_PAGE_SIZE + n1 ⊦ [asynced := ?] ((((content0.stream from m0 * VFS_PAGE_SIZE + n1) to (m0 * VFS_PAGE_SIZE + n1 - m0 * VFS_PAGE_SIZE + n1)) + (σ⊥ to n2)) + σ⊥ = σ⊥), n1 = 0, n2 = 0, # content0.stream < ⌜m0 * VFS_PAGE_SIZE + n1⌝

Rule argument

Additional information

Used simplifier rules: ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m ≤ m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ # content.stream = ∞; (s)% ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)% ⊦ ¬ ∞ < n∞; (s)% ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s)% ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s)% ⊦ ⌜m⌝ ≠ ∞; (s)%add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf%add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf% ⊦ # σ⊥ = ∞; (s)% ⊦ ⌜m⌝ < ∞; (s)% ⊦ #(σ0 + σ2) = # σ0 + # σ2; (s)%¬ # σ0 < ⌜n⌝ ⊦ #(σ0 to n) = ⌜n⌝ ; (s)%append-assoc: ⊦ (σ0 + σ3) + σ4 = σ0 + σ3 + σ4; from specification stream[buffer-inf]% ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2; (s)% ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ m + n - n + n1 = m - n1; (s)% ⊦ m - m = 0; (s)% ⊦ #(content.stream from n) = ∞; (s)% ⊦ ⌜0⌝ < n∞ ↔ n∞ ≠ ⌜0⌝ ; (s)% ⊦ n ≥ m ↔ m ≤ n; (s) Used terms: m0 * VFS_PAGE_SIZE + n1, σ⊥ to n2, m0 * VFS_PAGE_SIZE + n1, content0.stream