Proof step 6 from proof replay-safe-gc-copy (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # ax0 = # kx1, ro.inodes?, new(ax0, fs), orphans-cons(fs, ri, ro), ri-closed(ri, fs, ro), ri-cons(ri, fs), key ∈ ri, kx1.toSet ⊆ dom ri, ∀ kx0, ro0, fs0, ri0. # kx1 = # kx0 ∧ ro0.inodes? ∧ new(ax0, fs0) ∧ orphans-cons(fs0, ri0, ro0) ∧ ri-closed(ri0, fs0, ro0) ∧ ri-cons(ri0, fs0) ∧ kx0.toSet ⊆ dom ri0 → dups(kx0) ∨ replay-safe(ax0, fs0[ax0, fs0[ri0[kx0]]], ri0 ⊖ ro0) ⊦ dups(ax0), dups(kx1), adr ∈ fs, adr ∈ ax0, key ∈ kx1, ¬ adr ∈ ri ⊖ ro ∧ node-cons(fs[adr, fs[ri[key]]][ax0, fs[ri[kx1]]][adr].key, fs[adr, fs[ri[key]]][ax0, fs[ri[kx1]]][adr]) ∧ replay-safe(ax0, fs[adr, fs[ri[key]]][ax0, fs[ri[kx1]]], replay-one(adr, fs[adr, fs[ri[key]]][ax0, fs[ri[kx1]]][adr], ri ⊖ ro))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (ndx + ndx0) + ndx1 = ndx + ndx0 + ndx1; from specification list[node-list]% ⊦ fs[adr ' + ax, nd ' + ndx] = fs[adr, nd][ax, ndx]; (s)%a: ⊦ (ax + ax0) + ax1 = ax + ax0 + ax1; from specification list[address-list-set]% ⊦ nd + ndx = nd ' + ndx; (s)% ⊦ fs[adr ' + ax] = fs[adr] + fs[ax]; (s)% ⊦ adr + ax = adr ' + ax; (s)% ⊦ ri[key ' + kx] = ri[key] + ri[kx]; (s)% ⊦ dups(key ' + kx) ↔ dups(kx) ∨ key ∈ kx; (ws)% ⊦ key ∈ dom ri ↔ key ∈ ri; (s)% ⊦ ks ++ key ⊆ ks0 ↔ ks ⊆ ks0 ∧ key ∈ ks0; (ws)%unc: ⊦ ks ∪ ks0 = ks0 ∪ ks; from specification set-union[node-index]%una: ⊦ (ks ∪ ks0) ∪ ks1 = ks ∪ ks0 ∪ ks1; from specification set-union[node-index]% ⊦ ks ∪ ∅ = ks; (s)% ⊦ (ks ++ key) ∪ ks0 = (ks ∪ ks0) ++ key; (s)% ⊦ key '.toSet = ∅ ++ key; (s)% ⊦ (kx + kx0).toSet = kx.toSet ∪ kx0.toSet; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + n = m + n0 ↔ n = n0; (s)%a: ⊦ (kx + kx0) + kx1 = kx + kx0 + kx1; from specification list[key-list-set]% ⊦ m +1 = m + 1; (s)% ⊦ #(key ' + kx) = (# kx)+1; (s)% ⊦ key + kx = key ' + kx; (s)