[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 1355 from proof refine-truncate (previous step)

fs0[ri0[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))] = abs-files (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2])), abs-dirs(fs0, ri0) = abs-dirs(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]), orphans(fs0, ri0).inodes?, fo.inodes?, afs-cons(abs-dirs(fs0, ri0), abs-files(fs0, ri0)), afs-cons(abs-dirs(fs0, ri0), abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))]), file-node-cons (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2])), file-node-cons(fs0, ri0), log-cons(log0, fs0), orphans-cons (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2]), orphans(fs0, ri0)), orphans-cons(fs0, ri0, orphans(fs0, ri0)), replay-cons-strong (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), replay-cons-strong(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), ri-inj(ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2])), ri-inj(ri0), ri-inj(fi), ubifs-cons (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), ubifs-cons(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), ri0[inodekey(m)] ∈ fs0, inodekey(m) ∈ ri0, asynced0 → boolvar0, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ adr1 = adr2, m = 0, orphans (abs-dirs(fs0, ri0), abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2])) = abs-keys(orphans(fs0, ri0)), afs-cons (abs-dirs(fs0, ri0), abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2])), adr1 ∈ fs0, adr2 ∈ fs0, m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0, m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ (datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri0 ∨ buf-opt0.some?)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 1356:
⊦ afs-cons(dirs0, files0) → ( afs-cons(dirs1, files1) ↔ (∀ ino, name, n. ROOT_INO ∈ dirs0 ∧ (ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → dir-empty(ino, dirs0, files0)) ∧ ( ino ∈ dirs0 → ¬ ino ∈ files0 ∧ dirs0[ino].nlink = # links(ino, dirs0) ∧ dirs0[ino].nlink ≤ 1 ∧ dirs0[ino].size = # dirs0[ino].entries ∧ dirs0[ino].nsubdirs = # subdirs(ino, dirs0)) ∧ (ino ∈ files0 → ¬ ino ∈ dirs0 ∧ files0[ino].nlink = # links(ino, dirs0)) ∧ (ino ∈ dirs0 ∧ name ∈ dirs0[ino].entries → valid-ino(dirs0[ino].entries[name], dirs0, files0)) ∧ (ino ∈ files0 ∧ n ∈ files0[ino].content → valid-pagesize(ino, n, files0)) → ROOT_INO ∈ dirs1 ∧ (ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → dir-empty(ino, dirs1, files1)) ∧ ( ino ∈ dirs1 → ¬ ino ∈ files1 ∧ dirs1[ino].nlink = # links(ino, dirs1) ∧ dirs1[ino].nlink ≤ 1 ∧ dirs1[ino].size = # dirs1[ino].entries ∧ dirs1[ino].nsubdirs = # subdirs(ino, dirs1)) ∧ (ino ∈ files1 → ¬ ino ∈ dirs1 ∧ files1[ino].nlink = # links(ino, dirs1)) ∧ (ino ∈ dirs1 ∧ name ∈ dirs1[ino].entries → valid-ino(dirs1[ino].entries[name], dirs1, files1)) ∧ (ino ∈ files1 ∧ n ∈ files1[ino].content → valid-pagesize(ino, n, files1))))
Proof step 1357:
abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))] = abs-files (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2])), fs0[ri0[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), abs-dirs(fs0, ri0) = abs-dirs(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]), fo.inodes?, orphans(fs0, ri0).inodes?, afs-cons(abs-dirs(fs0, ri0), abs-files(fs0, ri0)), afs-cons(abs-dirs(fs0, ri0), abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))]), file-node-cons(fs0, ri0), file-node-cons (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2])), log-cons(log0, fs0), orphans-cons(fs0, ri0, orphans(fs0, ri0)), orphans-cons (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2]), orphans(fs0, ri0)), replay-cons-strong(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), replay-cons-strong (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), ri-inj(fi), ri-inj(ri0), ri-inj(ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2])), ubifs-cons(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), ubifs-cons (fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), min(n0, m2), ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), inodekey(m) ∈ ri0, ri0[inodekey(m)] ∈ fs0, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE, asynced0 → boolvar0 ⊦ adr1 = adr2, m = 0, orphans (abs-dirs(fs0, ri0), abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2])) = abs-keys(orphans(fs0, ri0)), adr2 ∈ fs0, adr1 ∈ fs0, ∀ ino, name, n. ROOT_INO ∈ abs-dirs(fs0, ri0) ∧ ( ino ∈ abs-dirs(fs0, ri0) ∧ ino ≠ ROOT_INO ∧ links(ino, abs-dirs(fs0, ri0)) = ∅ → dir-empty(ino, abs-dirs(fs0, ri0), abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))])) ∧ ( ino ∈ abs-dirs(fs0, ri0) → ¬ ino ∈ abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))] ∧ abs-dirs(fs0, ri0)[ino].nlink = # links(ino, abs-dirs(fs0, ri0)) ∧ abs-dirs(fs0, ri0)[ino].nlink ≤ 1 ∧ abs-dirs(fs0, ri0)[ino].size = # abs-dirs(fs0, ri0)[ino].entries ∧ abs-dirs(fs0, ri0)[ino].nsubdirs = # subdirs(ino, abs-dirs(fs0, ri0))) ∧ ( ino ∈ abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))] → ¬ ino ∈ abs-dirs(fs0, ri0) ∧ abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))][ino].nlink = # links(ino, abs-dirs(fs0, ri0))) ∧ ( ino ∈ abs-dirs(fs0, ri0) ∧ name ∈ abs-dirs(fs0, ri0)[ino].entries → valid-ino (abs-dirs(fs0, ri0)[ino].entries[name], abs-dirs(fs0, ri0), abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))])) ∧ ( ino ∈ abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))] ∧ n ∈ abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))][ino].content → valid-pagesize(ino, n, abs-files(fs0, ri0)[m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2))])) → ROOT_INO ∈ abs-dirs(fs0, ri0) ∧ ( ino ∈ abs-dirs(fs0, ri0) ∧ ino ≠ ROOT_INO ∧ links(ino, abs-dirs(fs0, ri0)) = ∅ → dir-empty (ino, abs-dirs(fs0, ri0), abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]))) ∧ ( ino ∈ abs-dirs(fs0, ri0) → ¬ ino ∈ abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]) ∧ abs-dirs(fs0, ri0)[ino].nlink = # links(ino, abs-dirs(fs0, ri0)) ∧ abs-dirs(fs0, ri0)[ino].nlink ≤ 1 ∧ abs-dirs(fs0, ri0)[ino].size = # abs-dirs(fs0, ri0)[ino].entries ∧ abs-dirs(fs0, ri0)[ino].nsubdirs = # subdirs(ino, abs-dirs(fs0, ri0))) ∧ ( ino ∈ abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]) → ¬ ino ∈ abs-dirs(fs0, ri0) ∧ abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]) [ino ] .nlink = # links(ino, abs-dirs(fs0, ri0))) ∧ ( ino ∈ abs-dirs(fs0, ri0) ∧ name ∈ abs-dirs(fs0, ri0)[ino].entries → valid-ino (abs-dirs(fs0, ri0)[ino].entries[name], abs-dirs(fs0, ri0), abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]))) ∧ ( ino ∈ abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]) ∧ n ∈ abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]) [ino ] .content → valid-pagesize (ino, n, abs-files(fs0[adr1, truncnode(inodekey(m), min(n0, m2))][adr2, inodenode(inodekey(m), md, false, m0, 0, n0)], ri0[inodekey(m), adr2]))), m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ (datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri0 ∨ buf-opt0.some?), m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0

