| files0[ino2] = mkfile(m2 * VFS_PAGE_SIZE + n0, md0, # links(ino2, dirs), content0), root.dir?, m1 * VFS_PAGE_SIZE + n1 < m2 * VFS_PAGE_SIZE + n0, n0 < VFS_PAGE_SIZE, m1 * VFS_PAGE_SIZE + n1 < n, dom of < ino3, n1 < VFS_PAGE_SIZE, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files0), afs-cons(dirs, files0[ino2, mkfile(n, md0, # links(ino2, dirs), content0 upto (n < m2 * VFS_PAGE_SIZE + n0 ⊃ n;m2 * VFS_PAGE_SIZE + n0))]), fids-cons(root, abs-files(files0), abs-of(of)), ispath(path, ROOT_INO, ino2, dirs, files0), of-cons(of, dirs, files0), of-cons(of, dirs, files0[ino2, mkfile(n, md0, # links(ino2, dirs), content0 upto (n < m2 * VFS_PAGE_SIZE + n0 ⊃ n;m2 * VFS_PAGE_SIZE + n0))]), pw(user, md0), px-parent(user, path, ROOT_INO, dirs, files0), m1 ∈ content0, ino2 ∈ files0, ROOT_INO ∈ dirs, psynced0 → asynced0 ⊦ content0[m1][n1] = (m1 * VFS_PAGE_SIZE < (n < m2 * VFS_PAGE_SIZE + n0 ⊃ n;m2 * VFS_PAGE_SIZE + n0) ⊃ content0[m1];zeropage)[n1], root[path].dir?, ino2 ∈ dirs, m2 * VFS_PAGE_SIZE + n0 ≤ n ∧ n0 ≠ 0 ∧ m2 ∈ content0 |
Used simplifier rules: ⊦ n < VFS_PAGE_SIZE → (zeropage)[n] = zero; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%transitivity: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification oelem[nat-set]% ⊦ m +1 = m + 1; (s)% ⊦ n0 < m0 → (m0 * m + n0 < m0 * n ↔ m < n); (s)% ⊦ ¬ n < n; (s)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ m ≤ n → (n < m ↔ false); (s)%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ n + 0 = n; (s)