| (ino0 = ino ⊃ mkfile(0, md, 1, ∅);(files ++ ino)[ino0]) = mkfile(m4, md2, m5, content0), files[ino0] = mkfile(m1, md1, m3, content), dirs[m] = mkdir(m0, md0, # links(m, dirs), m2, entries), dirs[ino0] = mkdir(m6, md3, m7, m8, entries0), afs-cons(dirs, files), ROOT_INO ∈ dirs, m ∈ dirs, ino0 ∈ dirs ∧ name ∈ entries0 → entries0[name] ∈ dirs ∨ entries0[name] ∈ files, ino0 ∈ files → ¬ ino0 ∈ dirs ∧ m3 = # links(ino0, dirs), ino0 ∈ dirs → m7 = # links(ino0, dirs) ∧ m7 ≤ 1 ∧ m6 = # entries0 ∧ m8 = # subdirs(ino0, dirs), ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → entries0 = ∅, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ino = 0, ino ∈ files, ino ∈ dirs, str ∈ entries, ( ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).entries = ∅) ∧ ( ino0 ∈ dirs → (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).nlink = # links(ino0, dirs) ∧ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).nlink ≤ 1 ∧ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).size = # (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).entries ∧ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).nsubdirs = # subdirs(ino0, dirs[m, mkdir(m0, md0, # links(m, dirs), m2, entries[str, ino])])) ∧ (ino0 = ino ∨ ino0 ∈ files → ¬ ino0 ∈ dirs ∧ m5 = # (ino = ino0 ⊃ ∅ ++ mklink(m, str);links(ino0, dirs))) ∧ ( ino0 ∈ dirs ∧ name ∈ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).entries → (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).entries[name] ∈ dirs ∨ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).entries[name] = ino ∨ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);dirs[ino0]).entries[name] ∈ files) ∧ ((ino0 = ino ∨ ino0 ∈ files) ∧ n ∈ content0 → # content0[n] = VFS_PAGE_SIZE) |
(ino0 = ino ⊃ mkfile(0, md, 1, ∅);(files ++ ino)[ino0]) = mkfile(m4, md2, m5, content0), dirs[ino0] = mkdir(m6, md3, m7, m8, entries0), dirs[m] = mkdir(m0, md0, # links(m, dirs), m2, entries), files[ino0] = mkfile(m1, md1, m3, content), afs-cons(dirs, files), m ∈ dirs, ROOT_INO ∈ dirs, ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → entries0 = ∅, ino0 ∈ files → ¬ ino0 ∈ dirs ∧ m3 = # links(ino0, dirs), ino0 ∈ dirs ∧ name ∈ entries0 → entries0[name] ∈ dirs ∨ entries0[name] ∈ files, ino0 ∈ dirs → m7 = # links(ino0, dirs) ∧ # links(ino0, dirs) ≤ 1 ∧ m6 = # entries0 ∧ m8 = # subdirs(ino0, dirs), links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ino = 0, str ∈ entries, ino ∈ dirs, ino ∈ files, ( ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).entries = ∅) ∧ ( ino0 ∈ dirs → (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).nlink = # links(ino0, dirs) ∧ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).nlink ≤ 1 ∧ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).size = # (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).entries ∧ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).nsubdirs = # subdirs(ino0, dirs[m, mkdir(m0, md0, # links(m, dirs), m2, entries[str, ino])])) ∧ (ino0 = ino ∨ ino0 ∈ files → ¬ ino0 ∈ dirs ∧ m5 = # (ino = ino0 ⊃ ∅ ++ mklink(m, str);links(ino0, dirs))) ∧ ( ino0 ∈ dirs ∧ name ∈ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).entries → (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).entries[name] ∈ dirs ∨ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).entries[name] = ino ∨ (ino0 = m ⊃ mkdir(m0 + 1, md0, # links(m, dirs), m2, entries[str, ino]);mkdir(m6, md3, m7, m8, entries0)).entries[name] ∈ files) ∧ ((ino0 = ino ∨ ino0 ∈ files) ∧ n ∈ content0 → # content0[n] = VFS_PAGE_SIZE)