| m8 + 1 = fs[ri[inodekey(fs[ri[dentrykey(m, str0)]].ino)]].nlink, m0 + 1 = fs[ri[inodekey(m)]].size, n0 + (boolvar3 ⊃ 1;0) = fs[ri[inodekey(m)]].nsubdirs, ¬ fs[ri[inodekey(fs[ri[dentrykey(m, str0)]].ino)]].directory ↔ ¬ boolvar0, fs[ri[dentrykey(m, str)]] = dentrynode(key0, m2), fs[ri[inodekey(m2)]] = inodenode(key1, md0, boolvar0, m5, m9, m10), fs[ri[inodekey(m)]].directory, fo.inodes?, ro.inodes?, file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), ri-cons(ri, fs), ri-inj(fi), ri-inj(ri), ubifs-cons(fs, ri, ro, fi, fo, log), dentrykey(m, str) ∈ ri, inodekey(m2) ∈ ri, dentrykey(m, str0) ∈ ri, inodekey(fs[ri[dentrykey(m, str0)]].ino) ∈ ri, inodekey(m) ∈ ri, ri[dentrykey(m, str)] ∈ fs, ri[inodekey(m2)] ∈ fs, ⌊err0⌋ , m8 = 0 → links(fs[ri[dentrykey(m, str0)]].ino, fs, ri) = ∅ ++ dentrykey(m, str0), fs[ri[inodekey(fs[ri[dentrykey(m, str0)]].ino)]].directory → dentrykeys(inodekey(fs[ri[dentrykey(m, str0)]].ino), ri) = ∅, fs[ri[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO, ¬ boolvar0 ∧ ¬ boolvar3 ∨ boolvar0 ∧ boolvar3 ∧ m3 = m10, ¬ boolvar0 ∧ ¬ boolvar2 ∨ fs[ri[inodekey(fs[ri[dentrykey(m, str0)]].ino)]].directory ∧ boolvar2 ∧ m6 = fs[ri[inodekey(fs[ri[dentrykey(m, str0)]].ino)]].size ⊦ ⟪skip⟫ (ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro)), fs[ri[dentrykey(m, str0)]].ino = 0, fs[ri[dentrykey(m, str0)]].ino = ROOT_INO, m = 0, mkdentry(str, m2) = mkdentry(str0, fs[ri[dentrykey(m, str0)]].ino), inodekey(m) ∈ ro |