This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| alltids-nonempty | ⊦ alltids ≠ ∅ | An Axiom |
| alltids-all | ⊦ tid ∈ alltids | An Axiom |
| lstep | ⊦ lstep(gs, ls, pc, a, gs0, ls0, pc0) ↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a) | An Axiom |
| pre-L1 | ⊦ pre(gs, ls, L1, a) ↔ a = τ | An Axiom |
| lstepf-L1 | ⊦ lstepf(gs, ls, L1, τ) = ls | An Axiom |
| gstepf-L1 | ⊦ gstepf(gs, ls, L1, τ) = gs | An Axiom |
| pcstepf-L1 | ⊦ pcstepf(gs, ls, L1, a) = (gs.gspmx ≠ ∅ ⊃ L2;L8) | An Axiom |
| pre-L2 | ⊦ pre(gs, ls, L2, a) ↔ (∃ lspmx0. (lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx) ∧ a = chooseL2(lspmx0)) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx) | An Axiom |
| lstepf-L2-0 | ⊦ lstepf(gs, ls, L2, τ) = ls | An Axiom |
| lstepf-L2-1 | ⊦ lstepf(gs, ls, L2, chooseL2(lspmx0)) = ls.lspmx:= lspmx0 | An Axiom |
| gstepf-L2-0 | ⊦ gstepf(gs, ls, L2, τ) = gs | An Axiom |
| gstepf-L2-1 | ⊦ gstepf(gs, ls, L2, chooseL2(lspmx0)) = (gs.gspmx:= (gs.gspmx \ dom (ls.lspmx:= lspmx0).lspmx)).ghostlspmxf:= gs.ghostlspmxf((ls.lspmx:= lspmx0).tid; (ls.lspmx:= lspmx0).lspmx) | An Axiom |
| pcstepf-L2 | ⊦ pcstepf(gs, ls, L2, a) = (∃ lspmx0. a = chooseL2(lspmx0) ⊃ L3;L1) | An Axiom |
| pre-L3 | ⊦ pre(gs, ls, L3, a) ↔ a = τ | An Axiom |
| lstepf-L3 | ⊦ lstepf(gs, ls, L3, τ) = ls | An Axiom |
| gstepf-L3 | ⊦ gstepf(gs, ls, L3, τ) = gs | An Axiom |
| pcstepf-L3 | ⊦ pcstepf(gs, ls, L3, a) = (ls.lspmx ≠ ∅ ⊃ L4;L1) | An Axiom |
| pre-L4 | ⊦ pre(gs, ls, L4, a) ↔ (∃ np0. np0 ∈ ls.lspmx ∧ a = chooseL4(np0)) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ls.lspmx) | An Axiom |
| lstepf-L4-0 | ⊦ lstepf(gs, ls, L4, chooseL4(np0)) = ls.np:= np0 | An Axiom |
| lstepf-L4-1 | ⊦ lstepf(gs, ls, L4, τ) = ls | An Axiom |
| gstepf-L4 | ⊦ gstepf(gs, ls, L4, a) = gs | An Axiom |
| pcstepf-L4 | ⊦ pcstepf(gs, ls, L4, a) = (∃ np0. a = chooseL4(np0) ⊃ L5;L0) | An Axiom |
| pre-L5 | ⊦ pre(gs, ls, L5, a) ↔ a = τ | An Axiom |
| lstepf-L5 | ⊦ lstepf(gs, ls, L5, τ) = ls.val:= gs.y[ls.np.r] | An Axiom |
| gstepf-L5 | ⊦ gstepf(gs, ls, L5, τ) = gs | An Axiom |
| pcstepf-L5 | ⊦ pcstepf(gs, ls, L5, a) = L6 | An Axiom |
| pre-L6 | ⊦ pre(gs, ls, L6, a) ↔ a = τ | An Axiom |
| lstepf-L6 | ⊦ lstepf(gs, ls, L6, a) = ls | An Axiom |
| gstepf-L6 | ⊦ gstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ (gs.y:= gs.y[ls.np.r, ls.val + ls.lspmx[ls.np] * gs.x[ls.np.c]]).ghostlspmxf:= gs.ghostlspmxf(ls.tid; gs.ghostlspmxf(ls.tid) -- ls.np) ;gs ) | An Axiom |
| pcstepf-L6 | ⊦ pcstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ L7;L3) | An Axiom |
| pre-L0 | ⊦ pre(gs, ls, L0, a) ↔ a = τ | An Axiom |
| lstepf-L0 | ⊦ lstepf(gs, ls, L0, τ) = ls | An Axiom |
| gstepf-L0 | ⊦ gstepf(gs, ls, L0, τ) = gs | An Axiom |
| pcstepf-L0 | ⊦ pcstepf(gs, ls, L0, a) = L3 | An Axiom |
| pre-L7 | ⊦ pre(gs, ls, L7, a) ↔ a = τ | An Axiom |
| lstepf-L7 | ⊦ lstepf(gs, ls, L7, τ) = ls.lspmx:= (ls.lspmx -- ls.np) | An Axiom |
| gstepf-L7 | ⊦ gstepf(gs, ls, L7, τ) = gs | An Axiom |
| pcstepf-L7 | ⊦ pcstepf(gs, ls, L7, a) = L3 | An Axiom |
| pre-I | ⊦ pre(gs, ls, I, a) ↔ a = invCMULT#(ls.tid) | An Axiom |
| gstepf-I | ⊦ gstepf(gs, ls, I, a) = gs | An Axiom |
| lstepf-I-CMULT | ⊦ lstepf(gs, ls, I, invCMULT#(ls.tid)) = ls | An Axiom |
| pcstepf-I-CMULT | ⊦ pcstepf(gs, ls, I, invCMULT#(ls.tid)) = L1 | An Axiom |
| gen-01 | VF3concAction freely generated by τ, invCMULT#, retCMULT#, chooseL4, chooseL2; | An Axiom |
| gen-02 | VF3concState freely generated by mkstate; | An Axiom |
| gen-04 | VF3concGState freely generated by mkgs; | An Axiom |
| case-01 | ⊦ a = τ ∨ a = invCMULT#(a.tid) ∨ a = retCMULT#(a.tid) ∨ a = chooseL4(a.np) ∨ a = chooseL2(a.lspmx) | An Axiom |
| inj-01 | ⊦ invCMULT#(tid) = invCMULT#(tid0) ↔ tid = tid0 | An Axiom |
| inj-02 | ⊦ retCMULT#(tid) = retCMULT#(tid0) ↔ tid = tid0 | An Axiom |
| inj-03 | ⊦ chooseL4(np) = chooseL4(np0) ↔ np = np0 | An Axiom |
| inj-04 | ⊦ chooseL2(lspmx) = chooseL2(lspmx0) ↔ lspmx = lspmx0 | An Axiom |
| sel-01 | ⊦ invCMULT#(tid).tid = tid | An Axiom |
| sel-02 | ⊦ retCMULT#(tid).tid = tid | An Axiom |
| sel-03 | ⊦ chooseL4(np).np = np | An Axiom |
| sel-04 | ⊦ chooseL2(lspmx).lspmx = lspmx | An Axiom |
| disj-01 | ⊦ chooseL4(np) ≠ chooseL2(lspmx) | An Axiom |
| disj-02 | ⊦ retCMULT#(tid) ≠ chooseL2(lspmx) | An Axiom |
| disj-03 | ⊦ retCMULT#(tid) ≠ chooseL4(np) | An Axiom |
| disj-04 | ⊦ invCMULT#(tid) ≠ chooseL2(lspmx) | An Axiom |
| disj-05 | ⊦ invCMULT#(tid) ≠ chooseL4(np) | An Axiom |
| disj-06 | ⊦ invCMULT#(tid) ≠ retCMULT#(tid0) | An Axiom |
| disj-07 | ⊦ τ ≠ chooseL2(lspmx) | An Axiom |
| disj-08 | ⊦ τ ≠ chooseL4(np) | An Axiom |
| disj-09 | ⊦ τ ≠ retCMULT#(tid) | An Axiom |
| disj-10 | ⊦ τ ≠ invCMULT#(tid) | An Axiom |
| elim-01 | ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf) | An Axiom |
| case-02 | ⊦ mkstate(s.gstate, s.lsf, s.pcf) = s | An Axiom |
| inj-05 | ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0 | An Axiom |
| updsel-01 | ⊦ (s.gstate:= gstate).gstate = gstate | An Axiom |
| updsel-02 | ⊦ (s.lsf:= lsf).gstate = s.gstate | An Axiom |
| updsel-03 | ⊦ (s.pcf:= pcf).gstate = s.gstate | An Axiom |
| updsel-04 | ⊦ (s.gstate:= gstate).lsf = s.lsf | An Axiom |
| updsel-05 | ⊦ (s.lsf:= lsf).lsf = lsf | An Axiom |
| updsel-06 | ⊦ (s.pcf:= pcf).lsf = s.lsf | An Axiom |
| updsel-07 | ⊦ (s.gstate:= gstate).pcf = s.pcf | An Axiom |
| updsel-08 | ⊦ (s.lsf:= lsf).pcf = s.pcf | An Axiom |
| updsel-09 | ⊦ (s.pcf:= pcf).pcf = pcf | An Axiom |
| upd-01 | ⊦ (mkstate(gstate, lsf, pcf).gstate:= gstate0) = mkstate(gstate0, lsf, pcf) | An Axiom |
| upd-02 | ⊦ (mkstate(gstate, lsf, pcf).lsf:= lsf0) = mkstate(gstate, lsf0, pcf) | An Axiom |
| upd-03 | ⊦ (mkstate(gstate, lsf, pcf).pcf:= pcf0) = mkstate(gstate, lsf, pcf0) | An Axiom |
| sel-05 | ⊦ mkstate(gstate, lsf, pcf).gstate = gstate | An Axiom |
| sel-06 | ⊦ mkstate(gstate, lsf, pcf).lsf = lsf | An Axiom |
| sel-07 | ⊦ mkstate(gstate, lsf, pcf).pcf = pcf | An Axiom |
| updsel-10 | ⊦ (ls.tid:= tid).tid = tid | An Axiom |
| updsel-11 | ⊦ (ls.lspmx:= lspmx).tid = ls.tid | An Axiom |
| updsel-12 | ⊦ (ls.np:= np).tid = ls.tid | An Axiom |
| updsel-13 | ⊦ (ls.tid:= tid).lspmx = ls.lspmx | An Axiom |
| updsel-14 | ⊦ (ls.lspmx:= lspmx).lspmx = lspmx | An Axiom |
| updsel-15 | ⊦ (ls.np:= np).lspmx = ls.lspmx | An Axiom |
| updsel-16 | ⊦ (ls.tid:= tid).np = ls.np | An Axiom |
| updsel-17 | ⊦ (ls.lspmx:= lspmx).np = ls.np | An Axiom |
| updsel-18 | ⊦ (ls.np:= np).np = np | An Axiom |
| elim-03 | ⊦ ((((spmx = gs.spmx ∧ gspmx = gs.gspmx) ∧ r = gs.r) ∧ x = gs.x) ∧ y = gs.y) ∧ ghostlspmxf = gs.ghostlspmxf ↔ gs = mkgs(spmx, gspmx, r, x, y, ghostlspmxf) | An Axiom |
| case-04 | ⊦ mkgs(gs.spmx, gs.gspmx, gs.r, gs.x, gs.y, gs.ghostlspmxf) = gs | An Axiom |
| inj-07 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf) = mkgs(spmx1, spmx2, r0, x1, x2, ghostlspmxf0) ↔ spmx = spmx1 ∧ spmx0 = spmx2 ∧ r = r0 ∧ x = x1 ∧ x0 = x2 ∧ ghostlspmxf = ghostlspmxf0 | An Axiom |
| updsel-19 | ⊦ (gs.spmx:= spmx).spmx = spmx | An Axiom |
| updsel-20 | ⊦ (gs.gspmx:= spmx0).spmx = gs.spmx | An Axiom |
| updsel-21 | ⊦ (gs.r:= r).spmx = gs.spmx | An Axiom |
| updsel-22 | ⊦ (gs.x:= x).spmx = gs.spmx | An Axiom |
| updsel-23 | ⊦ (gs.y:= x0).spmx = gs.spmx | An Axiom |
| updsel-24 | ⊦ (gs.ghostlspmxf:= ghostlspmxf).spmx = gs.spmx | An Axiom |
| updsel-25 | ⊦ (gs.spmx:= spmx).gspmx = gs.gspmx | An Axiom |
| updsel-26 | ⊦ (gs.gspmx:= spmx0).gspmx = spmx0 | An Axiom |
| updsel-27 | ⊦ (gs.r:= r).gspmx = gs.gspmx | An Axiom |
| updsel-28 | ⊦ (gs.x:= x).gspmx = gs.gspmx | An Axiom |
| updsel-29 | ⊦ (gs.y:= x0).gspmx = gs.gspmx | An Axiom |
| updsel-30 | ⊦ (gs.ghostlspmxf:= ghostlspmxf).gspmx = gs.gspmx | An Axiom |
| updsel-31 | ⊦ (gs.spmx:= spmx).r = gs.r | An Axiom |
| updsel-32 | ⊦ (gs.gspmx:= spmx0).r = gs.r | An Axiom |
| updsel-33 | ⊦ (gs.r:= r).r = r | An Axiom |
| updsel-34 | ⊦ (gs.x:= x).r = gs.r | An Axiom |
| updsel-35 | ⊦ (gs.y:= x0).r = gs.r | An Axiom |
| updsel-36 | ⊦ (gs.ghostlspmxf:= ghostlspmxf).r = gs.r | An Axiom |
| updsel-37 | ⊦ (gs.spmx:= spmx).x = gs.x | An Axiom |
| updsel-38 | ⊦ (gs.gspmx:= spmx0).x = gs.x | An Axiom |
| updsel-39 | ⊦ (gs.r:= r).x = gs.x | An Axiom |
| updsel-40 | ⊦ (gs.x:= x).x = x | An Axiom |
| updsel-41 | ⊦ (gs.y:= x0).x = gs.x | An Axiom |
| updsel-42 | ⊦ (gs.ghostlspmxf:= ghostlspmxf).x = gs.x | An Axiom |
| updsel-43 | ⊦ (gs.spmx:= spmx).y = gs.y | An Axiom |
| updsel-44 | ⊦ (gs.gspmx:= spmx0).y = gs.y | An Axiom |
| updsel-45 | ⊦ (gs.r:= r).y = gs.y | An Axiom |
| updsel-46 | ⊦ (gs.x:= x).y = gs.y | An Axiom |
| updsel-47 | ⊦ (gs.y:= x0).y = x0 | An Axiom |
| updsel-48 | ⊦ (gs.ghostlspmxf:= ghostlspmxf).y = gs.y | An Axiom |
| updsel-49 | ⊦ (gs.spmx:= spmx).ghostlspmxf = gs.ghostlspmxf | An Axiom |
| updsel-50 | ⊦ (gs.gspmx:= spmx0).ghostlspmxf = gs.ghostlspmxf | An Axiom |
| updsel-51 | ⊦ (gs.r:= r).ghostlspmxf = gs.ghostlspmxf | An Axiom |
| updsel-52 | ⊦ (gs.x:= x).ghostlspmxf = gs.ghostlspmxf | An Axiom |
| updsel-53 | ⊦ (gs.y:= x0).ghostlspmxf = gs.ghostlspmxf | An Axiom |
| updsel-54 | ⊦ (gs.ghostlspmxf:= ghostlspmxf).ghostlspmxf = ghostlspmxf | An Axiom |
| upd-07 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).spmx:= spmx1 = mkgs(spmx1, spmx0, r, x, x0, ghostlspmxf) | An Axiom |
| upd-08 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).gspmx:= spmx2 = mkgs(spmx, spmx2, r, x, x0, ghostlspmxf) | An Axiom |
| upd-09 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).r:= r0 = mkgs(spmx, spmx0, r0, x, x0, ghostlspmxf) | An Axiom |
| upd-10 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).x:= x1 = mkgs(spmx, spmx0, r, x1, x0, ghostlspmxf) | An Axiom |
| upd-11 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).y:= x2 = mkgs(spmx, spmx0, r, x, x2, ghostlspmxf) | An Axiom |
| upd-12 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).ghostlspmxf:= ghostlspmxf0 = mkgs(spmx, spmx0, r, x, x0, ghostlspmxf0) | An Axiom |
| sel-11 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).spmx = spmx | An Axiom |
| sel-12 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).gspmx = spmx0 | An Axiom |
| sel-13 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).r = r | An Axiom |
| sel-14 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).x = x | An Axiom |
| sel-15 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).y = x0 | An Axiom |
| sel-16 | ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).ghostlspmxf = ghostlspmxf | An Axiom |
| disj-11 | ⊦ L2 ≠ L0 | An Axiom |
| disj-12 | ⊦ L7 ≠ L0 | An Axiom |
| disj-13 | ⊦ L7 ≠ L2 | An Axiom |
| disj-14 | ⊦ L3 ≠ L0 | An Axiom |
| disj-15 | ⊦ L3 ≠ L2 | An Axiom |
| disj-16 | ⊦ L3 ≠ L7 | An Axiom |
| disj-17 | ⊦ L6 ≠ L0 | An Axiom |
| disj-18 | ⊦ L6 ≠ L2 | An Axiom |
| disj-19 | ⊦ L6 ≠ L7 | An Axiom |
| disj-20 | ⊦ L6 ≠ L3 | An Axiom |
| disj-21 | ⊦ L4 ≠ L0 | An Axiom |
| disj-22 | ⊦ L4 ≠ L2 | An Axiom |
| disj-23 | ⊦ L4 ≠ L7 | An Axiom |
| disj-24 | ⊦ L4 ≠ L3 | An Axiom |
| disj-25 | ⊦ L4 ≠ L6 | An Axiom |
| disj-26 | ⊦ L5 ≠ L0 | An Axiom |
| disj-27 | ⊦ L5 ≠ L2 | An Axiom |
| disj-28 | ⊦ L5 ≠ L7 | An Axiom |
| disj-29 | ⊦ L5 ≠ L3 | An Axiom |
| disj-30 | ⊦ L5 ≠ L6 | An Axiom |
| disj-31 | ⊦ L5 ≠ L4 | An Axiom |
| disj-32 | ⊦ L1 ≠ L0 | An Axiom |
| disj-33 | ⊦ L1 ≠ L2 | An Axiom |
| disj-34 | ⊦ L1 ≠ L7 | An Axiom |
| disj-35 | ⊦ L1 ≠ L3 | An Axiom |
| disj-36 | ⊦ L1 ≠ L6 | An Axiom |
| disj-37 | ⊦ L1 ≠ L4 | An Axiom |
| disj-38 | ⊦ L1 ≠ L5 | An Axiom |
| disj-39 | ⊦ F ≠ L0 | An Axiom |
| disj-40 | ⊦ F ≠ L2 | An Axiom |
| disj-41 | ⊦ F ≠ L7 | An Axiom |
| disj-42 | ⊦ F ≠ L3 | An Axiom |
| disj-43 | ⊦ F ≠ L6 | An Axiom |
| disj-44 | ⊦ F ≠ L4 | An Axiom |
| disj-45 | ⊦ F ≠ L5 | An Axiom |
| disj-46 | ⊦ F ≠ L1 | An Axiom |
| disj-47 | ⊦ I ≠ L0 | An Axiom |
| disj-48 | ⊦ I ≠ L2 | An Axiom |
| disj-49 | ⊦ I ≠ L7 | An Axiom |
| disj-50 | ⊦ I ≠ L3 | An Axiom |
| disj-51 | ⊦ I ≠ L6 | An Axiom |
| disj-52 | ⊦ I ≠ L4 | An Axiom |
| disj-53 | ⊦ I ≠ L5 | An Axiom |
| disj-54 | ⊦ I ≠ L1 | An Axiom |
| disj-55 | ⊦ I ≠ F | An Axiom |
| VF3concRely | ⊦ VF3concRely(gs, tid, gs0) ↔ gs.ghostlspmxf(tid) = gs0.ghostlspmxf(tid) ∧ gs0.gspmx ⊆ gs.gspmx | An Axiom |
| VF3concstep | ⊦ VF3concstep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ tid, ls, pc. lstep(gs, lsf(tid), pcf(tid), a, gs0, ls, pc) ∧ lsf0 = lsf(tid; ls) ∧ pcf0 = pcf(tid; pc)) | An Axiom |
| VF3concLInv | ⊦ VF3concLInv(gs, ls, pc) ↔ (pc = L8 ∨ pc = F → gs.gspmx = ∅) ∧ (pc = L3 ∨ pc = L4 ∨ pc = L5 ∨ pc = L6 → gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ (pc = L7 → ls.np ∈ ls.lspmx ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx -- ls.np) ∧ (pc = I ∨ pc = L1 ∨ pc = L2 ∨ pc = L8 ∨ pc = F → gs.ghostlspmxf(ls.tid) = ∅) ∧ (pc = L0 → false) ∧ (pc = L8 → true) ∧ (pc = L1 → true) ∧ (pc = L5 → ls.np ∈ ls.lspmx) ∧ (pc = L4 → ls.lspmx ≠ ∅) ∧ (pc = L6 → ls.np ∈ ls.lspmx) ∧ (pc = L3 → true) ∧ (pc = L7 → true) ∧ (pc = L2 → true) ∧ (pc = L0 → true) | An Axiom |
| VF3concGInv | ⊦ VF3concGInv(gs) ↔ alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x) | An Axiom |
| VF3concInv | ⊦ VF3concInv(gs, lsf, pcf) ↔ VF3concGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ VF3concLInv(gs, lsf(tid), pcf(tid))) | An Axiom |
| gen-03 | VF3concLState freely generated by mkls; | An Axiom |
| gen-05 | VF3concPC freely generated by I, F, L8, L1, L5, L4, L6, L3, L7, L2, L0; | An Axiom |
| case-05 | ⊦ pc = I ∨ pc = F ∨ pc = L8 ∨ pc = L1 ∨ pc = L5 ∨ pc = L4 ∨ pc = L6 ∨ pc = L3 ∨ pc = L7 ∨ pc = L2 ∨ pc = L0 | An Axiom |
| disj-56 | ⊦ L8 ≠ L0 | An Axiom |
| disj-57 | ⊦ L8 ≠ L2 | An Axiom |
| disj-58 | ⊦ L8 ≠ L7 | An Axiom |
| disj-59 | ⊦ L8 ≠ L3 | An Axiom |
| disj-60 | ⊦ L8 ≠ L6 | An Axiom |
| disj-61 | ⊦ L8 ≠ L4 | An Axiom |
| disj-62 | ⊦ L8 ≠ L5 | An Axiom |
| disj-63 | ⊦ L8 ≠ L1 | An Axiom |
| disj-64 | ⊦ F ≠ L8 | An Axiom |
| disj-65 | ⊦ I ≠ L8 | An Axiom |
| pcstepf-L8 | ⊦ pcstepf(gs, ls, L8, a) = F | An Axiom |
| gstepf-L8 | ⊦ gstepf(gs, ls, L8, retCMULT#(ls.tid)) = gs | An Axiom |
| lstepf-L8 | ⊦ lstepf(gs, ls, L8, retCMULT#(ls.tid)) = ls | An Axiom |
| pre-L8 | ⊦ pre(gs, ls, L8, a) ↔ a = retCMULT#(ls.tid) | An Axiom |
| elim-02 | ⊦ ((tid = ls.tid ∧ lspmx = ls.lspmx) ∧ np = ls.np) ∧ val = ls.val ↔ ls = mkls(tid, lspmx, np, val) | An Axiom |
| case-03 | ⊦ mkls(ls.tid, ls.lspmx, ls.np, ls.val) = ls | An Axiom |
| inj-06 | ⊦ mkls(tid, lspmx, np, val) = mkls(tid0, lspmx0, np0, val0) ↔ tid = tid0 ∧ lspmx = lspmx0 ∧ np = np0 ∧ val = val0 | An Axiom |
| updsel-55 | ⊦ (ls.val:= val).tid = ls.tid | An Axiom |
| updsel-56 | ⊦ (ls.val:= val).lspmx = ls.lspmx | An Axiom |
| updsel-57 | ⊦ (ls.val:= val).np = ls.np | An Axiom |
| updsel-58 | ⊦ (ls.tid:= tid).val = ls.val | An Axiom |
| updsel-59 | ⊦ (ls.lspmx:= lspmx).val = ls.val | An Axiom |
| updsel-60 | ⊦ (ls.np:= np).val = ls.val | An Axiom |
| updsel-61 | ⊦ (ls.val:= val).val = val | An Axiom |
| upd-04 | ⊦ mkls(tid, lspmx, np, val).tid:= tid0 = mkls(tid0, lspmx, np, val) | An Axiom |
| upd-05 | ⊦ mkls(tid, lspmx, np, val).lspmx:= lspmx0 = mkls(tid, lspmx0, np, val) | An Axiom |
| upd-06 | ⊦ mkls(tid, lspmx, np, val).np:= np0 = mkls(tid, lspmx, np0, val) | An Axiom |
| upd-13 | ⊦ mkls(tid, lspmx, np, val).val:= val0 = mkls(tid, lspmx, np, val0) | An Axiom |
| sel-08 | ⊦ mkls(tid, lspmx, np, val).tid = tid | An Axiom |
| sel-09 | ⊦ mkls(tid, lspmx, np, val).lspmx = lspmx | An Axiom |
| sel-10 | ⊦ mkls(tid, lspmx, np, val).np = np | An Axiom |
| sel-17 | ⊦ mkls(tid, lspmx, np, val).val = val | An Axiom |
| init | gspmx = spmx ∧ y = mkvector(r) ∧ okspmx(spmx, r, # x) ∧ (∀ tid. ghostlspmxf(tid) = ∅) ⊦ alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), gspmx) ∧ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ gspmx ⊆ spmx ∧ # y = r ∧ okspmx(spmx, r, # x) | A Proof Obligation |
| step-L1-L2 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L1, a) ∧ pcstepf(gs, ls, L1, a) = L2 → ( alldisjointp(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf), gstepf(gs, ls, L1, a).gspmx) ∧ gstepf(gs, ls, L1, a).y + (U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∪ gstepf(gs, ls, L1, a).gspmx ).toMatrix (gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x ) * gstepf(gs, ls, L1, a).x = gstepf(gs, ls, L1, a).spmx.toMatrix(gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x) * gstepf(gs, ls, L1, a).x ∧ U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∪ gstepf(gs, ls, L1, a).gspmx ⊆ gstepf(gs, ls, L1, a).spmx ∧ # gstepf(gs, ls, L1, a).y = gstepf(gs, ls, L1, a).r ∧ okspmx(gstepf(gs, ls, L1, a).spmx, gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x)) ∧ gstepf(gs, ls, L1, a).ghostlspmxf(lstepf(gs, ls, L1, a).tid) = ∅ | A Proof Obligation |
| step-L5-L6 | ⊦ ( ls.np ∈ ls.lspmx ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L5, a) ∧ pcstepf(gs, ls, L5, a) = L6 → lstepf(gs, ls, L5, a).np ∈ lstepf(gs, ls, L5, a).lspmx ∧ ( alldisjointp(alltids, gstepf(gs, ls, L5, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L5, a).ghostlspmxf), gstepf(gs, ls, L5, a).gspmx) ∧ gstepf(gs, ls, L5, a).y + (U(alltids, gstepf(gs, ls, L5, a).ghostlspmxf) ∪ gstepf(gs, ls, L5, a).gspmx ).toMatrix (gstepf(gs, ls, L5, a).r, # gstepf(gs, ls, L5, a).x ) * gstepf(gs, ls, L5, a).x = gstepf(gs, ls, L5, a).spmx.toMatrix(gstepf(gs, ls, L5, a).r, # gstepf(gs, ls, L5, a).x) * gstepf(gs, ls, L5, a).x ∧ U(alltids, gstepf(gs, ls, L5, a).ghostlspmxf) ∪ gstepf(gs, ls, L5, a).gspmx ⊆ gstepf(gs, ls, L5, a).spmx ∧ # gstepf(gs, ls, L5, a).y = gstepf(gs, ls, L5, a).r ∧ okspmx(gstepf(gs, ls, L5, a).spmx, gstepf(gs, ls, L5, a).r, # gstepf(gs, ls, L5, a).x)) ∧ gstepf(gs, ls, L5, a).ghostlspmxf(lstepf(gs, ls, L5, a).tid) = lstepf(gs, ls, L5, a).lspmx | A Proof Obligation |
| step-L4-L5 | ⊦ ( ls.lspmx ≠ ∅ ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L4, a) ∧ pcstepf(gs, ls, L4, a) = L5 → lstepf(gs, ls, L4, a).np ∈ lstepf(gs, ls, L4, a).lspmx ∧ ( alldisjointp(alltids, gstepf(gs, ls, L4, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L4, a).ghostlspmxf), gstepf(gs, ls, L4, a).gspmx) ∧ gstepf(gs, ls, L4, a).y + (U(alltids, gstepf(gs, ls, L4, a).ghostlspmxf) ∪ gstepf(gs, ls, L4, a).gspmx ).toMatrix (gstepf(gs, ls, L4, a).r, # gstepf(gs, ls, L4, a).x ) * gstepf(gs, ls, L4, a).x = gstepf(gs, ls, L4, a).spmx.toMatrix(gstepf(gs, ls, L4, a).r, # gstepf(gs, ls, L4, a).x) * gstepf(gs, ls, L4, a).x ∧ U(alltids, gstepf(gs, ls, L4, a).ghostlspmxf) ∪ gstepf(gs, ls, L4, a).gspmx ⊆ gstepf(gs, ls, L4, a).spmx ∧ # gstepf(gs, ls, L4, a).y = gstepf(gs, ls, L4, a).r ∧ okspmx(gstepf(gs, ls, L4, a).spmx, gstepf(gs, ls, L4, a).r, # gstepf(gs, ls, L4, a).x)) ∧ gstepf(gs, ls, L4, a).ghostlspmxf(lstepf(gs, ls, L4, a).tid) = lstepf(gs, ls, L4, a).lspmx | A Proof Obligation |
| step-L4-L0 | ⊦ ¬ ( ( ls.lspmx ≠ ∅ ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L4, a) ∧ pcstepf(gs, ls, L4, a) = L0) | A Proof Obligation |
| step-L6-L3 | ⊦ ( ls.np ∈ ls.lspmx ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L6, a) ∧ pcstepf(gs, ls, L6, a) = L3 → ( alldisjointp(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf), gstepf(gs, ls, L6, a).gspmx) ∧ gstepf(gs, ls, L6, a).y + (U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∪ gstepf(gs, ls, L6, a).gspmx ).toMatrix (gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x ) * gstepf(gs, ls, L6, a).x = gstepf(gs, ls, L6, a).spmx.toMatrix(gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x) * gstepf(gs, ls, L6, a).x ∧ U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∪ gstepf(gs, ls, L6, a).gspmx ⊆ gstepf(gs, ls, L6, a).spmx ∧ # gstepf(gs, ls, L6, a).y = gstepf(gs, ls, L6, a).r ∧ okspmx(gstepf(gs, ls, L6, a).spmx, gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x)) ∧ gstepf(gs, ls, L6, a).ghostlspmxf(lstepf(gs, ls, L6, a).tid) = lstepf(gs, ls, L6, a).lspmx | A Proof Obligation |
| step-L3-L4 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L3, a) ∧ pcstepf(gs, ls, L3, a) = L4 → lstepf(gs, ls, L3, a).lspmx ≠ ∅ ∧ ( alldisjointp(alltids, gstepf(gs, ls, L3, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L3, a).ghostlspmxf), gstepf(gs, ls, L3, a).gspmx) ∧ gstepf(gs, ls, L3, a).y + (U(alltids, gstepf(gs, ls, L3, a).ghostlspmxf) ∪ gstepf(gs, ls, L3, a).gspmx ).toMatrix (gstepf(gs, ls, L3, a).r, # gstepf(gs, ls, L3, a).x ) * gstepf(gs, ls, L3, a).x = gstepf(gs, ls, L3, a).spmx.toMatrix(gstepf(gs, ls, L3, a).r, # gstepf(gs, ls, L3, a).x) * gstepf(gs, ls, L3, a).x ∧ U(alltids, gstepf(gs, ls, L3, a).ghostlspmxf) ∪ gstepf(gs, ls, L3, a).gspmx ⊆ gstepf(gs, ls, L3, a).spmx ∧ # gstepf(gs, ls, L3, a).y = gstepf(gs, ls, L3, a).r ∧ okspmx(gstepf(gs, ls, L3, a).spmx, gstepf(gs, ls, L3, a).r, # gstepf(gs, ls, L3, a).x)) ∧ gstepf(gs, ls, L3, a).ghostlspmxf(lstepf(gs, ls, L3, a).tid) = lstepf(gs, ls, L3, a).lspmx | A Proof Obligation |
| step-L3-L1 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L3, a) ∧ pcstepf(gs, ls, L3, a) = L1 → ( alldisjointp(alltids, gstepf(gs, ls, L3, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L3, a).ghostlspmxf), gstepf(gs, ls, L3, a).gspmx) ∧ gstepf(gs, ls, L3, a).y + (U(alltids, gstepf(gs, ls, L3, a).ghostlspmxf) ∪ gstepf(gs, ls, L3, a).gspmx ).toMatrix (gstepf(gs, ls, L3, a).r, # gstepf(gs, ls, L3, a).x ) * gstepf(gs, ls, L3, a).x = gstepf(gs, ls, L3, a).spmx.toMatrix(gstepf(gs, ls, L3, a).r, # gstepf(gs, ls, L3, a).x) * gstepf(gs, ls, L3, a).x ∧ U(alltids, gstepf(gs, ls, L3, a).ghostlspmxf) ∪ gstepf(gs, ls, L3, a).gspmx ⊆ gstepf(gs, ls, L3, a).spmx ∧ # gstepf(gs, ls, L3, a).y = gstepf(gs, ls, L3, a).r ∧ okspmx(gstepf(gs, ls, L3, a).spmx, gstepf(gs, ls, L3, a).r, # gstepf(gs, ls, L3, a).x)) ∧ gstepf(gs, ls, L3, a).ghostlspmxf(lstepf(gs, ls, L3, a).tid) = ∅ | A Proof Obligation |
| step-L2-L3 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L2, a) ∧ pcstepf(gs, ls, L2, a) = L3 → ( alldisjointp(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf), gstepf(gs, ls, L2, a).gspmx) ∧ gstepf(gs, ls, L2, a).y + (U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∪ gstepf(gs, ls, L2, a).gspmx ).toMatrix (gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x ) * gstepf(gs, ls, L2, a).x = gstepf(gs, ls, L2, a).spmx.toMatrix(gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x) * gstepf(gs, ls, L2, a).x ∧ U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∪ gstepf(gs, ls, L2, a).gspmx ⊆ gstepf(gs, ls, L2, a).spmx ∧ # gstepf(gs, ls, L2, a).y = gstepf(gs, ls, L2, a).r ∧ okspmx(gstepf(gs, ls, L2, a).spmx, gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x)) ∧ gstepf(gs, ls, L2, a).ghostlspmxf(lstepf(gs, ls, L2, a).tid) = lstepf(gs, ls, L2, a).lspmx | A Proof Obligation |
| rely-L2-L3 | ⊦ ls.tid ≠ tid0 ∧ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L2, a) ∧ pcstepf(gs, ls, L2, a) = L3 → gs.ghostlspmxf(tid0) = gstepf(gs, ls, L2, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L2, a).gspmx ⊆ gs.gspmx | A Proof Obligation |
| step-L2-L1 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L2, a) ∧ pcstepf(gs, ls, L2, a) = L1 → ( alldisjointp(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf), gstepf(gs, ls, L2, a).gspmx) ∧ gstepf(gs, ls, L2, a).y + (U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∪ gstepf(gs, ls, L2, a).gspmx ).toMatrix (gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x ) * gstepf(gs, ls, L2, a).x = gstepf(gs, ls, L2, a).spmx.toMatrix(gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x) * gstepf(gs, ls, L2, a).x ∧ U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∪ gstepf(gs, ls, L2, a).gspmx ⊆ gstepf(gs, ls, L2, a).spmx ∧ # gstepf(gs, ls, L2, a).y = gstepf(gs, ls, L2, a).r ∧ okspmx(gstepf(gs, ls, L2, a).spmx, gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x)) ∧ gstepf(gs, ls, L2, a).ghostlspmxf(lstepf(gs, ls, L2, a).tid) = ∅ | A Proof Obligation |
| rely-L2-L1 | ⊦ ls.tid ≠ tid0 ∧ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L2, a) ∧ pcstepf(gs, ls, L2, a) = L1 → gs.ghostlspmxf(tid0) = gstepf(gs, ls, L2, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L2, a).gspmx ⊆ gs.gspmx | A Proof Obligation |
| stable-L0 | ⊦ true | A Proof Obligation |
| stable-L3 | ⊦ ( ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ alldisjointp(alltids, gs0.ghostlspmxf) ∧ disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx) ∧ gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x ∧ U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx ∧ # gs0.y = gs0.r ∧ okspmx(gs0.spmx, gs0.r, # gs0.x)) ∧ gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid) ∧ gs0.gspmx ⊆ gs.gspmx → gs0.ghostlspmxf(ls.tid) = ls.lspmx | A Proof Obligation |
| stable-L5 | ⊦ ( ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ ls.np ∈ ls.lspmx ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ alldisjointp(alltids, gs0.ghostlspmxf) ∧ disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx) ∧ gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x ∧ U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx ∧ # gs0.y = gs0.r ∧ okspmx(gs0.spmx, gs0.r, # gs0.x)) ∧ gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid) ∧ gs0.gspmx ⊆ gs.gspmx → ls.np ∈ ls.lspmx ∧ gs0.ghostlspmxf(ls.tid) = ls.lspmx | A Proof Obligation |
| stable-L7-01 | ⊦ ( ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ ls.np ∈ ls.lspmx ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx -- ls.np) ∧ alldisjointp(alltids, gs0.ghostlspmxf) ∧ disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx) ∧ gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x ∧ U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx ∧ # gs0.y = gs0.r ∧ okspmx(gs0.spmx, gs0.r, # gs0.x)) ∧ gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid) ∧ gs0.gspmx ⊆ gs.gspmx → ls.np ∈ ls.lspmx ∧ gs0.ghostlspmxf(ls.tid) = ls.lspmx -- ls.np | A Proof Obligation |
| stable-L8 | ⊦ ( ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.gspmx = ∅ ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ alldisjointp(alltids, gs0.ghostlspmxf) ∧ disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx) ∧ gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x ∧ U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx ∧ # gs0.y = gs0.r ∧ okspmx(gs0.spmx, gs0.r, # gs0.x)) ∧ gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid) ∧ gs0.gspmx ⊆ gs.gspmx → gs0.gspmx = ∅ ∧ gs0.ghostlspmxf(ls.tid) = ∅ | A Proof Obligation |
| rely-reflexive | alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), gspmx) ∧ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ gspmx ⊆ spmx ∧ # y = r ∧ okspmx(spmx, r, # x) ⊦ ghostlspmxf(tid) = ghostlspmxf(tid) ∧ gspmx ⊆ gspmx | A Proof Obligation |
| stable-L4 | ⊦ ( ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ ls.lspmx ≠ ∅ ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ alldisjointp(alltids, gs0.ghostlspmxf) ∧ disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx) ∧ gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x ∧ U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx ∧ # gs0.y = gs0.r ∧ okspmx(gs0.spmx, gs0.r, # gs0.x)) ∧ gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid) ∧ gs0.gspmx ⊆ gs.gspmx → ls.lspmx ≠ ∅ ∧ gs0.ghostlspmxf(ls.tid) = ls.lspmx | A Proof Obligation |
| stable-L1 | ⊦ ( ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ alldisjointp(alltids, gs0.ghostlspmxf) ∧ disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx) ∧ gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x ∧ U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx ∧ # gs0.y = gs0.r ∧ okspmx(gs0.spmx, gs0.r, # gs0.x)) ∧ gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid) ∧ gs0.gspmx ⊆ gs.gspmx → gs0.ghostlspmxf(ls.tid) = ∅ | A Proof Obligation |
| step-L7-L3 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ ls.np ∈ ls.lspmx ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx -- ls.np) ∧ pre(gs, ls, L7, a) ∧ pcstepf(gs, ls, L7, a) = L3 → ( alldisjointp(alltids, gstepf(gs, ls, L7, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L7, a).ghostlspmxf), gstepf(gs, ls, L7, a).gspmx) ∧ gstepf(gs, ls, L7, a).y + (U(alltids, gstepf(gs, ls, L7, a).ghostlspmxf) ∪ gstepf(gs, ls, L7, a).gspmx ).toMatrix (gstepf(gs, ls, L7, a).r, # gstepf(gs, ls, L7, a).x ) * gstepf(gs, ls, L7, a).x = gstepf(gs, ls, L7, a).spmx.toMatrix(gstepf(gs, ls, L7, a).r, # gstepf(gs, ls, L7, a).x) * gstepf(gs, ls, L7, a).x ∧ U(alltids, gstepf(gs, ls, L7, a).ghostlspmxf) ∪ gstepf(gs, ls, L7, a).gspmx ⊆ gstepf(gs, ls, L7, a).spmx ∧ # gstepf(gs, ls, L7, a).y = gstepf(gs, ls, L7, a).r ∧ okspmx(gstepf(gs, ls, L7, a).spmx, gstepf(gs, ls, L7, a).r, # gstepf(gs, ls, L7, a).x)) ∧ gstepf(gs, ls, L7, a).ghostlspmxf(lstepf(gs, ls, L7, a).tid) = lstepf(gs, ls, L7, a).lspmx | A Proof Obligation |
| rely-L6-L3 | ⊦ ls.tid ≠ tid0 ∧ ( ls.np ∈ ls.lspmx ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L6, a) ∧ pcstepf(gs, ls, L6, a) = L3 → gs.ghostlspmxf(tid0) = gstepf(gs, ls, L6, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L6, a).gspmx ⊆ gs.gspmx | A Proof Obligation |
| rely-L6-L7 | ⊦ ls.tid ≠ tid0 ∧ ( ls.np ∈ ls.lspmx ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L6, a) ∧ pcstepf(gs, ls, L6, a) = L7 → gs.ghostlspmxf(tid0) = gstepf(gs, ls, L6, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L6, a).gspmx ⊆ gs.gspmx | A Proof Obligation |
| step-L6-L7 | ⊦ ( ls.np ∈ ls.lspmx ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L6, a) ∧ pcstepf(gs, ls, L6, a) = L7 → ( alldisjointp(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf), gstepf(gs, ls, L6, a).gspmx) ∧ gstepf(gs, ls, L6, a).y + (U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∪ gstepf(gs, ls, L6, a).gspmx ).toMatrix (gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x ) * gstepf(gs, ls, L6, a).x = gstepf(gs, ls, L6, a).spmx.toMatrix(gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x) * gstepf(gs, ls, L6, a).x ∧ U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∪ gstepf(gs, ls, L6, a).gspmx ⊆ gstepf(gs, ls, L6, a).spmx ∧ # gstepf(gs, ls, L6, a).y = gstepf(gs, ls, L6, a).r ∧ okspmx(gstepf(gs, ls, L6, a).spmx, gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x)) ∧ lstepf(gs, ls, L6, a).np ∈ lstepf(gs, ls, L6, a).lspmx ∧ gstepf(gs, ls, L6, a).ghostlspmxf(lstepf(gs, ls, L6, a).tid) = lstepf(gs, ls, L6, a).lspmx -- lstepf(gs, ls, L6, a).np | A Proof Obligation |
| step-L1-L8 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L1, a) ∧ pcstepf(gs, ls, L1, a) = L8 → ( alldisjointp(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf), gstepf(gs, ls, L1, a).gspmx) ∧ gstepf(gs, ls, L1, a).y + (U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∪ gstepf(gs, ls, L1, a).gspmx ).toMatrix (gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x ) * gstepf(gs, ls, L1, a).x = gstepf(gs, ls, L1, a).spmx.toMatrix(gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x) * gstepf(gs, ls, L1, a).x ∧ U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∪ gstepf(gs, ls, L1, a).gspmx ⊆ gstepf(gs, ls, L1, a).spmx ∧ # gstepf(gs, ls, L1, a).y = gstepf(gs, ls, L1, a).r ∧ okspmx(gstepf(gs, ls, L1, a).spmx, gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x)) ∧ gstepf(gs, ls, L1, a).gspmx = ∅ ∧ gstepf(gs, ls, L1, a).ghostlspmxf(lstepf(gs, ls, L1, a).tid) = ∅ | A Proof Obligation |
| rely-L5-L6 | ⊦ ls.tid ≠ tid0 ∧ ( ls.np ∈ ls.lspmx ∧ ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx) ∧ pre(gs, ls, L5, a) ∧ pcstepf(gs, ls, L5, a) = L6 → gs.ghostlspmxf(tid0) = gstepf(gs, ls, L5, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L5, a).gspmx ⊆ gs.gspmx | A User Theorem |
| step-L1-L7 | ⊦ ( ( alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x)) ∧ gs.ghostlspmxf(ls.tid) = ∅) ∧ pre(gs, ls, L1, a) ∧ pcstepf(gs, ls, L1, a) = L7 → ( alldisjointp(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf), gstepf(gs, ls, L1, a).gspmx) ∧ gstepf(gs, ls, L1, a).y + (U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∪ gstepf(gs, ls, L1, a).gspmx ).toMatrix (gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x ) * gstepf(gs, ls, L1, a).x = gstepf(gs, ls, L1, a).spmx.toMatrix(gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x) * gstepf(gs, ls, L1, a).x ∧ U(alltids, gstepf(gs, ls, L1, a).ghostlspmxf) ∪ gstepf(gs, ls, L1, a).gspmx ⊆ gstepf(gs, ls, L1, a).spmx ∧ # gstepf(gs, ls, L1, a).y = gstepf(gs, ls, L1, a).r ∧ okspmx(gstepf(gs, ls, L1, a).spmx, gstepf(gs, ls, L1, a).r, # gstepf(gs, ls, L1, a).x)) ∧ gstepf(gs, ls, L1, a).gspmx = ∅ ∧ gstepf(gs, ls, L1, a).ghostlspmxf(lstepf(gs, ls, L1, a).tid) = ∅ | A User Theorem |