[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 178 from proof inv-commit-rec-ind (previous step)

zh[r0] = mkznode(r2, zbrar0, false, true, n), zh1[r0] = mkznode(r1, zbrar, false, true, m0), adr0 = adr3, pstate = index(m1), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, as1 ∩ as0 = ∅, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh), btree-sub-clean(r0, n, zh), inv(istore), inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore0), refsize-cons(istore, as0 ∪ as1), refsize-cons(istore2, as0 ∪ as), r0 ∈ zh, r0 ∈ zh1, m ∈ istore2, m1 ∈ istore, m ∈ istore, as1 ⊆ dom nodes(istore2), as1 ∩ dom nodes(istore2) ⊆ as, as ⊆ dom nodes(istore2), as ⊆ alladrs, alladrs ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore2), as1 ∩ dom nodes(istore2) ⊆ alladrs, as1 ⊆ dom nodes(istore), as1 ⊆ alladrs, istore2 ⊑ istore, istore0 ⊑ istore2, istore0 ⊑ istore, ¬ dups(nx), ¬ adr3 ∈ as1, ¬ adr3 ∈ as, height = 0 → as = ∅, height = 0 → as1 = ∅, ∀ height0, zh, r0, r, zbrar, boolvar, m0, adr0, adr1, istore1, istore, pstate, m, istore0, gstore0, nx, ginval, as, as0, gstore, rp, dirty, ri, alladrs, P, adr, ino, ns, err, bv. height0 < height → zh[r0] = mkznode(r, zbrar, boolvar, true, m0) ∧ adr0 = adr1 ∧ istore1 = istore ∧ pstate = index(m) ∧ remove-refsize0(istore0) = istore0 ∧ remove-refsize0(gstore0) = gstore0 ∧ elems nx ∩ ginval = ∅ ∧ as ∩ as0 = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ ((btree(rp, r0, adr1, height0, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh) ∧ inv(istore0) ∧ inv(istore) ∧ inv(gstore0) ∧ inv(gstore \ ginval) ∧ refsize-cons(istore, as0 ∪ as) ∧ m ∈ istore ∧ r0 ∈ zh ∧ as0 ⊆ dom nodes(istore) ∧ alladrs ⊆ dom nodes(istore) ∧ as ⊆ alladrs ∧ as ⊆ dom nodes(istore) ∧ istore0 ⊑ istore ∧ ¬ dups(nx) ∧ ¬ adr1 ∈ as ∧ (height0 = 0 → as = ∅) → ⟪btree_commit_rec#(r0, adr, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → bv) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr1;adr0), height0, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))) ⊦ ⟪btree_io_save#(r0, adr1, istore0, ginval1, gstore2, gstore1, nx, maxino, ginval; adr0, zh, istore, pstate, syn; err)⟫ ( istore2 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore2) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr0;adr3), height, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh)))

User applied rule insert program lemma

And obtained the following new goals

Proof step 179:
adr0 = adr1, r ∈ zh, zh[r].dirty, btree-sub-clean(r, zh[r].usedsize, zh), ((btree(rp, r, adr0, height, dirty, ri, nodes(istore), as, alladrs, ok) * P))(zh), as0 ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), refsize-cons(istore, as0 ∪ as), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), pstate.index?, istore1 = istore ⊦ ⟪btree_io_save#(r, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0; adr1, zh, istore, pstate, syn; err)⟫ ( refsize-cons(istore, as0 ∪ (err = ESUCCESS ⊃ as ++ adr1;as)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn) ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ adr1 ∈ as) ∧ (∃ as0, alladrs0. as0 = (err = ESUCCESS ⊃ as ++ adr1;as) ∧ alladrs0 = (err = ESUCCESS ⊃ (alladrs -- adr0) ++ adr1;alladrs) ∧ dom nodes(istore) = dom nodes(istore1) ∪ (err = ESUCCESS ⊃ {adr1} ;∅) ∧ (err = ESUCCESS → ¬ adr1 ∈ istore1) ∧ ((btree(rp, r, (err = ESUCCESS ⊃ adr1;adr0), height, err ≠ ESUCCESS, ri, nodes(istore), as0, alladrs0, ok) * P))(zh)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty))
Proof step 180:
dirty0 ↔ dirty, P0 = P, zh1[r0] = mkznode(r1, zbrar, false, true, m0), zh[r0] = mkznode(r2, zbrar0, false, true, n), adr0 = adr3, adr0 = adr0, adr2 = adr0, adr4 = adr1, alladrs0 = alladrs, as2 = as1, as3 = as0, ginval2 = ginval1, ginval3 = ginval, gstore3 = gstore2, gstore4 = gstore1, height0 = height, istore = istore, istore3 = istore0, istore4 = istore, maxino0 = maxino, nx0 = nx, pstate = index(m1), r3 = r0, remove-refsize0(istore0) = istore0, remove-refsize0(gstore1) = gstore1, ri0 = ri, rp0 = rp, elems nx ∩ ginval1 = ∅, as ∩ as0 = ∅, as1 ∩ as0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh), ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), ((btree(rp, r0, adr0, height, dirty, ri, nodes(istore), as1, alladrs, ok) * P))(zh), zh[r0].dirty, pstate.index?, btree-sub-clean(r0, n, zh), btree-sub-clean(r0, zh[r0].usedsize, zh), inv(istore0), inv(istore2), inv(gstore1), inv(gstore2 \ ginval1), inv(istore), inv-index(istore, istore0), inv-journal(nx, gstore2, gstore1, ginval1), inv-state(pstate, nx, gstore2, istore, syn), refsize-cons(istore2, as0 ∪ as), refsize-cons(istore, as0 ∪ as1), m ∈ istore, m1 ∈ istore, m ∈ istore2, r0 ∈ zh1, r0 ∈ zh, as1 ⊆ alladrs, as1 ⊆ dom nodes(istore), as1 ∩ dom nodes(istore2) ⊆ alladrs, as0 ⊆ dom nodes(istore2), alladrs ⊆ dom nodes(istore2), as ⊆ alladrs, as ⊆ dom nodes(istore2), as1 ∩ dom nodes(istore2) ⊆ as, as1 ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), istore0 ⊑ istore, istore0 ⊑ istore2, istore2 ⊑ istore, height = 0 → as1 = ∅, height = 0 → as = ∅, ∀ height0, zh, r0, r, zbrar, boolvar, m0, adr0, adr1, istore1, istore, pstate, m, istore0, gstore0, nx, ginval, as, as0, gstore, rp, dirty, ri, alladrs, P, adr, ino, ns, err, bv. height0 < height → zh[r0] = mkznode(r, zbrar, boolvar, true, m0) ∧ adr0 = adr1 ∧ istore1 = istore ∧ pstate = index(m) ∧ remove-refsize0(istore0) = istore0 ∧ remove-refsize0(gstore0) = gstore0 ∧ elems nx ∩ ginval = ∅ ∧ as ∩ as0 = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ ((btree(rp, r0, adr1, height0, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh) ∧ inv(istore0) ∧ inv(istore) ∧ inv(gstore0) ∧ inv(gstore \ ginval) ∧ refsize-cons(istore, as0 ∪ as) ∧ m ∈ istore ∧ r0 ∈ zh ∧ as0 ⊆ dom nodes(istore) ∧ alladrs ⊆ dom nodes(istore) ∧ as ⊆ alladrs ∧ as ⊆ dom nodes(istore) ∧ istore0 ⊑ istore ∧ ¬ dups(nx) ∧ ¬ adr1 ∈ as ∧ (height0 = 0 → as = ∅) → ⟪btree_commit_rec#(r0, adr, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → bv) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr1;adr0), height0, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))) ⊦ [btree_io_save#(r0, adr1, istore0, ginval1, gstore2, gstore1, nx, maxino, ginval; adr0, zh, istore, pstate, syn; err)] ( refsize-cons(istore, as3 ∪ (err = ESUCCESS ⊃ as2 ++ adr0;as2)) ∧ inv-index(istore, istore3) ∧ inv-state(pstate, nx0, gstore3, istore, syn) ∧ istore4 ⊑ istore ∧ r3 ∈ zh ∧ (err = ESUCCESS → ¬ adr0 ∈ as2) ∧ (∃ as0, alladrs1. as0 = (err = ESUCCESS ⊃ as2 ++ adr0;as2) ∧ alladrs1 = (err = ESUCCESS ⊃ (alladrs0 -- adr2) ++ adr0;alladrs0) ∧ dom nodes(istore) = dom nodes(istore4) ∪ (err = ESUCCESS ⊃ {adr0} ;∅) ∧ (err = ESUCCESS → ¬ adr0 ∈ istore4) ∧ ((btree(rp0, r3, (err = ESUCCESS ⊃ adr0;adr2), height0, err ≠ ESUCCESS, ri0, nodes(istore), as0, alladrs1, ok) * P0))(zh)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r3].dirty) → istore2 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore2) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr0;adr3), height, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))), dups(nx), adr3 ∈ as1, adr3 ∈ as

Rule argument

spec: <toplevel> name: inv-io-save seq: adr0 = adr1, r ∈ zh, zh[r].dirty, btree-sub-clean(r, zh[r].usedsize, zh), (( btree (rp, r, adr0, height, dirty, ri, nodes(istore), as, alladrs, ok) * P) )(zh), as0 ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), refsize-cons(istore, as0 ∪ as), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), pstate.index?, istore1 = istore ⊦ ⟪btree_io_save# (r, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0 ; adr1, zh, istore, pstate, syn ; err)⟫ ( refsize-cons (istore, as0 ∪ (err = ESUCCESS ⊃ as ++ adr1;as)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn) ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ adr1 ∈ as) ∧ (∃ as0, alladrs0. as0 = (err = ESUCCESS ⊃ as ++ adr1;as) ∧ alladrs0 = (err = ESUCCESS ⊃ (alladrs -- adr0) ++ adr1 ;alladrs ) ∧ dom nodes(istore) = dom nodes(istore1) ∪ (err = ESUCCESS ⊃ {adr1} ;∅) ∧ (err = ESUCCESS → ¬ adr1 ∈ istore1) ∧ (( btree (rp, r, (err = ESUCCESS ⊃ adr1;adr0), height, err ≠ ESUCCESS, ri, nodes(istore), as0, alladrs0, ok) * P) )(zh)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty)) subst: [ginval0, maxino, nx, gstore0, gstore, ginval, istore0, adr, r, syn, pstate, istore, zh, adr1, err, rp, height, dirty, ri, as, alladrs, P, as0, adr0, istore1] → [ginval, maxino, nx, gstore1, gstore2, ginval1, istore0, adr1, r0, syn, pstate, istore, zh, adr0, err, rp, height, dirty, ri, as1, alladrs, P, as0, adr0, istore] flags: <all paths>

