Proof step 1 from proof abs-leading-last-FO-no-pending (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  p(l) = FO(t) ' + fowl, ((h | l) | t) | false ≠ [], abs(h, rs, p), allReadsOK(h), noPendingW(t, p), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl ⊦

Rule argument

Additional information

Proof step 2 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  p(l) = FO(t) ' + fowl, ((h | l) | t) | false ≠ [], abs(h, rs, p), allReadsOK(h), noPendingW(t, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 3 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)))

• Proof step 5:

  p(l) = FO(t) ' + fowl, ((h | l) | t) | false ≠ [], allReadsOK(h), noPendingW(t, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl, ∀ l. absloc(events((h | l) | false), rs(l), p(l)) ⊦

Rule argument

Additional information

Used terms: h, rs, p

Proof step 4 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

Lemma abs-def

Proof step 5 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  p(l) = FO(t) ' + fowl, ((h | l) | t) | false ≠ [], absloc(events((h | l) | false), rs(l), p(l)), allReadsOK(h), noPendingW(t, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl ⊦

Rule argument

Additional information

Used terms: l

Proof step 6 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ allReadsOK(h) ↔ allReadsOKInd(∅, λ l. true, h)

• Proof step 8:

  p(l) = FO(t) ' + fowl, ((h | l) | t) | false ≠ [], absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), noPendingW(t, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl ⊦

Rule argument

Additional information

Used terms: h

Proof step 7 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ noPendingW(t, p) ↔ (∀ l. p(l) |W | t = [])

• Proof step 10:

  p(l) = FO(t) ' + fowl, ((h | l) | t) | false ≠ [], absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl, ∀ l. p(l) |W | t = [] ⊦

Rule argument

Additional information

Used terms: t, p

Proof step 9 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  p(l) = FO(t) ' + fowl, p(l) |W | t = [], ((h | l) | t) | false ≠ [], absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl ⊦

Rule argument

Additional information

Used terms: l

Proof step 11 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ absloc(events((h | l) | false), rset, FO(t) ' + fowl) ∧ allReadsOKInd(mem, persisted, h) ∧ persisted(l) ∧ fowl |W | t = [] ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rset → ((h | l) | t) | false = []

• Proof step 13:

  p(l) = FO(t) ' + fowl, p(l) |W | t = [], ((h | l) | t) | false ≠ [], absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ fowl ⊦ absloc(events((h | l) | false), rs(l), FO(t) ' + fowl) ∧ allReadsOKInd(∅, λ l. true, h) ∧ true ∧ fowl |W | t = [] ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rs(l)

Rule argument

Additional information

Used terms: λ l. true, fowl, ∅, l, t, rs(l), h

Proof step 12 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

Lemma abs-loc-no-w-last-firstfo-then-no-pending

Proof step 13 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  p(l) = FO(t) ' + fowl, p(l) |W | t = [], ((h | l) | t) | false ≠ [], fowl |W | t ≠ [], absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), FO(t) ∈ p(l), ¬ FO(t) ∈ fowl, ¬ t ∈ rs(l) ⊦

Rule argument

Additional information

Proof step 14 from proof abs-leading-last-FO-no-pending (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (FO(t) ' + fowl)|W = fowl |W; (s) a: ⊦ (x + y) + z = x + y + z; from specification list