Proof step 1 from proof init-state-inv (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), pcf = (λ tid. idle), ¬ FLITInv(gs, lsf, pcf), ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Proof step 2 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ¬ FLITInv(gs, lsf, λ tid. idle), ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Proof step 3 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ FLITInv(gs, lsf, pcf) ↔ FLITGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITLInv(gs, lsf(t), pcf(t)))

• Proof step 5:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ FLITGInv(gs) ∨ (∃ t. ¬(lsf(t).t = t ∧ FLITLInv(gs, lsf(t), idle))) ⊦

Rule argument

Additional information

Used terms: gs, lsf, λ tid. idle

Proof step 4 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ FLITGInv(gs) ∨ lsf(t).t ≠ t ∨ ¬ FLITLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Proof step 6 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ FLITGInv(gs) ↔ ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters)

• Proof step 8:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬(ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters)) ∨ lsf(t).t ≠ t ∨ ¬ FLITLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Used terms: gs

Proof step 7 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ ctrok(λ l. 0, λ l. ∅) ∨ ¬ writersOk(λ t. [], λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ FLITLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Proof step 9 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ FLITLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.freaders)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.fwriters)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.loc, gs.fwriters)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.bq, gs.pq)) ∧ (pc = W3 ∨ pc = W7 → noPending(ls.t, gs.bq, gs.pq)) ∧ (pc = W5 ∨ pc = W6 → FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc)) ∧ (pc = W1 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W7 → ¬ SF ∈ gs.bq(ls.t)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → gs.rfo(ls.t) = []) ∧ (pc = W3 → gs.bq(ls.t) = []) ∧ (pc = W4 → gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (pc = W5 → gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (pc = W6 → gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 → gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val)) ∧ (pc = W1 ∨ pc = W7 → gs.rfo(ls.t) = gs.bq(ls.t)) ∧ (pc = W2 → gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.bq, gs.pq)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.fwriters)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.freaders)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.loc, gs.freaders)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ¬ SF ∈ gs.bq(ls.t)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → gs.rfo(ls.t) = gs.bq(ls.t)) ∧ (pc = idle ∨ pc = ready ∨ pc = crashed → notMember(ls.t, gs.fwriters)) ∧ (pc = idle ∨ pc = ready ∨ pc = crashed → notMember(ls.t, gs.freaders)) ∧ (pc = idle ∨ pc = ready ∨ pc = crashed → noPendingW(ls.t, gs.bq, gs.pq)) ∧ (pc = idle ∨ pc = crashed → noPending(ls.t, gs.bq, gs.pq)) ∧ (pc = idle ∨ pc = ready ∨ pc = crashed → ¬ SF ∈ gs.bq(ls.t)) ∧ (pc = idle ∨ pc = ready ∨ pc = crashed → gs.rfo(ls.t) = gs.bq(ls.t))