Additional information

Used simplifier rules: sep-ass: ⊦ (P * P3) * P4 = P * P3 * P4; from specification heap-sep[zheap]%sep-com: ⊦ P * P2 = P2 * P; from specification heap-sep[zheap]%⊦ (( btree (rp, r0, adr, height, dirty0, ri, iast | as0, as, alladrs, nstat) * P) )(zh0) → (( btree (rp, r0, adr, height, dirty0, ri, iast, as, alladrs, nstat) * P) )(zh0); (ss)%⊦ inv-journal(nx, gstore, gstore0, ginval) ↔ inv(gstore \ ginval) ∧ inv(gstore0) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ remove-refsize0(gstore0) = gstore0; (s)%⊦ inv-index(istore, istore0) ↔ inv(istore) ∧ inv(istore0) ∧ istore0 ⊑ istore ∧ remove-refsize0(istore0) = istore0; (s)%⊦ inv-state(pstate, nx, gstore, istore, syn) ↔ ( pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn); (s)% ⊦ ¬ index(m).journal?; (s)% ⊦ index(m).index?; (s)% ⊦ index(m).lnum = m; (s)% ⊦ unbuffered ≠ index(m); (s)% ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).dirty ↔ boolvar0; (s)% ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).usedsize = m; (s)%sub-ntrans-01: ⊦ as ⊆ as0 ∧ ¬ as1 ⊆ as0 → ¬ as1 ⊆ as; (forward) from specification set-basic[node-store]%sub-ntrans: ⊦ as ⊆ as0 ∧ ¬ as ⊆ as1 → ¬ as0 ⊆ as1; (forward) from specification set-basic[node-store]% ⊦ istore ⊑ istore0 → dom nodes(istore) ⊆ dom nodes(istore0); (ss)