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: |
|---|---|---|
| dir-empty | ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅ | An Axiom |
| valid-ino | ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files | An Axiom |
| valid-dir-ino | ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs | An Axiom |
| valid-file-ino | ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files | An Axiom |
| valid-negdentry | ⊦ valid-negdentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ ¬ dent.name ∈ dirs[ino].entries ∧ dent.negdentry? | An Axiom |
| path-here | ⊦ ispath(ε, n, m, dirs, files) ↔ valid-ino(n, dirs, files) ∧ m = n | An Axiom |
| path-rec | ⊦ ispath(str ' + p, n, m, dirs, files) ↔ valid-dir-ino(n, dirs, files) ∧ str ∈ dirs[n].entries ∧ ispath(p, dirs[n].entries[str], m, dirs, files) | An Axiom |
| afs-cons | ⊦ afs-cons(dirs, files) ↔ (∀ ino. ROOT_INO ∈ dirs ∧ (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dir-empty(ino, dirs, files)) ∧ ( ino ∈ dirs → ¬ ino ∈ files ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs)) ∧ (ino ∈ files → ¬ ino ∈ dirs ∧ files[ino].nlink = # links(ino, dirs)) ∧ (∀ name. ino ∈ dirs ∧ name ∈ dirs[ino].entries → valid-ino(dirs[ino].entries[name], dirs, files)) ∧ (∀ n. ino ∈ files ∧ n ∈ files[ino].content → valid-pagesize(ino, n, files))) | An Axiom |
| expath | ⊦ ispath(p, n, dirs, files) ↔ (∃ m. ispath(p, n, m, dirs, files)) | An Axiom |
| lookup-rec | ⊦ ino ∈ dirs ∧ str ∈ dirs[n].entries → lookup(str ' + p, n, dirs, files) = lookup(p, dirs[n].entries[str], dirs, files) | An Axiom |
| lookup-here | ⊦ valid-ino(n, dirs, files) → lookup(ε, n, dirs, files) = n | An Axiom |
| at-upto | ⊦ m * VFS_PAGE_SIZE < n ∧ m ∈ content → (content upto n)[m] = content[m] | An Axiom |
| in-upto | ⊦ m ∈ content upto n ↔ m * VFS_PAGE_SIZE < n ∧ m ∈ content | An Axiom |
| links | ⊦ alink ∈ links(ino, dirs) ↔ alink.pino ∈ dirs ∧ alink.name ∈ dirs[alink.pino].entries ∧ ino = dirs[alink.pino].entries[alink.name] | An Axiom |
| valid-inode | ⊦ valid-inode(inode, dirs, files) ↔ inode = getinode(inode.ino, dirs, files) | An Axiom |
| valid-pagesize | ⊦ valid-pagesize(ino, n, files) ↔ # files[ino].content[n] = VFS_PAGE_SIZE | An Axiom |
| valid-dentry-03 | ⊦ valid-dentry(dent, dirs, files) ↔ (∃ ino. valid-dentry(ino, dent, dirs, files)) | An Axiom |
| valid-dentry-with-parent | ⊦ valid-dentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ valid-ino(dent.ino, dirs, files) ∧ dent.name ∈ dirs[ino].entries ∧ dent.ino = dirs[ino].entries[dent.name] ∧ dent.dentry? | An Axiom |
| getinode | ⊦ getinode(ino, dirs, files) = (ino ∈ dirs ⊃ mkinode(ino, dirs[ino].meta, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size) ;mkinode(ino, files[ino].meta, false, files[ino].nlink, 0, files[ino].size) ) | An Axiom |
| meta | ⊦ ispath(p, n, dirs, files) → meta(p, n, dirs, files) = (lookup(p, n, dirs, files) ∈ dirs ⊃ dirs[lookup(p, n, dirs, files)].meta;files[lookup(p, n, dirs, files)].meta) | An Axiom |
| valid-parent-ino | ⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO) | An Axiom |
| valid-content | ⊦ valid-content(ino, files) ↔ (∀ n. n ∈ files[ino].content → n * VFS_PAGE_SIZE < files[ino].size) | An Axiom |
| orphans | ⊦ ino ∈ orphans(dirs, files) ↔ valid-ino(ino, dirs, files) ∧ links(ino, dirs) = ∅ ∧ ino ≠ ROOT_INO | An Axiom |
| subdirs | ⊦ str ∈ subdirs(ino, dirs) ↔ ino ∈ dirs ∧ str ∈ dirs[ino].entries ∧ dirs[ino].entries[str] ∈ dirs | An Axiom |
| afs-cons-dir-nlink | ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) → # links(ino, dirs) = n | A User Theorem |
| afs-cons-file-nlink | ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, n, content) → # links(ino, dirs) = n | A User Theorem |
| afs-cons-in-next | ⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries ∧ afs-cons(dirs, files) → (entries[str] ∈ files ↔ ¬ entries[str] ∈ dirs) | A User Theorem |
| afs-cons-init | ⊦ afs-cons((∅ ++ ROOT_INO)[ROOT_INO, mkdir(0, md, 0, 0, ∅)], ∅) | A User Theorem |
| afs-cons-links-empty | ⊦ afs-cons(dirs, files) → (links(ino, dirs) = ∅ ↔ (ino ∈ dirs → dirs[ino].nlink = 0) ∧ (ino ∈ files → files[ino].nlink = 0)) | A User Theorem |
| afs-cons-links-rmorphans | ⊦ afs-cons(dirs, files) → links(ino, dirs \ orphans(dirs, files)) = links(ino, dirs) | A User Theorem |
| afs-cons-nlink0-empty | ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → entries = ∅ | A User Theorem |
| afs-cons-nlink0-notin | ⊦ afs-cons(dirs, files) ∧ ¬ ino ∈ dirs ∧ ¬ ino ∈ files → links(ino, dirs) = ∅ | A User Theorem |
| afs-cons-non0 | ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries → entries[str] ≠ 0 | A User Theorem |
| afs-cons-notfile | ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files | A User Theorem |
| afs-cons-pagesize | ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, n0, content) ∧ n ∈ content → # content[n] = VFS_PAGE_SIZE | A User Theorem |
| afs-cons-root-dir | ⊦ afs-cons(dirs, files) → ROOT_INO ∈ dirs | A User Theorem |
| afs-cons-root-notfile | ⊦ afs-cons(dirs, files) → ¬ ROOT_INO ∈ files | A User Theorem |
| afs-cons-size-at-upto | ⊦ afs-cons(dirs, files) ∧ m * VFS_PAGE_SIZE < n ∧ m ∈ content ∧ ino ∈ files ∧ files[ino] = mkfile(m0, md, n0, content) → # (content upto n)[m] = VFS_PAGE_SIZE | A User Theorem |
| del-entries-neq | ⊦ str ∈ entries → entries -- str ≠ entries | A User Theorem |
| empty-upto | ⊦ ∅ upto n = ∅ | A User Theorem |
| expath-append | ⊦ ispath(p + q, ino, dirs, files) → ispath(p, ino, dirs, files) | A User Theorem |
| expath-eps | ⊦ ispath(ε, n, dirs, files) ↔ n ∈ dirs ∨ n ∈ files | A User Theorem |
| expath-one | ⊦ ispath(str ', n, dirs, files) ↔ n ∈ dirs ∧ str ∈ dirs[n].entries ∧ (dirs[n].entries[str] ∈ dirs ∨ dirs[n].entries[str] ∈ files) | A User Theorem |
| expath-prefix | ⊦ ispath(q, n, dirs, files) ∧ p ⊑ q → ispath(p, n, dirs, files) | A User Theorem |
| expath-rec | ⊦ ispath(str ' + q, n, dirs, files) ↔ valid-dir-ino(n, dirs, files) ∧ str ∈ dirs[n].entries ∧ ispath(q, dirs[n].entries[str], dirs, files) | A User Theorem |
| expath-split | ⊦ ispath(p + q, ino, dirs, files) ↔ (∃ m. ispath(p, ino, m, dirs, files) ∧ ispath(q, m, dirs, files)) | A User Theorem |
| expath-split-given | ⊦ ispath(p, n, m, dirs, files) → (ispath(p + q, n, dirs, files) ↔ ispath(q, m, dirs, files)) | A User Theorem |
| isexpath | ⊦ ispath(p, n, m, dirs, files) → ispath(p, n, dirs, files) | A User Theorem |
| link-mod-dir-meta | ⊦ m ∈ dirs → links(ino, dirs[m, dirs[m].meta:= md]) = links(ino, dirs) | A User Theorem |
| links-add-entry | ⊦ p_ino ∈ dirs → links(ino0, dirs[p_ino, mkdir(m0, md, n, n0, entries[str, ino])]) = (ino = ino0 ⊃ links(ino0, dirs[p_ino, mkdir(m0, md, n, n0, entries)]) ++ mklink(p_ino, str) ;(str ∈ entries ∧ entries[str] = ino0 ⊃ links(ino0, dirs[p_ino, mkdir(m0, md, n, n0, entries)]) -- mklink(p_ino, str) ;links(ino0, dirs[p_ino, mkdir(m0, md, n, n0, entries)]) ) ) | A User Theorem |
| links-dec-nsubdirs | ⊦ p_ino ∈ dirs → links(ino, dirs[p_ino, mkdir(m0, md, n0, n1 - 1, entries)]) = links(ino, dirs[p_ino, mkdir(m0, md, n0, n1, entries)]) | A User Theorem |
| links-del-entry | ⊦ ino0 ∈ dirs → links(ino, dirs[ino0, mkdir(m, md, n0, n1, entries -- str)]) = (str ∈ entries ∧ entries[str] = ino ⊃ links(ino, dirs[ino0, mkdir(m, md, n0, n1, entries)]) -- mklink(ino0, str) ;links(ino, dirs[ino0, mkdir(m, md, n0, n1, entries)]) ) | A User Theorem |
| links-deldir | ⊦ ino0 ∈ dirs ∧ dirs[ino0] = mkdir(m, md, n, n0, ∅) → links(ino, dirs -- ino0) = links(ino, dirs) | A User Theorem |
| links-delother | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries ∧ entries[str] ≠ ino → links(ino, dirs[p_ino, mkdir(m0, md, n, n0, entries -- str)]) = links(ino, dirs) | A User Theorem |
| links-delother-subdirs | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries ∧ entries[str] ≠ ino → links(ino, dirs[p_ino, mkdir(m0, md, n, n1, entries -- str)]) = links(ino, dirs) | A User Theorem |
| links-delsame | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries → links(entries[str], dirs[p_ino, mkdir(m0, md, n, n0, entries -- str)]) = links(entries[str], dirs) -- mklink(p_ino, str) | A User Theorem |
| links-delsame-mod-subdirs | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries → links(entries[str], dirs[p_ino, mkdir(m0, md, n, n1, entries -- str)]) = links(entries[str], dirs) -- mklink(p_ino, str) | A User Theorem |
| links-dirs-union | ⊦ dirs0 ⊥ dirs1 → links(ino, dirs0 ∪ dirs1) = links(ino, dirs0) ∪ links(ino, dirs1) | A User Theorem |
| links-inc-nsubdirs | ⊦ p_ino ∈ dirs → links(ino, dirs[p_ino, mkdir(m0, md, n0, n1 + 1, entries)]) = links(ino, dirs[p_ino, mkdir(m0, md, n0, n1, entries)]) | A User Theorem |
| links-modmeta | ⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(m0, md0, n1, n2, entries) → links(ino0, dirs[ino, mkdir(m, md, n, n0, entries)]) = links(ino0, dirs) | A User Theorem |
| links-modmeta-write2 | ⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(m0, md0, n1, n2, entries) ∧ ino ≠ ino1 → links(ino0, dirs[ino1, ad][ino, mkdir(m, md, n, n0, entries)]) = links(ino0, dirs[ino1, ad]) | A User Theorem |
| links-modmeta-write3 | ⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(m0, md0, n1, n2, entries) ∧ ino ≠ ino1 ∧ ino ≠ ino2 → links(ino0, dirs[ino1, ad][ino2, ad0][ino, mkdir(m, md, n, n0, entries)]) = links(ino0, dirs[ino1, ad][ino2, ad0]) | A User Theorem |
| links-nonempty | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries → links(entries[str], dirs) ≠ ∅ | A User Theorem |
| links-put-same-entries | ⊦ ino ∈ dirs ∧ dirs[ino].entries = entries → links(ino0, dirs[ino, mkdir(m, md, n0, n1, entries)]) = links(ino0, dirs) | A User Theorem |
| links-putnew | ⊦ ¬ ino ∈ dirs ∧ ino ≠ 0 → links(ino0, (dirs ++ ino)[ino, mkdir(m, md, n, n0, ∅)]) = links(ino0, dirs) | A User Theorem |
| links-putother | ⊦ ino0 ≠ ino ∧ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ ¬ str ∈ entries → links(ino0, dirs[p_ino, mkdir(m0, md, n, n0, entries[str, ino])]) = links(ino0, dirs) | A User Theorem |
| links-putsame | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ ¬ str ∈ entries → links(ino, dirs[p_ino, mkdir(m0, md, n, n0, entries[str, ino])]) = links(ino, dirs) ++ mklink(p_ino, str) | A User Theorem |
| lookup-dir | n ∈ dirs ⊦ lookup(ε, n, dirs, files) = n | A User Theorem |
| lookup-file | ⊦ n ∈ files → lookup(ε, n, dirs, files) = n | A User Theorem |
| max-exists | ⊦ ∃ ino. ino ≠ 0 ∧ (∀ n. n ∈ dirs ∨ n ∈ files → n < ino) | A User Theorem |
| meta-dir | ⊦ ino ∈ dirs → meta(ε, ino, dirs, files) = dirs[ino].meta | A User Theorem |
| meta-exsplit | ⊦ ispath(p, n, m, dirs, files) ∧ ispath(q, m, dirs, files) → meta(p + q, n, dirs, files) = meta(q, m, dirs, files) | A User Theorem |
| meta-file | ¬ ino ∈ dirs ⊦ ino ∈ files → meta(ε, ino, dirs, files) = files[ino].meta | A User Theorem |
| meta-path | ⊦ ispath(p, n, m, dirs, files) → meta(p, n, dirs, files) = meta(ε, m, dirs, files) | A User Theorem |
| meta-split | ⊦ ispath(p, n, m, dirs, files) ∧ ispath(q, m, m0, dirs, files) → meta(p + q, n, dirs, files) = meta(q, m, dirs, files) | A User Theorem |
| new-exists | ⊦ ∃ ino. ino ≠ 0 ∧ ¬ ino ∈ dirs ∧ ¬ ino ∈ files | A User Theorem |
| orphans-del-dir | ⊦ ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ dirs[ino] = mkdir(n, md, 0, m, ∅) ∧ afs-cons(dirs, files) → orphans(dirs -- ino, files) = orphans(dirs, files) -- ino | A User Theorem |
| orphans-del-file | ⊦ ino ∈ files ∧ files[ino] = mkfile(n, md, 0, content) ∧ afs-cons(dirs, files) → orphans(dirs, files -- ino) = orphans(dirs, files) -- ino | A User Theorem |
| path-expath-prefix | ⊦ ispath(p + q, ino, m, dirs, files) → ispath(p, ino, dirs, files) | A User Theorem |
| path-file | ⊦ n ∈ files ∧ afs-cons(dirs, files) → (ispath(p, n, m, dirs, files) ↔ n = m ∧ p = ε) | A User Theorem |
| path-in-dirs | p ≠ ε ⊦ ispath(p, n, m, dirs, files) → n ∈ dirs | A User Theorem |
| path-in-end | ⊦ ispath(p, n, m, dirs, files) ∧ ¬ m ∈ files → m ∈ dirs | A User Theorem |
| path-in-start | ⊦ ispath(p, n, m, dirs, files) ∧ ¬ n ∈ files → n ∈ dirs | A User Theorem |
| path-inj | ⊦ ispath(p, n, m0, dirs, files) ∧ ispath(p, n, m1, dirs, files) → m0 = m1 | A User Theorem |
| path-links-empty | ⊦ ispath(p, ino, n, dirs, files) → (# links(n, dirs) = 0 ↔ p = ε ∧ links(ino, dirs) = ∅) | A User Theorem |
| path-lookup | ⊦ ispath(p, n, m, dirs, files) → lookup(p, n, dirs, files) = m | A User Theorem |
| path-one | ⊦ ispath(str ', n, m, dirs, files) ↔ n ∈ dirs ∧ str ∈ dirs[n].entries ∧ (m ∈ dirs ∨ m ∈ files) ∧ dirs[n].entries[str] = m | A User Theorem |
| path-prefix | ⊦ ispath(q, n, m, dirs, files) ∧ p ⊑ q → ispath(p, n, dirs, files) | A User Theorem |
| path-split | ⊦ ispath(p + q, n, m, dirs, files) ↔ (∃ m0. ispath(p, n, m0, dirs, files) ∧ ispath(q, m0, m, dirs, files)) | A User Theorem |
| path-split-one | ⊦ ispath(p, n, m, dirs, files) ∧ dirs[m] = mkdir(n0, md, n, n1, entries) → (ispath(p + str ', n, entries[str], dirs, files) ↔ m ∈ dirs ∧ str ∈ entries ∧ (entries[str] ∈ files ∨ entries[str] ∈ dirs)) | A User Theorem |
| path-trans | ⊦ ispath(p, n0, n1, dirs, files) ∧ ispath(q, n1, n2, dirs, files) → ispath(p + q, n0, n2, dirs, files) | A User Theorem |
| path-uni | ⊦ dirs0 ⊥ dirs1 ∧ ispath(p, n0, n1, dirs0, files) → ispath(p, n0, n1, dirs0 ∪ dirs1, files) | A User Theorem |
| path-uni-com | ⊦ dirs0 ⊥ dirs1 ∧ ispath(p, n0, n1, dirs1, files) → ispath(p, n0, n1, dirs0 ∪ dirs1, files) | A User Theorem |
| root-not-orphan | ⊦ ¬ ROOT_INO ∈ orphans(dirs, files) | A User Theorem |
| subdirs-add-entry | ⊦ ino ∈ dirs → subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries[str, ino0])]) = (ino0 ∈ dirs ⊃ subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries)]) ++ str ;(str ∈ entries ∧ entries[str] ∈ dirs ⊃ subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries)]) -- str ;subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries)]) ) ) | A User Theorem |
| subdirs-alloc | ⊦ ¬ ino ∈ dirs ∧ ino ≠ 0 ∧ p_ino ∈ dirs ∧ ¬ ino ∈ dirs[p_ino].entries → subdirs(p_ino, dirs ++ ino) = subdirs(p_ino, dirs) | A User Theorem |
| subdirs-dec-size | ⊦ p_ino ∈ dirs → subdirs(ino, dirs[p_ino, mkdir(m0 - 1, md, n0, n1, entries)]) = subdirs(ino, dirs[p_ino, mkdir(m0, md, n0, n1, entries)]) | A User Theorem |
| subdirs-del | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n0, n1, entries) → subdirs(p_ino, dirs[p_ino, mkdir(m, md, n0, n2, entries -- str)]) = (str ∈ entries ∧ entries[str] ∈ dirs ⊃ subdirs(p_ino, dirs) -- str;subdirs(p_ino, dirs)) | A User Theorem |
| subdirs-del-entry | ⊦ ino ∈ dirs → subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries -- str)]) = (str ∈ entries ∧ entries[str] ∈ dirs ⊃ subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries)]) -- str ;subdirs(ino, dirs[ino, mkdir(n, md, n0, n1, entries)]) ) | A User Theorem |
| subdirs-del-mod-size | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n0, n1, entries) → subdirs(p_ino, dirs[p_ino, mkdir(m0, md, n0, n2, entries -- str)]) = (str ∈ entries ∧ entries[str] ∈ dirs ⊃ subdirs(p_ino, dirs) -- str;subdirs(p_ino, dirs)) | A User Theorem |
| subdirs-delete-orphans | ⊦ ¬ ino ∈ orphans(dirs, files) → subdirs(ino, dirs \ orphans(dirs, files)) = subdirs(ino, dirs) | A User Theorem |
| subdirs-inc-size | ⊦ p_ino ∈ dirs → subdirs(ino, dirs[p_ino, mkdir(m0 + 1, md, n0, n1, entries)]) = subdirs(ino, dirs[p_ino, mkdir(m0, md, n0, n1, entries)]) | A User Theorem |
| subdirs-modmeta | ⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(m0, md0, n1, n2, entries) → subdirs(ino0, dirs[ino, mkdir(m, md, n, n0, entries)]) = subdirs(ino0, dirs) | A User Theorem |
| subdirs-put | ⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n0, n1, entries) → subdirs(p_ino, dirs[p_ino, mkdir(m, md, n0, n1, entries[str, ino])]) = (subdirs(p_ino, dirs) \ (str ∈ entries ∧ entries[str] ∈ dirs ⊃ {str} ;∅)) ∪ (ino ∈ dirs ⊃ {str} ;∅) | A User Theorem |
| subdirs-putother | ⊦ ino0 ≠ ino1 → subdirs(ino0, dirs[ino1, ad]) = subdirs(ino0, dirs) | A User Theorem |
| subdirs-write | ⊦ subdirs(ino, dirs[ino0, ad0][ino, ad]) = subdirs(ino, dirs[ino, ad]) | A User Theorem |
| upto-idem | ⊦ (content upto n) upto n = content upto n | A User Theorem |
| upto-less | ⊦ n ≤ m → (content upto m) upto n = content upto n | A User Theorem |
| upto-same | ⊦ valid-content(ino, files) ∧ ino ∈ files ∧ files[ino] = mkfile(n, md, m, content) → content upto n = content | A User Theorem |