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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pre(gs, ls, pc, globalPSCCRASH) ⊦

Rule argument

Additional information

Proof step 2 from proof not-pre-global-crash (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-globalPSCCRASH: ⊦ doReadPSC(t, l, v) ≠ globalPSCCRASH; pre-R2: ⊦ pre(gs, ls, R2, a) ↔ a = ctrReadPSC(ls.t, ls.l, gs.ctr(ls.l)); disj-ctrReadPSC-globalPSCCRASH: ⊦ ctrReadPSC(t, l, n) ≠ globalPSCCRASH; pre-R3: ⊦ pre(gs, ls, R3, a) ↔ a = pwbPSC(ls.t, ls.l); disj-globalPSCCRASH-pwbPSC: ⊦ globalPSCCRASH ≠ pwbPSC(t, l); pre-R4: ⊦ pre(gs, ls, R4, a) ↔ a = retFLITPSCREAD(ls.t, ls.v); disj-globalPSCCRASH-retFLITPSCREAD: ⊦ globalPSCCRASH ≠ retFLITPSCREAD(t, v); pre-W1: ⊦ pre(gs, ls, W1, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t); disj-globalPSCCRASH-sfencePSC: ⊦ globalPSCCRASH ≠ sfencePSC(t); pre-W2: ⊦ pre(gs, ls, W2, a) ↔ a = ctrIncPSC(ls.t, ls.l); disj-ctrIncPSC-globalPSCCRASH: ⊦ ctrIncPSC(t, l) ≠ globalPSCCRASH; pre-W3: ⊦ pre(gs, ls, W3, a) ↔ a = doWritePSC(ls.t, ls.l, ls.v); disj-doWritePSC-globalPSCCRASH: ⊦ doWritePSC(t, l, v) ≠ globalPSCCRASH; pre-W4: ⊦ pre(gs, ls, W4, a) ↔ a = pwbPSC(ls.t, ls.l); disj-globalPSCCRASH-pwbPSC: ⊦ globalPSCCRASH ≠ pwbPSC(t, l); pre-W5: ⊦ pre(gs, ls, W5, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t); disj-globalPSCCRASH-sfencePSC: ⊦ globalPSCCRASH ≠ sfencePSC(t); pre-W6: ⊦ pre(gs, ls, W6, a) ↔ a = ctrDecPSC(ls.t, ls.l); disj-ctrDecPSC-globalPSCCRASH: ⊦ ctrDecPSC(t, l) ≠ globalPSCCRASH; pre-W7: ⊦ pre(gs, ls, W7, a) ↔ a = retFLITPSCWRITE(ls.t); disj-globalPSCCRASH-retFLITPSCWRITE: ⊦ globalPSCCRASH ≠ retFLITPSCWRITE(t); pre-crashed: ⊦ pre(gs, ls, crashed, a) ↔ false; pre-idle: ⊦ pre(gs, ls, idle, a) ↔ a = callPSCRUN(ls.t); disj-callPSCRUN-globalPSCCRASH: ⊦ callPSCRUN(t) ≠ globalPSCCRASH; 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-globalPSCCRASH-invFLITPSCWRITE: ⊦ globalPSCCRASH ≠ invFLITPSCWRITE(t, l, v); disj-globalPSCCRASH-invFLITPSCREAD: ⊦ globalPSCCRASH ≠ invFLITPSCREAD(t, l); disj-callPSCCOMPLETE-globalPSCCRASH: ⊦ callPSCCOMPLETE(t) ≠ globalPSCCRASH; ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s)