Proof step 180 from proof refine-gc (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 181:

  # lax = # gndx0, # ax = # referenced-adrs(lax.to-adr(n1), ri), gstore2[n1] = groupblock(gndx0, lax, m0), abs-log(nx0, gstore3 ↓) = abs-log(nx1, gstore2 ↓) + ax, fs = nodes(gstore2 ↓, jro0), log = abs-log(nx1, gstore2 ↓), nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0)[ax, nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)]], remove-refsize0(gstore1) = gstore1, ri0 = ri, elems nx1 ∩ jro0 = ∅, (nx0.toSet \ nx1.toSet) ∩ dom gstore2 = ∅, elems nx0 ∩ jro = ∅, dom gstore1 ∪ elems nx0 = jro ∪ dom gstore3, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro0, #(jro ∪ dom gstore3) ≠ 0, jmaxino ≠ 0, jmaxino0 ≠ 0, m0 ≠ 0, pmaxino ≠ 0, jro ∪ dom gstore3 ≠ ∅, jro1.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, ri[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)].keys, ax].inos < jmaxino0, jro1 < jmaxino0, inv(gstore2 \ jro0), inv(gstore1), inv(groupblock(gndx0, lax, m0)), inv(gstore3 \ jro), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro0)), new(ax, nodes(gstore2 ↓, jro0)), refsize-cons(gstore3 -- n1, range ri[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)].keys, ax]), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), refsize-cons(gstore3, range ri[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)].keys, ax]), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(ri), ri-inj(ri[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)].keys, ax]), n1 ∈ jro ∪ dom gstore3, n1 ∈ gstore3, n1 ∈ gstore2, n1 ∈ gstore1, pmaxino ≤ jmaxino, jmaxino ≤ jmaxino0, pmaxino ≤ jmaxino0, range ri ⊆ dom nodes(gstore2 ↓, jro0), fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, dom gstore2 ⊆ dom gstore3, ri[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)].keys, ax].lebs ⊆ dom gstore3, ri.lebs ⊆ dom gstore3, ¬ dups(ax), ¬ dups(nx0), ¬ dups(nx1), ¬ dups(nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)].keys), ¬ n1 ∈ nx0, ¬ n1 ∈ jro0, ¬ n1 ∈ nx1, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore3 -- n1, jro ++ n1), jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore3, jro), jvalid3 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), jvalid5 → jvalid4 ⊦ ⟨aubifs_core_journal_gc#(fi1, jro1.keys, p_os.keys; ri, fs, log; jvalid5)⟩ ( ri0[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri0)].keys, ax] = ri ∧ log = abs-log(nx0, gstore3 ↓) ∧ fs = nodes(gstore3 ↓, jro) \ (dom nodes(gstore3 ↓, jro) | n1)), ∃ adr. adr.lnum = n1 ∧ adr ∈ ri[nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(adr.lnum), ri)].keys, ax]

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ ns ≠ ∅ → # ns ≠ 0; (forward) from specification set-basic[nat-set]%ne-01: ⊦ n ∈ ns → ns ≠ ∅; (forward) from specification set-basic[nat-set]% ⊦ n ∈ ns → ns ++ n = ns; (s)% ⊦ ns ++ n = ns ↔ n ∈ ns; (s)% ⊦ ns ++ n ++ n = ns ++ n; (s)%⊦ nodes(gstore -- n, ginval ++ n) = nodes(gstore, ginval) \ (dom nodes(gstore, ginval) | n); (s)% ⊦ ¬ n ∈ nx → abs-log(nx, gstore -- n) = abs-log(nx, gstore); (s)% ⊦ (gstore -- n)↓ = gstore ↓ -- n; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ inv(gstore \ ns) → inv(gstore \ (ns ++ n)); (s)% ⊦ n ∈ gstore → (gstore \ (ns ++ n)) -- n = gstore \ (ns ++ n); (s)% ⊦ (gstore -- n) \ ns = (gstore \ ns) -- n; (s)% ⊦ n ∈ ri.lebs ↔ (∃ adr. adr.lnum = n ∧ adr ∈ ri); (s)% ⊦ ns ⊆ ns0 -- n ↔ ns ⊆ ns0 ∧ ¬ n ∈ ns; (ws)%int-c: ⊦ ns ∩ ns0 = ns0 ∩ ns; from specification set-union[nat-set]%int-a: ⊦ (ns ∩ ns0) ∩ ns1 = ns ∩ ns0 ∩ ns1; from specification set-union[nat-set]% ⊦ n ∈ elems nx ↔ n ∈ nx; (s)% ⊦ ns ∩ (ns0 ++ n) = ∅ ↔ ns ∩ ns0 = ∅ ∧ ¬ n ∈ ns; (ws)%unc: ⊦ ns ∪ ns0 = ns0 ∪ ns; from specification set-union[nat-set]%una: ⊦ (ns ∪ ns0) ∪ ns1 = ns ∪ ns0 ∪ ns1; from specification set-union[nat-set]% ⊦ (ns ∪ (ns0 -- n)) ++ n = (ns ∪ ns0) ++ n; (s)% ⊦ (ns ++ n) ∪ ns0 = (ns ∪ ns0) ++ n; (s)% ⊦ dom(gstore -- n) = dom gstore -- n; (s)