Proof step 1 from proof first-vol-write-size2 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(firstVolWrite(l, h) = # h ↔ (h |W | l) | false = []) ⊦

Rule argument

Additional information

Proof step 2 from proof first-vol-write-size2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(firstVolWrite(l, h) = # h ↔ h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []) ⊦

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b);

Proof step 3 from proof first-vol-write-size2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ firstVolWrite(l, h) < # h ↔ (h |W | l) | false ≠ []

• Proof step 5:

  firstVolWrite(l, h) < # h ↔ (h |W | l) | false ≠ [], ¬(firstVolWrite(l, h) = # h ↔ h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []) ⊦

Rule argument

Additional information

Used terms: l, h

Proof step 4 from proof first-vol-write-size2 (previous step) (back to tree)

Lemma first-vol-write-size

Proof step 5 from proof first-vol-write-size2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  firstVolWrite(l, h) < # h ↔ (h |W | l) | false ≠ [], firstVolWrite(l, h) = # h, h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [] ⊦

• Proof step 8:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], firstVolWrite(l, h) < # h ↔ (h |W | l) | false ≠ [], firstVolWrite(l, h) ≠ # h ⊦

Rule argument

Additional information

Proof step 6 from proof first-vol-write-size2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  firstVolWrite(l, h) = # h, h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], (h |W | l) | false ≠ [], firstVolWrite(l, h) < # h ⊦

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b);

Proof step 7 from proof first-vol-write-size2 (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b); ⊦ ¬ n < n; (s)

Proof step 8 from proof first-vol-write-size2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], (h |W | l) | false = [], firstVolWrite(l, h) ≠ # h, ¬ firstVolWrite(l, h) < # h ⊦

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b);

Proof step 9 from proof first-vol-write-size2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ m < n ↔ ¬ n ≤ m

Rule argument

Additional information

Used simplifier rules: restrict-W: ⊦ h |W = h.filter(λ vpe. vpe._1.W?); restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b); first-vol-write-size3: ⊦ ¬ # h < firstVolWrite(l, h); ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) Used terms: firstVolWrite(l, h), # h

Proof step 10 from proof first-vol-write-size2 (previous step) (back to tree)

A spec-lemma