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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITInv(gs, lsf, pcf), flitInit(mkstate(gs, lsf, pcf)) ⊦ ∃ ags, alsf, apcf. flitpscInit(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:

  FLITInv(gs, lsf, pcf), flitInit(mkstate(gs, lsf, pcf)) ⊦ ∃ ags, alsf, apcf. flitpscInit(mkstate(ags, alsf, apcf)) ∧ ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters ∧ (∀ 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.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters;

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:

  ⊦ flitInit(mkstate(gs, lsf, pcf)) ↔ ( gs.pmem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ gs.pq = (λ l. []) ∧ gs.fctr = (λ l. 0) ∧ gs.freaders = (λ l. ∅) ∧ gs.fwriters = (λ l. ∅) ∧ gs.bq = (λ t. []) ∧ gs.rfo = (λ t. [])) ∧ (∀ t. lsf(t).t = t)

• Proof step 5:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), pcf = (λ tid. idle), FLITInv(gs, lsf, pcf), ∀ t. lsf(t).t = t ⊦ ∃ ags, alsf, apcf. flitpscInit(mkstate(ags, alsf, apcf)) ∧ ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters ∧ (∀ 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.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ∃ ags, alsf, apcf. flitpscInit(mkstate(ags, alsf, apcf)) ∧ ags.mem = (λ l. O) ∧ ags.ctr = (λ l. 0) ∧ reorder(ags.p, λ l. [], λ t. []) ∧ ags.writers = (λ 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)

User applied rule exists right

And obtained the following new goals

• Proof step 7:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ flitpscInit(mkstate(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), λ t. mkFLITPSCls(t, l, O), λ t. idle)) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).mem = (λ l. O) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).ctr = (λ l. 0) ∧ reorder(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).p, λ l. [], λ t. []) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).writers = (λ l. ∅) ∧ (∀ t. labs(gs, lsf(t), idle, mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t, l, O), idle))

Rule argument

Additional information

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

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:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ flitpscInit(mkstate(mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), λ t. mkFLITPSCls(t, l, O), λ t. idle)) ∧ reorder(λ l. [], λ l. [], λ t. []) ∧ labs(gs, lsf(t), idle, mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t, l, O), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem = mem; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ 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 10:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ ( ( mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).mem = (λ l. O) ∧ (λ t. idle) = (λ tid. idle) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).p = (λ l. []) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).ctr = (λ l. 0) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).readers = (λ l. ∅) ∧ mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅).writers = (λ l. ∅)) ∧ (∀ t. mkFLITPSCls(t, l, O).t = t)) ∧ reorder(λ l. [], λ l. [], λ t. []) ∧ labs(gs, lsf(t), idle, mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t, l, O), idle)

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ reorder(λ l. [], λ l. [], λ t. []) ∧ labs(gs, lsf(t), idle, mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t, l, O), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem = mem; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ reorder(p, pq, rfo) ↔ (∀ l. reorder(l, p(l), pq(l), rfo))

• Proof step 13:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦ (∀ l. reorder(l, [], [], λ t. [])) ∧ labs(gs, lsf(t), idle, mkFLITPSCgs(λ l. O, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t, l, O), idle)

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  gs.bq = (λ t. []), gs.fctr = (λ l. 0), gs.freaders = (λ l. ∅), gs.fwriters = (λ l. ∅), gs.pmem = (λ l. O), gs.pq = (λ l. []), gs.rfo = (λ t. []), lsf(t).t ≠ t, FLITInv(gs, lsf, λ tid. idle), ∀ t. lsf(t).t = t ⊦

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ 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 = R1) ∧ (pc = R2 → apc = R2) ∧ (pc = R3 → apc = R3) ∧ (pc = R4 → apc = R4) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.loc = als.l) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.val = als.v) ∧ (pc = W1 → apc = W1) ∧ (pc = W2 → apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2)) ∧ (pc = W3 → apc = W3) ∧ (pc = W4 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4)) ∧ ( pc = W5 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5))) ∧ ( pc = W6 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3 ;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6)) )) ∧ (pc = W7 → apc = W7) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.loc = als.l) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.val = als.v); ⊦ W7 ≠ idle; (s) ⊦ W6 ≠ idle; (s) ⊦ W5 ≠ idle; (s) ⊦ W4 ≠ idle; (s) ⊦ W3 ≠ idle; (s) ⊦ W2 ≠ idle; (s) ⊦ W1 ≠ idle; (s) ⊦ R4 ≠ idle; (s) ⊦ R3 ≠ idle; (s) ⊦ R2 ≠ idle; (s) ⊦ R1 ≠ idle; (s) ⊦ crashed ≠ idle; (s) ⊦ idle ≠ ready; (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ propFOs(t, l, []) = []; (s) ⊦ reorder(l, [], fowl0, rfo) ↔ fowl0 = [] ∧ (∀ t. propFOs(t, l, rfo(t)) = []); (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t