Rule argument

spec: afs-asm name: afs-cons-reduce seq: ⊦ afs-cons(dirs0, files0) → ( afs-cons(dirs1, files1) ↔ (∀ ino, name, n. ROOT_INO ∈ dirs0 ∧ ( ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → dir-empty(ino, dirs0, files0)) ∧ ( ino ∈ dirs0 → ¬ ino ∈ files0 ∧ dirs0[ino].nlink = # links(ino, dirs0) ∧ dirs0[ino].nlink ≤ 1 ∧ dirs0[ino].size = # dirs0[ino].entries ∧ dirs0[ino].nsubdirs = # subdirs(ino, dirs0)) ∧ ( ino ∈ files0 → ¬ ino ∈ dirs0 ∧ files0[ino].nlink = # links(ino, dirs0)) ∧ ( ino ∈ dirs0 ∧ name ∈ dirs0[ino].entries → valid-ino (dirs0[ino].entries[name], dirs0, files0)) ∧ ( ino ∈ files0 ∧ n ∈ files0[ino].content → valid-pagesize(ino, n, files0)) → ROOT_INO ∈ dirs1 ∧ ( ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → dir-empty(ino, dirs1, files1)) ∧ ( ino ∈ dirs1 → ¬ ino ∈ files1 ∧ dirs1[ino].nlink = # links(ino, dirs1) ∧ dirs1[ino].nlink ≤ 1 ∧ dirs1[ino].size = # dirs1[ino].entries ∧ dirs1[ino].nsubdirs = # subdirs(ino, dirs1)) ∧ ( ino ∈ files1 → ¬ ino ∈ dirs1 ∧ files1[ino].nlink = # links(ino, dirs1)) ∧ ( ino ∈ dirs1 ∧ name ∈ dirs1[ino].entries → valid-ino (dirs1[ino].entries[name], dirs1, files1)) ∧ ( ino ∈ files1 ∧ n ∈ files1[ino].content → valid-pagesize(ino, n, files1)))) subst: [dirs0, files0, files1, dirs1] → [abs-dirs(fs0, ri0), abs-files(fs0, ri0) [m, mkfile (n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2)) ], abs-files (fs0[adr1, truncnode(inodekey(m), min(n0, m2))] [adr2, inodenode(inodekey(m), md, false, m0, 0, n0) ], ri0[inodekey(m), adr2]), abs-dirs(fs0, ri0)] flags: <all paths>

Additional information

Used terms: abs-dirs(fs0, ri0), abs-files(fs0, ri0) [m, mkfile(n0, md, m0, abs-content(m, fs0, ri0) upto min(n0, m2)) ], abs-files (fs0[adr1, truncnode(inodekey(m), min(n0, m2))] [adr2, inodenode(inodekey(m), md, false, m0, 0, n0) ], ri0[inodekey(m), adr2]), abs-dirs(fs0, ri0)