Proof step 1 from proof step-absstep-I12-I13-tau-other (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ls0.n0 = get_hash(ls0.e, ls0.sz), ls.n0 = get_hash(ls.e, ls.sz), ls0.sz = # gs0.ar, ls.sz = # gs.ar, lsf(tid0).tid = alsf(tid0).tid, ls.tid = als.tid, lsf(tid0).tid = tid0, lsf(tid).tid = tid, alsf(tid).tid = tid, I13 = pcstepf(gs, ls, I12, τ), gs0.ar[ls0.n] = ls0.e0, alsf(tid) = als, apc = invInsert, apcf(tid) = apc, gs0 = gstepf(gs, ls, I12, τ), ls0 = lstepf(gs, ls, I12, τ), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = I12, pcf0(tid) = I13, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls.e ≠ ⊥, ls0.e ≠ ⊥, gs.ar[ls.n] ≠ ⊥, gs.ar[ls.n] ≠ ls.e, gs0.ar[ls0.n] ≠ ⊥, tid ≠ tid0, ls0.n < # gs0.ar, ls0.n0 < # gs0.ar, ls.n < # gs.ar, ls.n0 < # gs.ar, HashsetLInv(gs0, lsf(tid0), pcf(tid0)), HashsetLInv(gs, lsf(tid0), pcf(tid0)), SetLInv(ags, alsf(tid0), apcf(tid0)), SetLInv(ags, als, apc), absset(gs.ar, ags.set), allslotsfull(gs0.ar, ls0.n0, ls0.n, ls0.e, false), allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs0.ar), htok(gs.ar), pre(gs, ls, I12, τ), ¬ ls.b, ¬ ls0.b, pcf(tid0) = idle → apcf(tid0) = idle, pcf(tid0) = I1 ∨ pcf(tid0) = I2 ∨ pcf(tid0) = I3 ∨ pcf(tid0) = I4 ∨ pcf(tid0) = I6 ∨ pcf(tid0) = I10 ∨ pcf(tid0) = I11 ∨ pcf(tid0) = I12 ∨ pcf(tid0) = I16 ∨ pcf(tid0) = I17 ∨ pcf(tid0) = I18 ∨ pcf(tid0) = I20 → apcf(tid0) = invInsert, pcf(tid0) = I5 → apcf(tid0) = (lsf(tid0).b ⊃ retInsert;invInsert), pcf(tid0) = I7 ∨ pcf(tid0) = I13 → apcf(tid0) = (lsf(tid0).e = lsf(tid0).e0 ⊃ retInsert;invInsert), pcf(tid0) = I8 → apcf(tid0) = retInsert, pcf(tid0) = I9 ∨ pcf(tid0) = I14 ∨ pcf(tid0) = I15 ∨ pcf(tid0) = I19 ∨ pcf(tid0) = I21 → apcf(tid0) = retInsert, pcf(tid0) = I7 ∨ pcf(tid0) = I8 ∨ pcf(tid0) = I13 ∨ pcf(tid0) = I14 → lsf(tid0).e = lsf(tid0).e0 → alsf(tid0).lb, pcf(tid0) = I9 ∨ pcf(tid0) = I15 ∨ pcf(tid0) = I19 → (alsf(tid0).lb ↔ lsf(tid0).b), pcf(tid0) = I5 → lsf(tid0).b → ¬ alsf(tid0).lb, pcf(tid0) = I21 → ¬ alsf(tid0).lb, pcf(tid0) = M1 ∨ pcf(tid0) = M2 ∨ pcf(tid0) = M3 ∨ pcf(tid0) = M4 ∨ pcf(tid0) = M5 ∨ pcf(tid0) = M6 ∨ pcf(tid0) = M17 → apcf(tid0) = invMember, pcf(tid0) = M7 → apcf(tid0) = (lsf(tid0).e0 ≠ lsf(tid0).e ∧ lsf(tid0).e0 ≠ ⊥ ∧ (lsf(tid0).n + 1) % # gs.ar ≠ lsf(tid0).n0 ⊃ invMember;retMember), pcf(tid0) = M10 → apcf(tid0) = (lsf(tid0).e0 ≠ ⊥ ∧ (lsf(tid0).n + 1) % # gs.ar ≠ lsf(tid0).n0 ⊃ invMember;retMember), pcf(tid0) = M13 → apcf(tid0) = ((lsf(tid0).n + 1) % # gs.ar ≠ lsf(tid0).n0 ⊃ invMember;retMember), pcf(tid0) = M14 → apcf(tid0) = (lsf(tid0).n ≠ lsf(tid0).n0 ⊃ invMember;retMember), pcf(tid0) = M8 ∨ pcf(tid0) = M9 ∨ pcf(tid0) = M11 ∨ pcf(tid0) = M12 ∨ pcf(tid0) = M15 ∨ pcf(tid0) = M16 → apcf(tid0) = retMember, pcf(tid0) = M7 → lsf(tid0).e0 = lsf(tid0).e ∨ lsf(tid0).e0 = ⊥ ∨ (lsf(tid0).n + 1) % # gs.ar = lsf(tid0).n0 → (lsf(tid0).e = lsf(tid0).e0 ↔ alsf(tid0).lb), pcf(tid0) = M10 → lsf(tid0).e0 = ⊥ ∨ (lsf(tid0).n + 1) % # gs.ar = lsf(tid0).n0 → ¬ alsf(tid0).lb, pcf(tid0) = M13 → (lsf(tid0).n + 1) % # gs.ar = lsf(tid0).n0 → ¬ alsf(tid0).lb, pcf(tid0) = M14 → lsf(tid0).n = lsf(tid0).n0 → ¬ alsf(tid0).lb, pcf(tid0) = M9 ∨ pcf(tid0) = M12 ∨ pcf(tid0) = M16 → (alsf(tid0).lb ↔ lsf(tid0).b), pcf(tid0) = M11 ∨ pcf(tid0) = M15 → ¬ alsf(tid0).lb, pcf(tid0) = M8 → alsf(tid0).lb, apcf(tid0) = invMember ∨ apcf(tid0) = invInsert → lsf(tid0).e = alsf(tid0).le, apc = invMember ∨ apc = invInsert → ls.e = als.le, ∀ tid1. tid1 ≠ tid ∧ tid1 ≠ tid0 → HashsetLInv(gs, lsf(tid1), pcf(tid1)) ∧ SetLInv(ags, alsf(tid1), apcf(tid1)) ∧ labs(gs, lsf(tid1), pcf(tid1), ags, alsf(tid1), apcf(tid1)), ∀ tid0. tid0 ≠ tid → alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0 ⊦ lsf(tid0).tid = alsf(tid0).tid ∧ (pcf(tid0) = idle → apcf(tid0) = idle) ∧ ( pcf(tid0) = I1 ∨ pcf(tid0) = I2 ∨ pcf(tid0) = I3 ∨ pcf(tid0) = I4 ∨ pcf(tid0) = I6 ∨ pcf(tid0) = I10 ∨ pcf(tid0) = I11 ∨ pcf(tid0) = I12 ∨ pcf(tid0) = I16 ∨ pcf(tid0) = I17 ∨ pcf(tid0) = I18 ∨ pcf(tid0) = I20 → apcf(tid0) = invInsert) ∧ (pcf(tid0) = I5 → apcf(tid0) = (lsf(tid0).b ⊃ retInsert;invInsert)) ∧ (pcf(tid0) = I7 ∨ pcf(tid0) = I13 → apcf(tid0) = (lsf(tid0).e = lsf(tid0).e0 ⊃ retInsert;invInsert)) ∧ (pcf(tid0) = I8 → apcf(tid0) = retInsert) ∧ (pcf(tid0) = I9 ∨ pcf(tid0) = I14 ∨ pcf(tid0) = I15 ∨ pcf(tid0) = I19 ∨ pcf(tid0) = I21 → apcf(tid0) = retInsert) ∧ (pcf(tid0) = I7 ∨ pcf(tid0) = I8 ∨ pcf(tid0) = I13 ∨ pcf(tid0) = I14 → lsf(tid0).e = lsf(tid0).e0 → alsf(tid0).lb) ∧ (pcf(tid0) = I9 ∨ pcf(tid0) = I15 ∨ pcf(tid0) = I19 → (alsf(tid0).lb ↔ lsf(tid0).b)) ∧ (pcf(tid0) = I5 → lsf(tid0).b → ¬ alsf(tid0).lb) ∧ (pcf(tid0) = I21 → ¬ alsf(tid0).lb) ∧ (pcf(tid0) = M1 ∨ pcf(tid0) = M2 ∨ pcf(tid0) = M3 ∨ pcf(tid0) = M4 ∨ pcf(tid0) = M5 ∨ pcf(tid0) = M6 ∨ pcf(tid0) = M17 → apcf(tid0) = invMember) ∧ ( pcf(tid0) = M7 → apcf(tid0) = (lsf(tid0).e0 ≠ lsf(tid0).e ∧ lsf(tid0).e0 ≠ ⊥ ∧ (lsf(tid0).n + 1) % # gs0.ar ≠ lsf(tid0).n0 ⊃ invMember;retMember)) ∧ (pcf(tid0) = M10 → apcf(tid0) = (lsf(tid0).e0 ≠ ⊥ ∧ (lsf(tid0).n + 1) % # gs0.ar ≠ lsf(tid0).n0 ⊃ invMember;retMember)) ∧ (pcf(tid0) = M13 → apcf(tid0) = ((lsf(tid0).n + 1) % # gs0.ar ≠ lsf(tid0).n0 ⊃ invMember;retMember)) ∧ (pcf(tid0) = M14 → apcf(tid0) = (lsf(tid0).n ≠ lsf(tid0).n0 ⊃ invMember;retMember)) ∧ (pcf(tid0) = M8 ∨ pcf(tid0) = M9 ∨ pcf(tid0) = M11 ∨ pcf(tid0) = M12 ∨ pcf(tid0) = M15 ∨ pcf(tid0) = M16 → apcf(tid0) = retMember) ∧ ( pcf(tid0) = M7 → lsf(tid0).e0 = lsf(tid0).e ∨ lsf(tid0).e0 = ⊥ ∨ (lsf(tid0).n + 1) % # gs0.ar = lsf(tid0).n0 → (lsf(tid0).e = lsf(tid0).e0 ↔ alsf(tid0).lb)) ∧ (pcf(tid0) = M10 → lsf(tid0).e0 = ⊥ ∨ (lsf(tid0).n + 1) % # gs0.ar = lsf(tid0).n0 → ¬ alsf(tid0).lb) ∧ (pcf(tid0) = M13 → (lsf(tid0).n + 1) % # gs0.ar = lsf(tid0).n0 → ¬ alsf(tid0).lb) ∧ (pcf(tid0) = M14 → lsf(tid0).n = lsf(tid0).n0 → ¬ alsf(tid0).lb) ∧ (pcf(tid0) = M9 ∨ pcf(tid0) = M12 ∨ pcf(tid0) = M16 → (alsf(tid0).lb ↔ lsf(tid0).b)) ∧ (pcf(tid0) = M11 ∨ pcf(tid0) = M15 → ¬ alsf(tid0).lb) ∧ (pcf(tid0) = M8 → alsf(tid0).lb) ∧ (apcf(tid0) = invMember ∨ apcf(tid0) = invInsert → lsf(tid0).e = alsf(tid0).le)

Rule argument

Additional information

Proof step 2 from proof step-absstep-I12-I13-tau-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ gstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs); (s) ⊦ pre(gs, ls, I12, a) ↔ a = (gs.ar[ls.n] = ⊥ ∨ gs.ar[ls.n] = ls.e ⊃ doINSERT(ls.tid, true);τ); (s) ⊦ m < n → n ≠ 0; (s) ⊦ pcstepf(gs, ls, I12, a) = I13; (s) ⊦ lstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]); (s)