Proof step 67 from proof truncate-greater (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ ¬ # σ1 < ⌜n⌝ ∧ ¬ # σ2 < ⌜n1⌝ → (σ1 to n) + σ2 to n1 + n = (σ1 to n) + (σ2 to n1)

• Proof step 69:

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

Rule argument

Additional information

Used simplifier rules: ⊦ # content.stream = ∞; (s)% ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)% ⊦ ¬ ∞ < n∞; (s)% ⊦ # σ⊥ = ∞; (s)%¬ # σ0 < ⌜n⌝ ⊦ #(σ0 to n) = ⌜n⌝ ; (s)% ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)% ⊦ ¬ n < 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% ⊦ ⌜m⌝ < ∞; (s)% ⊦ #(σ0 + σ2) = # σ0 + # σ2; (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⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ ⌜n⌝ + n∞1 = ⌜n⌝ + n∞2 ↔ n∞1 = n∞2; (s)% ⊦ finp(σ0 to m); (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s)%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 Used terms: n0, σ⊥ to n0, m1 * (n0 + n2) + n2, content0.stream