Proof step 1 from proof not-pre-global-persist (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pre(gs, ls, pc, globalPSCPERSIST_W(l)) ⊦

Rule argument

Additional information

Proof step 2 from proof not-pre-global-persist (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: gen-FLITPSCPC: ⊦ ; pre-R1: ⊦ pre(gs, ls, R1, a) ↔ a = doReadPSC(ls.t, ls.l, ((gs.mem ⊕ gs.p))(ls.l)); disj-doReadPSC-globalPSCPERSISTuscW: ⊦ doReadPSC(t, l, v) ≠ globalPSCPERSIST_W(l0); pre-R2: ⊦ pre(gs, ls, R2, a) ↔ a = ctrReadPSC(ls.t, ls.l, gs.ctr(ls.l)); disj-ctrReadPSC-globalPSCPERSISTuscW: ⊦ ctrReadPSC(t, l, n) ≠ globalPSCPERSIST_W(l0); pre-R3: ⊦ pre(gs, ls, R3, a) ↔ a = pwbPSC(ls.t, ls.l); disj-globalPSCPERSISTuscW-pwbPSC: ⊦ globalPSCPERSIST_W(l) ≠ pwbPSC(t, l0); pre-R4: ⊦ pre(gs, ls, R4, a) ↔ a = retFLITPSCREAD(ls.t, ls.v); disj-globalPSCPERSISTuscW-retFLITPSCREAD: ⊦ globalPSCPERSIST_W(l) ≠ retFLITPSCREAD(t, v); pre-W1: ⊦ pre(gs, ls, W1, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t); disj-globalPSCPERSISTuscW-sfencePSC: ⊦ globalPSCPERSIST_W(l) ≠ sfencePSC(t); pre-W2: ⊦ pre(gs, ls, W2, a) ↔ a = ctrIncPSC(ls.t, ls.l); disj-ctrIncPSC-globalPSCPERSISTuscW: ⊦ ctrIncPSC(t, l) ≠ globalPSCPERSIST_W(l0); pre-W3: ⊦ pre(gs, ls, W3, a) ↔ a = doWritePSC(ls.t, ls.l, ls.v); disj-doWritePSC-globalPSCPERSISTuscW: ⊦ doWritePSC(t, l, v) ≠ globalPSCPERSIST_W(l0); pre-W4: ⊦ pre(gs, ls, W4, a) ↔ a = pwbPSC(ls.t, ls.l); disj-globalPSCPERSISTuscW-pwbPSC: ⊦ globalPSCPERSIST_W(l) ≠ pwbPSC(t, l0); pre-W5: ⊦ pre(gs, ls, W5, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t); disj-globalPSCPERSISTuscW-sfencePSC: ⊦ globalPSCPERSIST_W(l) ≠ sfencePSC(t); pre-W6: ⊦ pre(gs, ls, W6, a) ↔ a = ctrDecPSC(ls.t, ls.l); disj-ctrDecPSC-globalPSCPERSISTuscW: ⊦ ctrDecPSC(t, l) ≠ globalPSCPERSIST_W(l0); pre-W7: ⊦ pre(gs, ls, W7, a) ↔ a = retFLITPSCWRITE(ls.t); disj-globalPSCPERSISTuscW-retFLITPSCWRITE: ⊦ globalPSCPERSIST_W(l) ≠ retFLITPSCWRITE(t); pre-crashed: ⊦ pre(gs, ls, crashed, a) ↔ false; pre-idle: ⊦ pre(gs, ls, idle, a) ↔ a = callPSCRUN(ls.t); disj-callPSCRUN-globalPSCPERSISTuscW: ⊦ callPSCRUN(t) ≠ globalPSCPERSIST_W(l); pre-ready: ⊦ pre(gs, ls, ready, a) ↔ (∃ l0, v0. a = invFLITPSCWRITE(ls.t, l0, v0)) ∨ (∃ l0. a = invFLITPSCREAD(ls.t, l0)) ∨ a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)); disj-globalPSCPERSISTuscW-invFLITPSCWRITE: ⊦ globalPSCPERSIST_W(l) ≠ invFLITPSCWRITE(t, l0, v); disj-globalPSCPERSISTuscW-invFLITPSCREAD: ⊦ globalPSCPERSIST_W(l) ≠ invFLITPSCREAD(t, l0); disj-callPSCCOMPLETE-globalPSCPERSISTuscW: ⊦ callPSCCOMPLETE(t) ≠ globalPSCPERSIST_W(l); ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s)