| (m = m2 ⊃ mkdir(m0, md1, m3, m1, abs-children(m2, fs, ri) -- str) ;mkdir(fs[ri[inodekey(m)]].size, fs[ri[inodekey(m)]].meta, 1, fs[ri[inodekey(m)]].nsubdirs, ∅) ) = mkdir(m4, md, 0, m6, entries), 1 = fs[ri[inodekey(m)]].nlink, fs[ri[dentrykey(m2, str)]] = dentrynode(key, m), fs[ri[inodekey(m2)]] = inodenode(key0, md1, true, m3, m1 + 1, m0 + 1), abs-children(m, fs, ri) = ∅, dentrykeys(inodekey(m), ri) = ∅, links(m, fs, ri) = ∅ ++ dentrykey(m2, str), fs[ri[inodekey(m)]].directory, orphans(fs, ri).inodes?, fo.inodes?, afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, orphans(fs, ri)), replay-cons-strong(fs, ri, orphans(fs, ri), fi, fo, log), ri-cons(ri, fs), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), ri[inodekey(m2)] ∈ fs, inodekey(m) ∈ ri, ri[dentrykey(m2, str)] ∈ fs, dentrykey(m2, str) ∈ ri, inodekey(m2) ∈ ri, asynced → boolvar0, ∀ adr, adr0, adr1. adr ∈ fs ∨ adr0 ∈ fs ∨ adr1 ∈ fs ∨ adr = adr0 ∨ adr = adr1 ∨ adr0 = adr1 ⊦ ⟨asynced := ?⟩ ((asynced → boolvar) ∧ ENOSPC = ENOSPC), # links(m2, abs-dirs(fs, ri)) = 0, links(m2, abs-dirs(fs, ri)) = ∅, m = ROOT_INO, m = 0, m2 = ROOT_INO, m2 = 0, m3 = 0 |