Proof step 1 from proof abs-init (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITPSCInv(gs, lsf, pcf), flitpscInit(mkstate(gs, lsf, pcf)) ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf))

Rule argument

Additional information

Proof step 2 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  FLITPSCInv(gs, lsf, pcf), flitpscInit(mkstate(gs, lsf, pcf)) ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: abs-def: ⊦ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ↔ gabs(gs, lsf, pcf, ags, alsf, apcf) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t))); gabs-def: ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p);

Proof step 3 from proof abs-init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ flitpscInit(mkstate(gs, lsf, pcf)) ↔ (gs.mem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ gs.p = (λ l. []) ∧ gs.ctr = (λ l. 0) ∧ gs.readers = (λ l. ∅) ∧ gs.writers = (λ l. ∅)) ∧ (∀ t. lsf(t).t = t)

• Proof step 5:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), pcf = (λ tid. idle), FLITPSCInv(gs, lsf, pcf), ∀ t. lsf(t).t = t ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)))

Rule argument

Additional information

Used terms: gs, lsf, pcf

Proof step 4 from proof abs-init (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), FLITPSCInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ ags.pm = (λ l. O) ∧ ags.vm = (λ l. O) ⊕ (λ l. []) ∧ abs(ags.h, λ l. ∅, λ l. []) ∧ (∀ t. labs(gs, lsf(t), idle, ags, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 6 from proof abs-init (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  ctr = (λ l. 0), gs = mkFLITPSCgs(mem, p, ctr, writers, writers0), mem = (λ l. O), p = (λ l. []), writers = (λ l. ∅), writers0 = (λ l. ∅), FLITPSCInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ ags.pm = (λ l. O) ∧ ags.vm = (λ l. O) ⊕ (λ l. []) ∧ abs(ags.h, λ l. ∅, λ l. []) ∧ (∀ t. labs(gs, lsf(t), idle, ags, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers); (elim) Used terms: gs, mem, ctr, writers, writers0, p

Proof step 7 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ ags.pm = (λ l. O) ∧ ags.vm = (λ l. O) ⊕ (λ l. []) ∧ abs(ags.h, λ l. ∅, λ l. []) ∧ (∀ t. labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, ags, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 8 from proof abs-init (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ plibInit(mkstate(mkPLIBgs(∅, ∅, []), λ t. mkPLIBls(t, l, v0, v1), λ t. idle)) ∧ mkPLIBgs(∅, ∅, []).pm = (λ l. O) ∧ mkPLIBgs(∅, ∅, []).vm = (λ l. O) ⊕ (λ l. []) ∧ abs(mkPLIBgs(∅, ∅, []).h, λ l. ∅, λ l. []) ∧ (∀ t. labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle))

Rule argument

Additional information

Used terms: mkPLIBgs(∅, ∅, []), λ t. mkPLIBls(t, l, v0, v1), λ t. idle

Proof step 9 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ plibInit(mkstate(mkPLIBgs(∅, ∅, []), λ t. mkPLIBls(t, l, v0, v1), λ t. idle)) ∧ ∅ = (λ l. O) ⊕ (λ l. []) ∧ abs([], λ l. ∅, λ l. []) ∧ labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkPLIBgs(vm, vm0, h).vm = vm; (s) ⊦ ∅(l) = O; (s) ⊦ mkPLIBgs(vm, vm0, h).pm = vm0; (s)

Proof step 10 from proof abs-init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ plibInit(mkstate(gs, lsf, pcf)) ↔ (gs.vm = ∅ ∧ gs.pm = ∅ ∧ pcf = (λ t. idle) ∧ gs.h = []) ∧ (∀ t. lsf(t).t = t)

• Proof step 12:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ( (mkPLIBgs(∅, ∅, []).vm = ∅ ∧ mkPLIBgs(∅, ∅, []).pm = ∅ ∧ (λ t. idle) = (λ t. idle) ∧ mkPLIBgs(∅, ∅, []).h = []) ∧ (∀ t. mkPLIBls(t, l, v0, v1).t = t)) ∧ ∅ = (λ l. O) ⊕ (λ l. []) ∧ abs([], λ l. ∅, λ l. []) ∧ labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle)

Rule argument

Additional information

Used terms: mkPLIBgs(∅, ∅, []), λ t. mkPLIBls(t, l, v0, v1), λ t. idle

Proof step 11 from proof abs-init (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ abs([], λ l. ∅, λ l. []) ∧ labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkPLIBgs(vm, vm0, h).pm = vm0; (s) ⊦ mkPLIBgs(vm, vm0, h).vm = vm; (s)

Proof step 13 from proof abs-init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)))

• Proof step 15:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ (∀ l. absloc(events(([] | l) | false), ∅, [])) ∧ labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle)

Rule argument

Additional information

Used terms: [], λ l. ∅, λ l. []

Proof step 14 from proof abs-init (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ labs(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ [] |W = []; (s) ⊦ absloc([], rset, fowl) ↔ fowl |W = []; (s) ⊦ events([]) = []; (s) ⊦ [] | b = []; (s) ⊦ [] | l = []; (s)

Proof step 16 from proof abs-init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ (pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ (pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ (pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = [])

• Proof step 18:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ lsf(t).t = mkPLIBls(t, l, v0, v1).t ∧ (idle = idle → idle = idle) ∧ (idle = ready → idle = ready) ∧ (idle = crashed → idle = crashed) ∧ (idle = R1 → idle = invRead) ∧ (idle = R2 ∨ idle = R3 ∨ idle = R4 → idle = resRead) ∧ (idle = W1 ∨ idle = W2 ∨ idle = W3 → idle = invWrite) ∧ (idle = W4 ∨ idle = W5 ∨ idle = W6 ∨ idle = W7 → idle = resWrite) ∧ (idle = R1 → lsf(t).l = mkPLIBls(t, l, v0, v1).il) ∧ (idle = R2 ∨ idle = R3 ∨ idle = R4 → lsf(t).v = mkPLIBls(t, l, v0, v1).ov) ∧ ( idle = W1 ∨ idle = W2 ∨ idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 ∨ idle = W7 → lsf(t).l = mkPLIBls(t, l, v0, v1).il ∧ lsf(t).v = mkPLIBls(t, l, v0, v1).iv) ∧ ( idle = idle ∨ idle = ready ∨ idle = R1 ∨ idle = R4 ∨ idle = W1 ∨ idle = W5 → (∀ l. ¬ FO(lsf(t).t) ∈ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).p(l) → ((mkPLIBgs(∅, ∅, []).h | l) | lsf(t).t) | false = [])) ∧ (idle = W2 ∨ idle = W3 ∨ idle = W6 ∨ idle = W7 → (∀ l. ((mkPLIBgs(∅, ∅, []).h | l) | lsf(t).t) | false = [])) ∧ ( idle = R2 ∨ idle = R3 → (∀ l0. l0 ≠ lsf(t).l ∧ ¬ FO(lsf(t).t) ∈ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).p(l0) → ((mkPLIBgs(∅, ∅, []).h | l0) | lsf(t).t) | false = [])) ∧ (idle = R2 → mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).ctr(lsf(t).l) = 0 → ((mkPLIBgs(∅, ∅, []).h | lsf(t).l) | lsf(t).t) | false = []) ∧ ( idle = W4 → ((mkPLIBgs(∅, ∅, []).h | lsf(t).l) | lsf(t).t) | false = (W(lsf(t).t, lsf(t).l, lsf(t).v), false) ' ∨ ((mkPLIBgs(∅, ∅, []).h | lsf(t).l) | lsf(t).t) | false = [])

Rule argument

Additional information

Used terms: lsf(t), mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), idle, mkPLIBgs(∅, ∅, []), mkPLIBls(t, l, v0, v1), idle

Proof step 17 from proof abs-init (previous step) (back to tree)

Lemma labs-def

Proof step 18 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ lsf(t).t = t

Rule argument

Additional information

Used simplifier rules: ⊦ W4 ≠ idle; (s) ⊦ R2 ≠ idle; (s) ⊦ R3 ≠ idle; (s) ⊦ W7 ≠ idle; (s) ⊦ W6 ≠ idle; (s) ⊦ W3 ≠ idle; (s) ⊦ W2 ≠ idle; (s) ⊦ [] | b = []; (s) ⊦ [] | t = []; (s) ⊦ [] | l = []; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ ¬ a ∈ []; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s) ⊦ W5 ≠ idle; (s) ⊦ W1 ≠ idle; (s) ⊦ R4 ≠ idle; (s) ⊦ R1 ≠ idle; (s) ⊦ crashed ≠ idle; (s) ⊦ idle ≠ ready; (s) ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s)

