Proof step 1 from proof stable-W4 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.rfo(ls.t) = [], SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(gs0.bq, gs0.pq), readFOsOk(gs.rfo, gs.fwriters), readFOsOk(gs0.rfo, gs0.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.freaders, gs0.freaders), relyws(ls.t, gs.fwriters, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(gs0.bq, gs0.pq, gs0.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = [], gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t), gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' ⊦ notMember(ls.t, gs0.freaders) ∧ oneMember(ls.t, ls.loc, gs0.fwriters) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = [] ∧ (gs0.bq(ls.t) = [] ∨ gs0.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (gs0.bq(ls.t) ≠ [] ∧ gs0.bq(ls.t).head.W? → gs0.bq(ls.t).head = W(ls.loc, ls.val))

Rule argument

Additional information

Proof step 2 from proof stable-W4 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs0.rfo(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(gs0.bq, gs0.pq), readFOsOk(gs.rfo, gs.fwriters), readFOsOk(gs0.rfo, gs0.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.freaders, gs0.freaders), relyws(ls.t, gs.fwriters, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(gs0.bq, gs0.pq, gs0.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), [] = gs.bq(ls.t) → [] = gs0.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), SF ' = gs.bq(ls.t) → SF ' = gs0.bq(ls.t) ∨ [] = gs0.bq(ls.t), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' ⊦ (gs0.bq(ls.t) = [] ∨ gs0.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (gs0.bq(ls.t) ≠ [] ∧ gs0.bq(ls.t).head.W? → gs0.bq(ls.t).head = W(ls.loc, ls.val))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ bel ⊒w bel0 ∧ ¬ be ∈ bel → ¬ be ∈ bel0; (as) ⊦ relyws(t, tsf0, tsf1) ∧ oneMember(t, l, tsf0) → oneMember(t, l, tsf1); (s) ⊦ relyws(t, tsf0, tsf1) ∧ notMember(t, tsf0) → notMember(t, tsf1); (s)

Proof step 3 from proof stable-W4 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  gs.rfo(ls.t) = [], gs0.rfo(ls.t) = [], gs0.bq(ls.t) ≠ [], gs0.bq(ls.t) ≠ W(ls.loc, ls.val) ', SFTrailing(gs0.bq), SFTrailing(gs.bq), ctrok(gs0.fctr, gs0.fwriters), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), readFOsOk(gs0.rfo, gs0.fwriters), readFOsOk(gs.rfo, gs.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.fwriters, gs0.fwriters), relyws(ls.t, gs.freaders, gs0.freaders), writersOk(gs0.bq, gs0.pq, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), SF ' = gs.bq(ls.t) → SF ' = gs0.bq(ls.t) ∨ [] = gs0.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), [] = gs.bq(ls.t) → [] = gs0.bq(ls.t), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' ⊦

• Proof step 6:

  gs.rfo(ls.t) = [], gs0.rfo(ls.t) = [], gs0.bq(ls.t) ≠ [], gs0.bq(ls.t).head ≠ W(ls.loc, ls.val), gs0.bq(ls.t).head.W?, SFTrailing(gs0.bq), SFTrailing(gs.bq), ctrok(gs0.fctr, gs0.fwriters), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), readFOsOk(gs0.rfo, gs0.fwriters), readFOsOk(gs.rfo, gs.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.fwriters, gs0.fwriters), relyws(ls.t, gs.freaders, gs0.freaders), writersOk(gs0.bq, gs0.pq, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), SF ' = gs.bq(ls.t) → SF ' = gs0.bq(ls.t) ∨ [] = gs0.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), [] = gs.bq(ls.t) → [] = gs0.bq(ls.t), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' ⊦

Rule argument

Additional information

Proof step 4 from proof stable-W4 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.bq(ls.t) = W(ls.loc, ls.val) ', gs0.rfo(ls.t) = [], gs.rfo(ls.t) = [], gs0.bq(ls.t) ≠ [], gs0.bq(ls.t) ≠ gs.bq(ls.t), [] ≠ gs.bq(ls.t), SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(gs0.bq, gs0.pq), readFOsOk(gs.rfo, gs.fwriters), readFOsOk(gs0.rfo, gs0.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.freaders, gs0.freaders), relyws(ls.t, gs.fwriters, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(gs0.bq, gs0.pq, gs0.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), SF ' = gs.bq(ls.t) → SF ' = gs0.bq(ls.t) ⊦

Rule argument

Additional information

Proof step 5 from proof stable-W4 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ W(l, v) ≠ SF; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ be ' ⊒w bel ↔ bel = be ' ∨ bel = []; (ws) ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.bq(ls.t), be, bel

Proof step 6 from proof stable-W4 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gs.bq(ls.t) = W(ls.loc, ls.val) ', gs0.rfo(ls.t) = [], gs.rfo(ls.t) = [], gs0.bq(ls.t) ≠ [], gs0.bq(ls.t).head ≠ W(ls.loc, ls.val), [] ≠ gs.bq(ls.t), gs0.bq(ls.t).head.W?, SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(gs0.bq, gs0.pq), readFOsOk(gs.rfo, gs.fwriters), readFOsOk(gs0.rfo, gs0.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.freaders, gs0.freaders), relyws(ls.t, gs.fwriters, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(gs0.bq, gs0.pq, gs0.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), SF ' = gs.bq(ls.t) → SF ' = gs0.bq(ls.t) ⊦

Rule argument

Additional information

Proof step 7 from proof stable-W4 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  gs.bq(ls.t) = W(ls.loc, ls.val) ', gs0.bq(ls.t) = be + bel, gs.rfo(ls.t) = [], gs0.rfo(ls.t) = [], gs0.bq(ls.t) ≠ [], [] ≠ gs.bq(ls.t), be ≠ W(ls.loc, ls.val), be.W?, SFTrailing(gs0.bq), SFTrailing(gs.bq), ctrok(gs0.fctr, gs0.fwriters), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), readFOsOk(gs0.rfo, gs0.fwriters), readFOsOk(gs.rfo, gs.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.fwriters, gs0.fwriters), relyws(ls.t, gs.freaders, gs0.freaders), writersOk(gs0.bq, gs0.pq, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), ¬ SF ∈ gs.bq(ls.t), SF ' = gs.bq(ls.t) → SF ' = gs0.bq(ls.t), gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs0.bq(ls.t), be, bel

Proof step 8 from proof stable-W4 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.bq(ls.t) = W(ls.loc, ls.val) ', gs0.bq(ls.t) = be ' + bel, gs0.rfo(ls.t) = [], gs.rfo(ls.t) = [], [] ≠ gs.bq(ls.t), be ≠ W(ls.loc, ls.val), be.W?, SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(gs0.bq, gs0.pq), readFOsOk(gs.rfo, gs.fwriters), readFOsOk(gs0.rfo, gs0.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.freaders, gs0.freaders), relyws(ls.t, gs.fwriters, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(gs0.bq, gs0.pq, gs0.fwriters), gs.bq(ls.t) ⊒w be ' + bel, ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), SF ' = gs.bq(ls.t) → SF ' = be ' + bel ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 9 from proof stable-W4 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ W(l, v) ≠ SF; (s) ⊦ x + [] = x; (s) ⊦ be ' ⊒w be0 ' + bel ↔ be0 = be ∧ bel = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.bq(ls.t), be0, bel0