Proof step 51 from proof truncate-smaller (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ ¬ # σ1 < ⌜n⌝ → σ1 + σ2 to n = σ1 to n

• Proof step 53:

  VFS_PAGE_SIZE = n0 + n1, files0[m] = mkfile(m0, md0, # links(m, dirs), content0), n1 < VFS_PAGE_SIZE, afs-cons(dirs, files0), m ∈ files0, m1 ∈ content0 ⊦ [asynced := ?] ((content0.stream to m1 * VFS_PAGE_SIZE) + ((content0.stream from m1 * VFS_PAGE_SIZE) to n1 to n1) = content0.stream to m1 * VFS_PAGE_SIZE + n1), n0 = 0, n1 = 0, #((content0.stream from m1 * VFS_PAGE_SIZE) to n1) < ⌜n1⌝

Rule argument

Additional information

Used simplifier rules: ⊦ #(content.stream from n) = ∞; (s)% ⊦ ¬ ∞ < n∞; (s)%¬ # σ0 < ⌜n⌝ ⊦ #(σ0 to n) = ⌜n⌝ ; (s)% ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)% ⊦ ¬ n < n; (s)% ⊦ ⌜m⌝ < ∞; (s)% ⊦ # content.stream = ∞; (s)% ⊦ #(σ0 + σ2) = # σ0 + # σ2; (s)% ⊦ # σ⊥ = ∞; (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%append-assoc: ⊦ (σ0 + σ3) + σ4 = σ0 + σ3 + σ4; from specification stream[buffer-inf]% ⊦ ⌜m + 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∞ < ∞ ↔ n∞ ≠ ∞; (s)% ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s)% ⊦ ⌜m⌝ ≠ ∞; (s)% ⊦ finp(σ0 to m); (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s) Used terms: n1, (σ⊥ to n0) + (content0.stream from VFS_PAGE_SIZE * m1 + VFS_PAGE_SIZE), (content0.stream from m1 * VFS_PAGE_SIZE) to n1