Proof step 19 from proof abs-init (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  lsf(t) = mkFLITPSCls(t0, l0, v), FLITPSCInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ t0 = t

Rule argument

Additional information

Used simplifier rules: ⊦ (t = ls.t ∧ l = ls.l) ∧ v = ls.v ↔ ls = mkFLITPSCls(t, l, v); (elim) Used terms: lsf(t), t0, l0, v

Proof step 20 from proof abs-init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

• Proof step 22:

  lsf(t) = mkFLITPSCls(t0, l0, v), FLITPSCGInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), ∀ t. lsf(t).t = t, ∀ t. lsf(t).t = t ∧ FLITPSCLInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle) ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ t0 = t

Rule argument

Additional information

Used terms: mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ tid. idle

Proof step 21 from proof abs-init (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof abs-init (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  lsf(t).t = t, lsf(t) = mkFLITPSCls(t0, l0, v), FLITPSCGInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCLInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), idle), ∀ t. lsf(t).t = t ⊦ ∅ = (λ l. O) ⊕ (λ l. []) ∧ t0 = t

Rule argument

Additional information

Used terms: t

Proof step 23 from proof abs-init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  lsf(t0) = mkFLITPSCls(t0, l0, v), ∅ ≠ (λ l. O) ⊕ (λ l. []), FLITPSCGInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCLInv(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t0, l0, v), idle), ∀ t. lsf(t).t = t ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCls(t, l, v).t = t; (s)

Proof step 24 from proof abs-init (previous step) (back to tree)

User applied rule expand left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ∅(l) = O; (s) ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s) ⊦ v ⊕ [] = v; (s)