• Proof step 11:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ ctrok(λ l. 0, λ l. ∅) ∨ ¬ writersOk(λ t. [], λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ ( (idle = W1 ∨ idle = W2 ∨ idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 ∨ idle = W7 → notMember(lsf(t).t, gs.freaders)) ∧ (idle = W1 ∨ idle = W2 ∨ idle = W7 → notMember(lsf(t).t, gs.fwriters)) ∧ (idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 → oneMember(lsf(t).t, lsf(t).loc, gs.fwriters)) ∧ (idle = W1 ∨ idle = W2 → noPendingW(lsf(t).t, gs.bq, gs.pq)) ∧ (idle = W3 ∨ idle = W7 → noPending(lsf(t).t, gs.bq, gs.pq)) ∧ (idle = W5 ∨ idle = W6 → FOFollowsW(lsf(t).t, gs.bq(lsf(t).t), gs.pq(lsf(t).loc), lsf(t).loc)) ∧ (idle = W1 ∨ idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W7 → ¬ SF ∈ gs.bq(lsf(t).t)) ∧ (idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 ∨ idle = W7 → gs.rfo(lsf(t).t) = []) ∧ (idle = W3 → gs.bq(lsf(t).t) = []) ∧ (idle = W4 → gs.bq(lsf(t).t) = [] ∨ gs.bq(lsf(t).t) = W(lsf(t).loc, lsf(t).val) ') ∧ (idle = W5 → gs.bq(lsf(t).t) = [] ∨ gs.bq(lsf(t).t) = FO(lsf(t).loc) ' ∨ gs.bq(lsf(t).t) = W(lsf(t).loc, lsf(t).val) ' + FO(lsf(t).loc) ') ∧ ( idle = W6 → gs.bq(lsf(t).t) = [] ∨ gs.bq(lsf(t).t) = SF ' ∨ gs.bq(lsf(t).t) = FO(lsf(t).loc) ' + SF ' ∨ gs.bq(lsf(t).t) = W(lsf(t).loc, lsf(t).val) ' + FO(lsf(t).loc) ' + SF ') ∧ (idle = W4 ∨ idle = W5 ∨ idle = W6 → gs.bq(lsf(t).t) ≠ [] ∧ gs.bq(lsf(t).t).head.W? → gs.bq(lsf(t).t).head = W(lsf(t).loc, lsf(t).val)) ∧ (idle = W1 ∨ idle = W7 → gs.rfo(lsf(t).t) = gs.bq(lsf(t).t)) ∧ (idle = W2 → gs.rfo(lsf(t).t) = gs.bq(lsf(t).t) ∨ gs.rfo(lsf(t).t) + SF ' = gs.bq(lsf(t).t)) ∧ (idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → noPendingW(lsf(t).t, gs.bq, gs.pq)) ∧ (idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → notMember(lsf(t).t, gs.fwriters)) ∧ (idle = R1 ∨ idle = R4 → notMember(lsf(t).t, gs.freaders)) ∧ (idle = R2 ∨ idle = R3 → oneMember(lsf(t).t, lsf(t).loc, gs.freaders)) ∧ (idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → ¬ SF ∈ gs.bq(lsf(t).t)) ∧ (idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → gs.rfo(lsf(t).t) = gs.bq(lsf(t).t)) ∧ (idle = idle ∨ idle = ready ∨ idle = crashed → notMember(lsf(t).t, gs.fwriters)) ∧ (idle = idle ∨ idle = ready ∨ idle = crashed → notMember(lsf(t).t, gs.freaders)) ∧ (idle = idle ∨ idle = ready ∨ idle = crashed → noPendingW(lsf(t).t, gs.bq, gs.pq)) ∧ (idle = idle ∨ idle = crashed → noPending(lsf(t).t, gs.bq, gs.pq)) ∧ (idle = idle ∨ idle = ready ∨ idle = crashed → ¬ SF ∈ gs.bq(lsf(t).t)) ∧ (idle = idle ∨ idle = ready ∨ idle = crashed → gs.rfo(lsf(t).t) = gs.bq(lsf(t).t))) ⊦

Rule argument

Additional information

Used terms: gs, lsf(t), idle

Proof step 10 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ ctrok(λ l. 0, λ l. ∅) ∨ ¬ writersOk(λ t. [], λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ noPending(t, bq, pq) → noPendingW(t, bq, pq); (ss) ⊦ R4 ≠ idle; (s) ⊦ R3 ≠ idle; (s) ⊦ R2 ≠ idle; (s) ⊦ R1 ≠ idle; (s) ⊦ W2 ≠ idle; (s) ⊦ W7 ≠ idle; (s) ⊦ W1 ≠ idle; (s) ⊦ W6 ≠ idle; (s) ⊦ W5 ≠ idle; (s) ⊦ W4 ≠ idle; (s) ⊦ W3 ≠ idle; (s)

Proof step 12 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ctrok(ctr, writers) ↔ (∀ l. # writers(l) = ctr(l))

• Proof step 14:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬(∀ l. # ∅ = 0) ∨ ¬ writersOk(λ t. [], λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: λ l. 0, λ l. ∅

Proof step 13 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ writersOk(λ t. [], λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ∅ = 0; (s)

Proof step 15 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ writersOk(bq, p, writers) ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = [] ∧ bq(t) |WL l = []))

• Proof step 17:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬(∀ l, t. (t ∈ ∅ → (∀ l0. l0 ≠ l → ¬ t ∈ ∅)) ∧ (¬ t ∈ ∅ → [] |W | t = [] ∧ [] |WL l = [])) ∨ ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: λ t. [], λ l. [], λ l. ∅

Proof step 16 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ pendingOk(λ t. [], λ l. []) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] |WL l = []; (s) ⊦ [] | t = []; (s) ⊦ [] |W = []; (s) ⊦ ¬ a ∈ ∅; (s)

Proof step 18 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ pendingOk(bq, p) ↔ (∀ l, t. #(p(l) |W | t) + #(bq(t) |WL l) ≤ 1)

• Proof step 20:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬(∀ l, t. #([] |W | t) + #([] |WL l) ≤ 1) ∨ ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: λ t. [], λ l. []

Proof step 19 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ SFTrailing(λ t. []) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # [] = 0; (s) ⊦ [] |WL l = []; (s) ⊦ [] | t = []; (s) ⊦ [] |W = []; (s)

Proof step 21 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ SFTrailing(bq) ↔ (∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast)

• Proof step 23:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬(∀ t. [] = [] ∨ ¬ SF ∈ [].butlast) ∨ ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: λ t. []

Proof step 22 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ readFOsOk(λ t. [], λ l. ∅) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Proof step 24 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ readFOsOk(rfo, writers) ↔ rfo.FOs? ∧ (∀ t, l. t ∈ writers(l) → rfo(t) = [])

• Proof step 26:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬((λ t. []).FOs? ∧ (∀ t, l. t ∈ ∅ → [] = [])) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: λ t. [], λ l. ∅

Proof step 25 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬ (λ t. []).FOs? ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 27 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ rfo.FOs? ↔ (∀ t. rfo(t).forall(.FO?))

• Proof step 29:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, ¬(∀ t. [].forall(.FO?)) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: λ t. []

Proof step 28 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [].forall(p); (s)

Proof step 30 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ notMember(t, tsf) ↔ (∀ l. ¬ t ∈ tsf(l))

• Proof step 32:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬(∀ l. ¬ lsf(t).t ∈ ∅) ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used terms: lsf(t).t, λ l. ∅

Proof step 31 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬ noPending(lsf(t).t, λ t. [], λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 33 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ noPending(t, bq, p) ↔ (∀ l. p(l) | t = [] ∧ bq(t) = [])

• Proof step 35:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬(∀ l. [] | lsf(t).t = [] ∧ [] = []) ⊦

Rule argument

Additional information

Used terms: lsf(t).t, λ t. [], λ l. []

Proof step 34 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), lsf(t).t ≠ t, ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s)

Proof step 36 from proof init-state-inv (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t