Proof step 1 from proof abs-single-FO-one-pending (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), abs(h, rs, p), allReadsOK(h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Proof step 2 from proof abs-single-FO-one-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  FO(t) = p(l)[n], ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), abs(h, rs, p), allReadsOK(h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Used simplifier rules: delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del

Proof step 3 from proof abs-single-FO-one-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:

  FO(t) = p(l)[n], ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), allReadsOK(h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n, ∀ 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-single-FO-one-pending (previous step) (back to tree)

Lemma abs-def

Proof step 5 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  FO(t) = p(l)[n], ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOK(h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Used terms: l

Proof step 6 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  FO(t) = p(l)[n], l = l0, ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOK(h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

• Proof step 17:

  FO(t) = p(l)[n], l ≠ l0, ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOK(h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Used formulas: l = l0

Proof step 7 from proof abs-single-FO-one-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  FO(t) = p(l0)[n], ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l0) | false), rs(l0), p(l0)), allReadsOK(h), isPersistFO(n, p(l0)), onePendingW(t, l0, p), FO(t) ∈ p(l0), ¬ t ∈ rs(l0), ¬ FO(t) ∈ p(l0) -p n ⊦

Rule argument

Additional information

Used simplifier rules: delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del

Proof step 8 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  FO(t) = p(l0)[n], ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l0) | false), rs(l0), p(l0)), allReadsOK(h), isPersistFO(n, p(l0)), noPendingW(t, p), onePendingW(t, l0, p), FO(t) ∈ p(l0), ¬ t ∈ rs(l0), ¬ FO(t) ∈ p(l0) -p n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ onePendingW(t, l, p) ∧ FOFollowsW(t, p(l)) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ p(l) → noPendingW(t, p); (ss) Used formulas: noPendingW(t, p)

Proof step 9 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  FO(t) = p(l0)[n], ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l0) | false), rs(l0), p(l0)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l0)), noPendingW(t, p), onePendingW(t, l0, p), FO(t) ∈ p(l0), ¬ t ∈ rs(l0), ¬ FO(t) ∈ p(l0) -p n ⊦

Rule argument

Additional information

Used terms: h

Proof step 10 from proof abs-single-FO-one-pending (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof abs-single-FO-one-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, fowl) ∧ allReadsOKInd(mem, persisted, h) ∧ persisted(l) ∧ isPersistFO(n, fowl) ∧ (fowl -p n)|W | t = [] ∧ ¬ FO(t) ∈ fowl -p n ∧ FO(t) ∈ fowl ∧ ¬ t ∈ rset → ((h | l) | t) | false = []

• Proof step 13:

  FO(t) = p(l0)[n], ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l0) | false), rs(l0), p(l0)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l0)), noPendingW(t, p), onePendingW(t, l0, p), FO(t) ∈ p(l0), ¬ t ∈ rs(l0), ¬ FO(t) ∈ p(l0) -p n ⊦ absloc(events((h | l0) | false), rs(l0), p(l0)) ∧ allReadsOKInd(∅, λ l. true, h) ∧ true ∧ isPersistFO(n, p(l0)) ∧ (p(l0) -p n)|W | t = [] ∧ ¬ FO(t) ∈ p(l0) -p n ∧ FO(t) ∈ p(l0) ∧ ¬ t ∈ rs(l0)

Rule argument

Additional information

Used terms: λ l. true, p(l0), ∅, l0, t, n, rs(l0), h

Proof step 12 from proof abs-single-FO-one-pending (previous step) (back to tree)

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

Proof step 13 from proof abs-single-FO-one-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  FO(t) = p(l0)[n], ((h | l0) | t) | false ≠ [], p(l0) |W | t ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l0) | false), rs(l0), p(l0)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l0)), noPendingW(t, p), onePendingW(t, l0, p), FO(t) ∈ p(l0), ¬ t ∈ rs(l0), ¬ FO(t) ∈ p(l0) -p n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ isPersistFO(n, fowl) → (fowl -p n)|W = fowl |W; (s)

Proof step 14 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  FO(t) = p(l0)[n], ((h | l0) | t) | false ≠ [], p(l0) |W | t ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l0) | false), rs(l0), p(l0)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l0)), onePendingW(t, l0, p), FO(t) ∈ p(l0), ¬ t ∈ rs(l0), ¬ FO(t) ∈ p(l0) -p n, ∀ l. p(l) |W | t = [] ⊦

Rule argument

Additional information

Used terms: t, p

Proof step 15 from proof abs-single-FO-one-pending (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 17 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  FO(t) = p(l)[n], l ≠ l0, ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Used terms: h

Proof step 18 from proof abs-single-FO-one-pending (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  FO(t) = p(l)[n], l ≠ l0, ((h | l) | t) | false ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦ absloc(events((h | l) | false), rs(l), p(l)) ∧ allReadsOKInd(∅, λ l. true, h) ∧ true ∧ isPersistFO(n, p(l)) ∧ (p(l) -p n)|W | t = [] ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ p(l) ∧ ¬ t ∈ rs(l)

Rule argument

Additional information

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

Proof step 20 from proof abs-single-FO-one-pending (previous step) (back to tree)

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

Proof step 21 from proof abs-single-FO-one-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  FO(t) = p(l)[n], l ≠ l0, ((h | l) | t) | false ≠ [], p(l) |W | t ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l)), onePendingW(t, l0, p), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ isPersistFO(n, fowl) → (fowl -p n)|W = fowl |W; (s)

Proof step 22 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = [])

• Proof step 24:

  FO(t) = p(l)[n], l ≠ l0, ((h | l) | t) | false ≠ [], p(l) |W | t ≠ [], FOFollowsW(t, p(l0)), absloc(events((h | l) | false), rs(l), p(l)), allReadsOKInd(∅, λ l. true, h), isPersistFO(n, p(l)), FO(t) ∈ p(l), ¬ t ∈ rs(l), ¬ FO(t) ∈ p(l) -p n, ∀ l1. l1 ≠ l0 → p(l1) |W | t = [] ⊦

Rule argument

Additional information

Used terms: t, l0, p

Proof step 23 from proof abs-single-FO-one-pending (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof abs-single-FO-one-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l