Proof step 1 from proof take-first-vol-write-no-unpersisted-writes (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ((h.take(firstVolWrite(l, h)))|W | l) | false ≠ [] ⊦

Rule argument

Additional information

Proof step 2 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h.take(firstVolWrite(l, 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 take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  [].take(firstVolWrite(l, [])).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [] ⊦

• Proof step 6:

  (vpe + h0).take(firstVolWrite(l, vpe + h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 4 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)

Rule argument

Additional information

Used simplifier rules: ⊦ [].indexWhere(p) = 0; (s) ⊦ x.take(0) = []; (s) ⊦ [].filter(p) = []; (s) Used terms: l, []

Proof step 5 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Lemma firstVolWrite-def

Proof step 6 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (vpe ' + h0).take(firstVolWrite(l, vpe ' + h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 7 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)

• Proof step 9:

  (vpe ' + h0).take((vpe ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used terms: l, vpe ' + h0

Proof step 8 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Lemma firstVolWrite-def

Proof step 9 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  vpe = (e, b), (vpe ' + h0).take((vpe ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 10 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ((e, b) ' + h0).take(((e, b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 11 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  e = R(t, l0, v), ((e, b) ' + h0).take(((e, b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

• Proof step 31:

  e = W(t, l0, v), ((e, b) ' + h0).take(((e, b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;;

Proof step 12 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ((R(t, l0, v), b) ' + h0).take(((R(t, l0, v), b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 13 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ ¬ p(a) → (a ' + x).indexWhere(p) = 1 + x.indexWhere(p)

• Proof step 15:

  ((R(t, l0, v), b) ' + h0).take(1 + h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦ (R(t, l0, v), b)._1.W? ∧ (R(t, l0, v), b)._1.l = l ∧ ¬ (R(t, l0, v), b)._2

Rule argument

Additional information

Used simplifier rules: ⊦ R(t, l, v).l = l; (s) ⊦ ¬ R(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2, (R(t, l0, v), b), h0

Proof step 14 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ R(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s)

Proof step 16 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used terms: l

Proof step 17 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 19:

  h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], ∃ a. a ∈ h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Used terms: h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)) .filter (λ vpe. vpe._1.W? ) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 )

Proof step 18 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  h0.take(firstVolWrite(vpe._1.l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = vpe._1.l).filter(λ vpe. ¬ vpe._2) = [], vpe._1.W?, vpe ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = vpe._1.l ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦ vpe._2

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 20 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  h0.take(firstVolWrite(e.l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = e.l).filter(λ vpe. ¬ vpe._2) = [], ¬ boolvar, vpe = (e, boolvar), e.W?, vpe ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = e.l ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 21 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  h0.take(firstVolWrite(e.l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = e.l).filter(λ vpe. ¬ vpe._2) = [], e.W?, (e, false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = e.l ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 22 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 23:

  h0.take(firstVolWrite(l0, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l0).filter(λ vpe. ¬ vpe._2) = [], e = W(t, l0, v), e.W?, (e, false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = l0 ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ e.W? → ((t = e.t ∧ l = e.l) ∧ v = e.v ↔ e = W(t, l, v)); (elim) Used terms: e, t, l0, v

Proof step 23 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  h0.take(firstVolWrite(l0, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l0).filter(λ vpe. ¬ vpe._2) = [], (W(t, l0, v), false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = l0 ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).W?; (s)

Proof step 24 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 26:

  (W(t, l0, v), false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = l0 ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], ∀ a. ¬ a ∈ h0.take(firstVolWrite(l0, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l0).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Used terms: h0.take(firstVolWrite(l0, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe0. vpe0._1.l = l0) .filter (λ vpe. ¬ vpe._2 )

Proof step 25 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  (W(t, l0, v), false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = l0 ∧ ¬ vpe0._2)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], ∀ a. ¬ a ∈ h0.take(firstVolWrite(a._1.l, h0)) ∨ ¬ a._1.W? ∨ a._1.l ≠ l0 ∨ a._2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 27 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 28:

  (W(t, l0, v), false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = l0 ∧ ¬ vpe0._2)), ∀ a. ¬ a ∈ h0.take(firstVolWrite(a._1.l, h0)) ∨ ¬ a._1.W? ∨ a._1.l ≠ l0 ∨ a._2, ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], ¬ (W(t, l0, v), false) ∈ h0.take(firstVolWrite((W(t, l0, v), false)._1.l, h0)) ∨ ¬ (W(t, l0, v), false)._1.W? ∨ (W(t, l0, v), false)._1.l ≠ l0 ∨ (W(t, l0, v), false)._2 ⊦

Rule argument

Additional information

Used terms: (W(t, l0, v), false)

Proof step 28 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  (W(t, l0, v), false) ∈ h0.take(h0.indexWhere(λ vpe0. vpe0._1.W? ∧ vpe0._1.l = l0 ∧ ¬ vpe0._2)), ¬ (W(t, l0, v), false) ∈ h0.take(firstVolWrite(l0, h0)), ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], ∀ a. ¬ a ∈ h0.take(firstVolWrite(a._1.l, h0)) ∨ ¬ a._1.W? ∨ a._1.l ≠ l0 ∨ a._2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s)

Proof step 29 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)

Rule argument

Additional information

Used terms: l0, h0

Proof step 30 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Lemma firstVolWrite-def

Proof step 31 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  ((W(t, l0, v), b) ' + h0).take(((W(t, l0, v), b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 32 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 33:

  b, ((W(t, l0, v), b) ' + h0).take(((W(t, l0, v), b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

• Proof step 42:

  ¬ b, ((W(t, l0, v), b) ' + h0).take(((W(t, l0, v), b) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used formulas: b

Proof step 33 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  ((W(t, l0, v), true) ' + h0).take(((W(t, l0, v), true) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 34 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ ¬ p(a) → (a ' + x).indexWhere(p) = 1 + x.indexWhere(p)

• Proof step 36:

  ((W(t, l0, v), true) ' + h0).take(1 + h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦ (W(t, l0, v), true)._1.W? ∧ (W(t, l0, v), true)._1.l = l ∧ ¬ (W(t, l0, v), true)._2

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2, (W(t, l0, v), true), h0

Proof step 35 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦ (l0 = l ⊃ (W(t, l, v), true) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s)

Proof step 37 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 38:

  (l0 = l ⊃ (W(t, l, v), true) ';[]).filter(λ vpe. ¬ vpe._2) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

• Proof step 39:

  h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 38 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) Used formulas: l0 = l

Proof step 39 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 40:

  h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [] ⊦

Rule argument

Additional information

Used terms: l

Proof step 40 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)

Rule argument

Additional information

Used terms: l, h0

Proof step 41 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Lemma firstVolWrite-def

Proof step 42 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  ((W(t, l0, v), false) ' + h0).take(((W(t, l0, v), false) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 43 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ p(a) → (a ' + x).indexWhere(p) = 0

• Proof step 45:

  ((W(t, l0, v), false) ' + h0).take(((W(t, l0, v), false) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦ (W(t, l0, v), false)._1.W? ∧ (W(t, l0, v), false)._1.l = l ∧ ¬ (W(t, l0, v), false)._2

Rule argument

Additional information

Used simplifier rules: ⊦ x.take(0) = []; (s) ⊦ W(t, l, v).l = l; (s) ⊦ [].filter(p) = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2, (W(t, l0, v), false), h0

Proof step 44 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  ((W(t, l0, v), false) ' + h0).take(((W(t, l0, v), false) ' + h0).indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], l0 ≠ l, ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s)

Proof step 46 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ ¬ p(a) → (a ' + x).indexWhere(p) = 1 + x.indexWhere(p)

• Proof step 48:

  ((W(t, l0, v), false) ' + h0).take(1 + h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?) .filter (λ vpe. vpe._1.l = l ) .filter (λ vpe. ¬ vpe._2 ) ≠ [], l0 ≠ l, ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦ (W(t, l0, v), false)._1.W? ∧ (W(t, l0, v), false)._1.l = l ∧ ¬ (W(t, l0, v), false)._2

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2, (W(t, l0, v), false), h0

Proof step 47 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], l0 ≠ l, ∀ l. h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).take(n + 1) = a + x.take(n); (s)

Proof step 49 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 50:

  h0.take(firstVolWrite(l, h0)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [], h0.take(h0.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], l0 ≠ l ⊦

Rule argument

Additional information

Used terms: l

Proof step 50 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

  ⊦ firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2)

Rule argument

Additional information

Used terms: l, h0

Proof step 51 from proof take-first-vol-write-no-unpersisted-writes (previous step) (back to tree)

Lemma firstVolWrite-def