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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid)) ⊦ ⟪fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.bq(tid) ≠ [], n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ⟪fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 4:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ⟪PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  bq = gs.bq, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ⟪PROP_FO(tid, l, gs.fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

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

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 6:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ⟪choose n with n < # bq(tid) ∧ isPropFO(n, l, bq(tid)) in pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n) ifnone skip; gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

Used simplifier rules: decl: PROP_FO(tid, l, fwriters; pq, bq, rfo) {choose n with n < # bq(tid) ∧ isPropFO(n, l, bq(tid)) in pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n) ifnone skip };

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

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 7:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # bq(tid), n0 < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, bq(tid)), isPropFO(n0, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ⟪pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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 16:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ∀ n. ¬(n < # bq(tid) ∧ isPropFO(n, l, bq(tid))) ⊦ ⟪skip; gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 8:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n0 < # gs.bq(tid), n < # bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n0, l, gs.bq(tid)), isPropFO(n, l, bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ⟪gs := ((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))⟫ ( 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))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 9:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # bq(tid), n0 < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, bq(tid)), isPropFO(n0, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ctrok ((((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).fctr, (((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).fwriters) ∧ writersOk ((((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).bq, (((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).pq, (((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).fwriters) ∧ pendingOk ((((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).bq, (((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).pq) ∧ SFTrailing((((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).bq) ∧ readFOsOk ((((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).rfo, (((gs.pq:= pq(l := pq(l) + FO(tid))).bq:= bq(tid := bq(tid) -p n)).rfo:= rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n))).fwriters)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  gs.bq(tid) ≠ [], n0 < # gs.bq(tid), n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n0, l, gs.bq(tid)), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ readFOsOk(gs.rfo(tid := (tid ∈ gs.fwriters(l) ⊃ gs.rfo(tid);gs.rfo(tid) -p n)), gs.fwriters) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.rfo:= bq0).fwriters = gs.fwriters; (s) ⊦ x + a = x + a '; (s) ⊦ (gs.rfo:= bq0).rfo = bq0; (s) ⊦ SFTrailing(bq) ∧ isPropFO(n, l, bq(t)) → SFTrailing(bq(t := bq(t) -p n)); (ss) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ (gs.rfo:= bq0).bq = gs.bq; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ pendingOk(bq, pq) ∧ isPropFO(n, l, bq(t)) → pendingOk(bq(t := bq(t) -p n), pq(l := pq(l) + FO(t) ')); (ss) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ (gs.rfo:= bq0).pq = gs.pq; (s) ⊦ writersOk(bq, pq, writers) ∧ isPropFO(n, l, bq(t)) → writersOk(bq(t := bq(t) -p n), pq(l := pq(l) + FO(t) '), writers); (ss) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ (gs.rfo:= bq0).fctr = gs.fctr; (s)

Proof step 10 from proof step-PROP_FO (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  gs.bq(tid) ≠ [], n < # gs.bq(tid), n0 < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), isPropFO(n0, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), tid ∈ gs.fwriters(l), ¬ readFOsOk(gs.rfo(tid := gs.rfo(tid)), gs.fwriters) ⊦

• Proof step 14:

  gs.bq(tid) ≠ [], n < # gs.bq(tid), n0 < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), isPropFO(n0, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ readFOsOk(gs.rfo(tid := gs.rfo(tid) -p n), gs.fwriters), ¬ tid ∈ gs.fwriters(l) ⊦

Rule argument

Additional information

Proof step 11 from proof step-PROP_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gs.rfo(tid) = [], gs.bq(tid) ≠ [], gs.fctr(l) ≠ 0, gs.fwriters(l) ≠ ∅, n0 < # gs.bq(tid), n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n0, l, gs.bq(tid)), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), tid ∈ gs.fwriters(l), ¬ readFOsOk(gs.rfo(tid := []), gs.fwriters) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ctrok(ctr, writers) → # writers(l) = ctr(l); (s) size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic readFOsOk-empty-rfo-while-writing: ⊦ readFOsOk(rfo, writers) ∧ t ∈ writers(l) → rfo(t) = []; (forward) from specification FLIT-preds

Proof step 12 from proof step-PROP_FO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  gs.rfo(tid := []) = gs.rfo, gs.rfo(tid) = [], gs.bq(tid) ≠ [], gs.fctr(l) ≠ 0, gs.fwriters(l) ≠ ∅, n < # gs.bq(tid), n0 < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), isPropFO(n0, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), tid ∈ gs.fwriters(l), ¬ readFOsOk(gs.rfo(tid := []), gs.fwriters) ⊦

Rule argument

Additional information

Used formulas: gs.rfo(tid := []) = gs.rfo

Proof step 13 from proof step-PROP_FO (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Proof step 14 from proof step-PROP_FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ readFOsOk(rfo, writers) → readFOsOk(rfo(t := rfo(t) -p n), writers)

Rule argument

Additional information

Used terms: gs.rfo, tid, n, gs.fwriters

Proof step 15 from proof step-PROP_FO (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof step-PROP_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 17:

  bq = gs.bq, fwriters = gs.fwriters, pq = gs.pq, rfo = gs.rfo, gs.bq(tid) ≠ [], n < # gs.bq(tid), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), isPropFO(n, l, gs.bq(tid)), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ∀ n. ¬(n < # bq(tid) ∧ isPropFO(n, l, bq(tid))) ⊦ ⟪gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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))

Rule argument

Additional information

Proof step 17 from proof step-PROP_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.rfo:= bq0).fctr = gs.fctr; (s) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.rfo:= bq0).pq = gs.pq; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.rfo:= bq0).bq = gs.bq; (s) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ (gs.rfo:= bq0).rfo = bq0; (s) ⊦ (gs.rfo:= bq0).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s)