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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pre(gs, ls, W6, a), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), 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 ' ⊦ ∀ fl. (ls.loc = fl ⊃ gs.fctr(ls.loc) ≥ 1;true)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ oneMember(t, l, writers) ∧ ctrok(ctr, writers) → ctr(l) ≠ 0; (as) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n ≥ m ↔ m ≤ n; (s) ⊦ pre(gs, ls, W6, a) ↔ (gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l))) ∧ a = ctrDec(ls.t, ls.loc); (s)