Proof step 1 from proof step-absstep-W5-W6-tau-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ags.ctr = gs.fctr, ls.loc = als.l, ags.mem = gs.pmem, gs0.rfo(t) = [], gs.rfo(t) = [], ls.t = als.t, lsf(t).t = t, alsf(t).t = t, ls.val = als.v, ags.writers = gs.fwriters, W6 = pcstepf(gs, ls, W5, τ), alsf(t) = als, apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5)), apcf(t) = apc, gs0 = gstepf(gs, ls, W5, τ), ls0 = lstepf(gs, ls, W5, τ), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = W5, pcf0(t) = W6, FLITPSCLInv(ags, als, apc), FOFollowsW(t, gs0.bq(t), gs0.pq(ls0.loc), ls0.loc), FOFollowsW(t, gs.bq(t), gs.pq(ls.loc), ls.loc), SFTrailing(gs0.bq), SFTrailing(gs.bq), ctrok(ags.ctr, ags.writers), ctrok(gs0.fctr, gs0.fwriters), ctrok(gs.fctr, gs.fwriters), notMember(t, gs0.freaders), notMember(t, gs.freaders), oneMember(t, ls0.loc, gs0.fwriters), oneMember(t, ls.loc, gs.fwriters), pendingOk(ags.p), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), pre(gs, ls, W5, τ), readFOsOk(gs0.rfo, gs0.fwriters), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags.p, ags.writers), writersOk(gs0.bq, gs0.pq, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val), gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. t0 ≠ t → alsf(t0).t = t0, ∀ t0. t0 ≠ t → lsf(t0).t = t0, gs0.bq(t) = [] ∨ gs0.bq(t) = SF ' ∨ gs0.bq(t) = FO(ls0.loc) ' + SF ' ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ' + FO(ls0.loc) ' + SF ', gs.bq(t) = [] ∨ gs.bq(t) = FO(ls.loc) ' ∨ gs.bq(t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' ⊦ (ags.mem = gs0.pmem ∧ ags.ctr = gs0.fctr ∧ reorder(ags.p, gs0.pq, gs0.rfo) ∧ ags.writers = gs0.fwriters) ∧ ls0.t = als.t ∧ apc = (W(ls0.loc, ls0.val) ∈ gs0.bq(ls0.t) ⊃ W3;(FO(ls0.loc) ∈ gs0.bq(ls0.t) ⊃ W4;(SF ∈ gs0.bq(ls0.t) ⊃ W5;W6))) ∧ ls0.loc = als.l ∧ ls0.val = als.v

Rule argument

Additional information

Proof step 2 from proof step-absstep-W5-W6-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ FO(l) ≠ SF; (s) ⊦ W(l, v) ≠ SF; (s) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ x + a = x + a '; (s) ⊦ gstepf(gs, ls, W5, τ) = gs.bq:= gs.bq(ls.t := gs.bq(ls.t) + SF); (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).rfo = gs.rfo; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ (gs.bq:= bq).pmem = gs.pmem; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ x + y = z + y ↔ x = z; (s) ⊦ x = y + x ↔ y = []; (s) ⊦ SFTrailing(bq(t := bq(t) + be ')) ↔ SFTrailing(bq) ∧ ¬ SF ∈ bq(t); (s) ⊦ (gs.bq:= bq).freaders = gs.freaders; (s) ⊦ pre(gs, ls, W5, a) ↔ a = τ; (s) ⊦ pcstepf(gs, ls, W5, a) = W6; (s) ⊦ lstepf(gs, ls, W5, τ) = ls; (s)