This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| initialization | ino = LEB_SIZE ⊦ ⟪vfs_format#(n, isdir0, ino, md; dirs, files, asynced; of, ino0, err)⟫ ( ( err = ESUCCESS → ⟨posix_format#(n, isdir0, ino, md; ; root, fs0, ofh0, psynced, err0)⟩ ((ofh0 = abs-of(of) ∧ fs0 = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ tree, fs, ofh, isdir. ⟨posix_format#(n, isdir0, ino, md; ; root, fs0, ofh0, psynced, err0)⟩ (tree = root ∧ fs = fs0 ∧ ofh = ofh0 ∧ (isdir ↔ psynced) ∧ err = err0)))) | A Proof Obligation |
| refine-mkdir | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_mkdir#(path, md, user; err, dirs, files, asynced)⟫ ⟨posix_mkdir#(path, md, user, fs, ofh; err0, root; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-rmdir | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_rmdir#(path, user, of; err, dirs, files, asynced)⟫ ⟨posix_rmdir#(path, user, fs, ofh; err0, root; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-create | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_create#(path, md, user; err, dirs, files, asynced)⟫ ⟨posix_create#(path, md, user, ofh; err0, root, fs; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-open | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), fd = ino0, err = err0 ⊦ ⟪vfs_open#(path, mode, user, dirs, files, asynced; fd, err, of, ino)⟫ ⟨posix_open#(path, mode, user, root, fs; ino0, err0, ofh)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ fd = ino0 ∧ err = err0) | A Proof Obligation |
| refine-close | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_close#(fd, user, asynced; err, of, dirs, files)⟫ ⟨posix_close#(fd, user, root; err0, fs, ofh)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-read | n ≤ # buf, ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), buf = buf0, n = n0, err = err0 ⊦ ⟪vfs_read#(fd, user, dirs, files, asynced; buf, n, err, of)⟫ ⟨posix_read#(fd, user, root, fs; buf0, n0, err0, ofh)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ buf = buf0 ∧ n = n0 ∧ err = err0) | A Proof Obligation |
| refine-write | n ≤ # buf, ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), n = n0, err = err0 ⊦ ⟪vfs_write#(fd, buf, user; n, err, of, dirs, files, asynced)⟫ ⟨posix_write#(fd, buf, user, root; n0, err0, fs, ofh; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ n = n0 ∧ err = err0) | A Proof Obligation |
| refine-seek | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), n = n0, err = err0 ⊦ ⟪vfs_seek#(fd, whence, user, dirs, files, asynced; n, err, of)⟫ ⟨posix_seek#(fd, whence, user, root, fs; n0, err0, ofh)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ n = n0 ∧ err = err0) | A Proof Obligation |
| refine-renam | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_rename#(path, path', user, of; err, dirs, files, asynced)⟫ ⟨posix_rename#(path, path', user, ofh; err0, root, fs; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-link | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_link#(path, path', user; err, dirs, files, asynced)⟫ ⟨posix_link#(path, path', user, fs, ofh; err0, root; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-unlink | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_unlink#(path, user, of; err, dirs, files, asynced)⟫ ⟨posix_unlink#(path, user, ofh; err0, root, fs; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-truncate | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_truncate#(path, n, user; err, dirs, files, asynced)⟫ ⟨posix_truncate#(path, n, user, root, ofh; err0, fs; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-readmeta | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), md = md0, ino0 = ino1, ino2 = ino3, err = err0 ⊦ ⟪vfs_readmeta#(path, user, dirs, files, asynced; md, ino0, ino2, err)⟫ ⟨posix_readmeta#(path, user, root, fs, ofh; md0, ino1, ino3, err0)⟩ ( (ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ md = md0 ∧ ino0 = ino1 ∧ ino2 = ino3 ∧ err = err0) | A Proof Obligation |
| refine-writemeta | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), err = err0 ⊦ ⟪vfs_writemeta#(path, md, user; err, dirs, files, asynced)⟫ ⟨posix_writemeta#(path, md, user, ofh; err0, root, fs; psynced)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-readdir | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), strings = strings0, err = err0 ⊦ ⟪vfs_readdir#(path, user, dirs, files, asynced; strings, err)⟫ ⟨posix_readdir#(path, user, root, fs, ofh; strings0, err0)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ strings = strings0 ∧ err = err0) | A Proof Obligation |
| recovery | dirs = dirs0 \ orphans(dirs0, files), files0 = files \ orphans(dirs0, files), ofh0 = abs-of(of), fs0 = abs-files(files), abs(tree0, ROOT_INO)(dirs0), isdir0 → isdir1, isdir1, tree0.dir?, fids-cons(tree0, fs0, ofh0), of-cons(of, dirs0, files), dom of < ino, afs-cons(dirs0, files) ⊦ ⟪vfs_recover#(isdir2; dirs, files0, asynced; of0, ino0, err)⟫ ( ( err = ESUCCESS → (∃ root, fs, ofh, psynced. posix-crash(tree0, fs0, ofh0, root, fs, ofh) ∧ ⟨posix_recover#(isdir2; root, fs, ofh; psynced, err0)⟩ ((ofh = abs-of(of0) ∧ fs = abs-files(files0) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ tree, fs, ofh, isdir. ⟨posix_recover#(isdir2; root0, fs1, ofh1; psynced0, err0)⟩ (tree = root0 ∧ fs = fs1 ∧ ofh = ofh1 ∧ (isdir ↔ psynced0) ∧ err = err0)))) | A Proof Obligation |
| synced | psynced, ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino ⊦ asynced | A Proof Obligation |
| refine-fsyncdir | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_fsyncdir#(path, isdir, user, dirs, files; asynced; err)⟫ ⟨posix_fsyncdir#(path, isdir, user; ; psynced, err0)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-fsync | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_fsync#(path, isdir, user, dirs, files; asynced; err)⟫ ⟨posix_fsync#(path, isdir, user, root, fs, ofh; ; psynced, err0)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| refine-sync | ofh = abs-of(of), fs = abs-files(files), abs(root, ROOT_INO)(dirs), psynced → asynced, root.dir?, fids-cons(root, fs, ofh), of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_sync#(dirs, files; asynced; err)⟫ ⟨posix_sync#(; ; psynced, err0)⟩ ((ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced)) ∧ err = err0) | A Proof Obligation |
| abs-acyclic | ⊦ abs(tree, ROOT_INO)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n, md, m, m0, entries) ∧ str ∈ entries ∧ ispath(p, ROOT_INO, ino, dirs, files) → entries[str] ≠ ROOT_INO | A User Theorem |
| abs-fold-del | ⊦ str ∈ entries ∧ p ∈ tree ∧ tree[p] = dnode(md, sdt) ∧ ((abs|(tree, ROOT_INO, p, ino0) * ino0 => mkdir(# entries - 1, md, m0, m1, entries -- str) * abs(sdt -- str, entries -- str)))(dirs) → abs(tree -- (p + str '), ROOT_INO)(dirs) | A User Theorem |
| abs-fold-del-p | ⊦ str ∈ entries ∧ p ∈ tree ∧ tree[p] = dnode(md, sdt) ∧ ((abs|(tree, ROOT_INO, p, ino0) * ino0 => mkdir(# entries - 1, md, m0, m1, entries -- str) * abs(sdt -- str, entries -- str) * D))(dirs) → ((abs(tree -- (p + str '), ROOT_INO) * D))(dirs) | A User Theorem |
| abs-fold-new | abs(tree0, ino1) = emp ⊦ ¬ str ∈ entries ∧ p ∈ tree ∧ tree[p] = dnode(md, sdt) ∧ ((abs|(tree, ROOT_INO, p, ino0) * ino0 => mkdir(# entries + 1, md, m0, m1, entries[str, ino1]) * abs(sdt, entries)))(dirs) → abs(tree[p + str ', tree0], ROOT_INO)(dirs) | A User Theorem |
| abs-fold-new-p | D ⊆ abs(tree0, ino1) ⊦ ¬ str ∈ entries ∧ p ∈ tree ∧ tree[p] = dnode(md, sdt) ∧ ((abs|(tree, ROOT_INO, p, ino0) * ino0 => mkdir(# entries + 1, md, m0, m1, entries[str, ino1]) * abs(sdt, entries) * D))(dirs) → abs(tree[p + str ', tree0], ROOT_INO)(dirs) | A User Theorem |
| abs-unfold | ⊦ ispath(p, ROOT_INO, ino, dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n, md, m0, m1, entries) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ ¬ abs(tree0, ROOT_INO)(dirs0) → ( abs(tree, ROOT_INO)(dirs) ↔ (∃ sdt. ((abs|(tree, ROOT_INO, p, ino) * ino => mkdir(n, md, m0, m1, entries) * abs(sdt, entries)))(dirs) ∧ p ∈ tree ∧ tree[p] = dnode(md, sdt))) | A User Theorem |
| abs-unfold-entry-p | ⊦ str ∈ entries ∧ entries[str] ∈ dirs0 ∧ dirs1 ≡ dirs0[entries[str], ad] → (((abs(sdt, entries) * D))(dirs0) ↔ str ∈ sdt ∧ ((abs(sdt[str], entries[str]) * abs(sdt -- str, entries -- str) * D))(dirs0)) | A User Theorem |
| dir-empty | ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ m ∈ dirs ∧ dirs[m] = mkdir(m0, md, n0, n1, entries) ∧ str ∈ entries ∧ entries[str] ∈ dirs → (dirs[entries[str]].entries = ∅ ↔ tree[p + str '].entries = ∅) | A User Theorem |
| dir-entry | ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ m ∈ dirs ∧ dirs[m] = mkdir(m0, md, n0, n1, entries) ∧ str ∈ entries → (entries[str] ∈ dirs ↔ tree[p + str '].dir?) | A User Theorem |
| fid-file | ⊦ ⌜n⌝ ∈ tree.fids ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) → n ∈ files | A User Theorem |
| fid-ino | ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ m ∈ files → (tree[p] = fnode(fid) ↔ fid = ⌜m⌝ ) | A User Theorem |
| fid-ino-entry | ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ m ∈ dirs ∧ dirs[m] = mkdir(m0, md, n0, n1, entries) ∧ str ∈ entries ∧ entries[str] ∈ files → (tree[p + str '] = fnode(fid) ↔ fid = ⌜entries[str]⌝ ) | A User Theorem |
| file-fid | ⊦ n ∈ files ∧ abs(tree, ROOT_INO)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (⌜n⌝ ∈ tree.fids ↔ links(n, dirs) ≠ ∅) | A User Theorem |
| files-del-eq | ⊦ ino ∈ files0 ∧ ino ∈ files1 ∧ abs-files(files0)[⌜ino⌝ , f] ≠ abs-files(files) → (files0 -- ino = files1 -- ino ↔ (∃ af. files1 = files0[ino, af])) | A User Theorem |
| ispath-target | ⊦ ispath(p, ino, dirs, files) ↔ (∃ m. ispath(p, ino, m, dirs, files)) | A User Theorem |
| make-abs-fold-work | ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n, md, n0, n1, entries) → # entries = n | A User Theorem |
| of | ⊦ ⌜ino⌝ ∈ abs-of(of).fids ↔ is-open(ino, of) | A User Theorem |
| path-in | ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → p ∈ tree ∧ (tree[p].dir? ↔ m ∈ dirs) | A User Theorem |
| path-in-eq | ⊦ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (p ∈ tree ↔ ispath(p, ino, dirs, files)) | A User Theorem |
| path-in-last | ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (p + str ' ∈ tree ↔ m ∈ dirs ∧ str ∈ dirs[m].entries) | A User Theorem |
| pr | ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (pr(user, p, tree, abs-files(files)) ↔ pr(user, meta(ε, m, dirs, files))) | A User Theorem |
| pw | ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (pw(user, p, tree, abs-files(files)) ↔ pw(user, meta(ε, m, dirs, files))) | A User Theorem |
| px | ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (px(user, p, tree, abs-files(files)) ↔ px(user, p, ino, dirs, files)) | A User Theorem |
| px-parent | ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (px-parent(user, p, tree, abs-files(files)) ↔ px-parent(user, p, ino, dirs, files)) | A User Theorem |
| px-prefix | ⊦ ispath(q, ino, m, dirs, files) ∧ px(user, p, tree, abs-files(files)) ∧ q ⊑ p ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → px(user, q, ino, dirs, files) | A User Theorem |
| py | ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (py(user, p, tree, abs-files(files)) ↔ py(user, p, ino, dirs, files)) | A User Theorem |
| py-last | ⊦ ispath(p, ino, m, dirs, files) ∧ py(user, p, ino, dirs, files) → px(user, meta(ε, m, dirs, files)) | A User Theorem |
| py-prefix | ⊦ ispath(q, ino, m, dirs, files) ∧ py(user, p, tree, abs-files(files)) ∧ q ⊑ p ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → px(user, q, ino, dirs, files) | A User Theorem |
| py-pw | ⊦ ispath(p, ino, m, dirs, files) ∧ py(user, p, ino, dirs, files) → pw(user, meta(ε, m, dirs, files)) | A User Theorem |
| py-px | ⊦ ispath(p, ino, m, dirs, files) ∧ py(user, p, ino, dirs, files) → px(user, p, ino, dirs, files) | A User Theorem |
| py-px-prefix | ⊦ ispath(q, ino, m, dirs, files) ∧ q ⊑ p ∧ py(user, p, ino, dirs, files) → px(user, q, ino, dirs, files) | A User Theorem |
| py-strong | ⊦ ispath(q, ino, m, dirs, files) ∧ px-parent(user, q, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (py(user, q, ino, dirs, files) ↔ pw(user, meta(ε, m, dirs, files)) ∧ px(user, meta(ε, m, dirs, files))) | A User Theorem |