| abs-log(nx1, gstore2 ↓) = [], dom gstore1 = dom gstore3 ∪ jro, fi = fi2, ndx0 = [], ndx2 = ndx0 + ndx1, nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0), nx = [], remove-refsize0(gstore1) = gstore1, elems nx1 ∩ jro0 = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro0, fi2.inos < jmaxino0, jro2 < jmaxino3, p_os < pmaxino, fi2.inos < jmaxino3, fi1.inos < pmaxino, inv(gstore2 \ jro0), inv(gstore1), inv(gstore3 \ jro), key-cons(ndx1), key-cons(ndx0), refsize-cons(gstore2, range fi2), refsize-cons(gstore1, range fi1), refsize-cons(gstore3, range fi2), ri-inj(fi2), ri-inj(fi1), jmaxino3 ≤ jmaxino0, pmaxino ≤ jmaxino3, pmaxino ≤ jmaxino0, ndx0.flashsize ≤ LEB_SIZE, fi2.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, ndx1.keys.toSet ⊆ dom fi2, ndx0.keys.toSet ⊆ dom fi2, range fi2 ⊆ dom nodes(gstore2 ↓, jro0), fi2.lebs ⊆ dom gstore3, dom gstore2 ⊆ dom gstore3, jvalid7 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), ndx1 = [] ∨ LEB_SIZE < ndx0.flashsize + ndx1.head.flashsize ⊦ ⟪err := EINVAL⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (∃ ndx. ndx2 = ndx + ndx1) ∧ jmaxino3 ≤ jmaxino0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro)) ∧ fi.inos < jmaxino0 ∧ fi.lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi) ∧ inv(gstore3 \ jro) ∧ elems nx ∩ jro = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore3 ∪ jro ∧ ri-inj(fi) ∧ ndx1.keys.toSet ⊆ dom fi ∧ range fi ⊆ dom nodes(gstore3 ↓, jro) ∧ dom gstore2 ⊆ dom gstore3 ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅ ∧ (∃ ndx, ndx0. ndx2 = ndx + ndx0 ∧ (err = ESUCCESS → ndx0 = ndx1) ∧ new(abs-log(nx, gstore3 ↓), nodes(gstore2 ↓, jro0)) ∧ ¬ dups(abs-log(nx, gstore3 ↓)) ∧ # abs-log(nx, gstore3 ↓) = # ndx ∧ fi = fi2[ndx.keys, abs-log(nx, gstore3 ↓)] ∧ nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0)[abs-log(nx, gstore3 ↓), ndx]) ∧ (err = ESUCCESS ⊃ # ndx1;0) < # ndx2), ndx0 + ndx1 = [], jmaxino3 = 0, pmaxino = 0, dups(nx1), dups(ndx0.keys + ndx1.keys), dups(ndx0.keys), dups(ndx1.keys) |
Used simplifier rules: ⊦ [] + ndx = ndx; (s)%a: ⊦ (ndx + ndx0) + ndx1 = ndx + ndx0 + ndx1; from specification list[node-list]% ⊦ [].keys = []; (s)% ⊦ [].toSet = ∅; (s)% ⊦ ∅ ⊆ ks; (s)% ⊦ [].flashsize = 0; (s)% ⊦ 0 ≤ m; (s)% ⊦ key-cons([]); (s)% ⊦ [] + kx = kx; (s)%a: ⊦ (kx + kx0) + kx1 = kx + kx0 + kx1; from specification list[key-list-set]% ⊦ ¬ dups([]); (s)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ ESUCCESS ≠ EINVAL; (s)% ⊦ ⌊EINVAL⌋ ; (s)% ⊦ ndx = ndx0 + ndx ↔ ndx0 = []; (s)% ⊦ ns < n ∧ n ≤ m → (ns < m ↔ true); (ss)% ⊦ elems [] = ∅; (s)% ⊦ ns ∩ ∅ = ∅; (s)%int-a: ⊦ (ns ∩ ns0) ∩ ns1 = ns ∩ ns0 ∩ ns1; from specification set-union[nat-set]%int-c: ⊦ ns ∩ ns0 = ns0 ∩ ns; from specification set-union[nat-set]% ⊦ ¬ dups([]); (s)% ⊦ ns ∪ ∅ = ns; (s)%una: ⊦ (ns ∪ ns0) ∪ ns1 = ns ∪ ns0 ∪ ns1; from specification set-union[nat-set]%unc: ⊦ ns ∪ ns0 = ns0 ∪ ns; from specification set-union[nat-set]% ⊦ [].toSet = ∅; (s)% ⊦ ∅ \ ns = ∅; (s)% ⊦ abs-log([], gstore) = []; (s)% ⊦ new([], fs); (s)% ⊦ ¬ dups([]); (s)% ⊦ # [] = 0; (s)% ⊦ # ndx = 0 ↔ ndx = []; (s)% ⊦ ri[[], []] = ri; (s)% ⊦ fs[[], []] = fs; (s)% ⊦ 0 < m ↔ m ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%sub-ntrans: ⊦ as ⊆ as0 ∧ ¬ as ⊆ as1 → ¬ as0 ⊆ as1; (forward) from specification set-basic[node-store]%sub-ntrans-01: ⊦ as ⊆ as0 ∧ ¬ as1 ⊆ as0 → ¬ as1 ⊆ as; (forward) from specification set-basic[node-store]