[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 17 from proof afs-cons-reduce (previous step)

files0[ino] = mkfile(m, md, m0, content), files1[ino] = mkfile(m1, md0, m2, content0), dirs0[ino] = mkdir(m3, md1, m4, m5, entries), dirs1[ino] = mkdir(m6, md2, m7, m8, entries0), afs-cons(dirs0, files0), ROOT_INO ∈ dirs1, ROOT_INO ∈ dirs0, ino ∈ dirs0 → m4 = # links(ino, dirs0) ∧ # links(ino, dirs0) ≤ 1 ∧ m3 = # entries ∧ m5 = # subdirs(ino, dirs0), ino ∈ dirs0 ∧ name ∈ entries → entries[name] ∈ dirs0 ∨ entries[name] ∈ files0, ino ∈ files0 → ¬ ino ∈ dirs0 ∧ m0 = # links(ino, dirs0), ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → entries = ∅, ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → dirs1[ino].entries = ∅, 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), ∀ ino0. (ino0 ∈ dirs1 ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs1) = ∅ → dirs1[ino0].entries = ∅) ∧ ( ino0 ∈ dirs1 → ¬ ino0 ∈ files1 ∧ dirs1[ino0].nlink = # links(ino0, dirs1) ∧ dirs1[ino0].nlink ≤ 1 ∧ dirs1[ino0].size = # dirs1[ino0].entries ∧ dirs1[ino0].nsubdirs = # subdirs(ino0, dirs1)) ∧ (ino0 ∈ files1 → ¬ ino0 ∈ dirs1 ∧ files1[ino0].nlink = # links(ino0, dirs1)) ∧ (∀ name0. ino0 ∈ dirs1 ∧ name0 ∈ dirs1[ino0].entries → dirs1[ino0].entries[name0] ∈ dirs1 ∨ dirs1[ino0].entries[name0] ∈ files1) ∧ (∀ n. ino0 ∈ files1 ∧ n ∈ files1[ino0].content → # files1[ino0].content[n] = VFS_PAGE_SIZE), ∀ name0. ino ∈ dirs1 ∧ name0 ∈ dirs1[ino].entries → dirs1[ino].entries[name0] ∈ dirs1 ∨ dirs1[ino].entries[name0] ∈ files1, ∀ n. ino ∈ files1 ∧ n ∈ files1[ino].content → # files1[ino].content[n] = VFS_PAGE_SIZE ⊦ (ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → entries0 = ∅) ∧ (ino ∈ dirs1 → m7 = # links(ino, dirs1) ∧ # links(ino, dirs1) ≤ 1 ∧ m6 = # entries0 ∧ m8 = # subdirs(ino, dirs1)) ∧ (ino ∈ files1 → ¬ ino ∈ dirs1 ∧ m2 = # links(ino, dirs1)) ∧ (ino ∈ dirs1 ∧ name ∈ entries0 → entries0[name] ∈ dirs1 ∨ entries0[name] ∈ files1)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 18:
files0[ino] = mkfile(m, md, m0, content), files1[ino] = mkfile(m1, md0, m2, content0), dirs0[ino] = mkdir(m3, md1, m4, m5, entries), dirs1[ino] = mkdir(m6, md2, m7, m8, entries0), afs-cons(dirs0, files0), ROOT_INO ∈ dirs1, ROOT_INO ∈ dirs0, ino ∈ dirs0 → m4 = # links(ino, dirs0) ∧ # links(ino, dirs0) ≤ 1 ∧ m3 = # entries ∧ m5 = # subdirs(ino, dirs0), ino ∈ dirs0 ∧ name ∈ entries → entries[name] ∈ dirs0 ∨ entries[name] ∈ files0, ino ∈ files0 → ¬ ino ∈ dirs0 ∧ m0 = # links(ino, dirs0), ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → entries = ∅, ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → entries0 = ∅, ino ∈ dirs1 → ¬ ino ∈ files1 ∧ m7 = # links(ino, dirs1) ∧ # links(ino, dirs1) ≤ 1 ∧ m6 = # entries0 ∧ m8 = # subdirs(ino, dirs1), ino ∈ files1 → ¬ ino ∈ dirs1 ∧ m2 = # links(ino, dirs1), ∀ ino0. (ino0 ∈ dirs1 ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs1) = ∅ → dirs1[ino0].entries = ∅) ∧ ( ino0 ∈ dirs1 → ¬ ino0 ∈ files1 ∧ dirs1[ino0].nlink = # links(ino0, dirs1) ∧ dirs1[ino0].nlink ≤ 1 ∧ dirs1[ino0].size = # dirs1[ino0].entries ∧ dirs1[ino0].nsubdirs = # subdirs(ino0, dirs1)) ∧ (ino0 ∈ files1 → ¬ ino0 ∈ dirs1 ∧ files1[ino0].nlink = # links(ino0, dirs1)) ∧ (∀ name0. ino0 ∈ dirs1 ∧ name0 ∈ dirs1[ino0].entries → dirs1[ino0].entries[name0] ∈ dirs1 ∨ dirs1[ino0].entries[name0] ∈ files1) ∧ (∀ n. ino0 ∈ files1 ∧ n ∈ files1[ino0].content → # files1[ino0].content[n] = VFS_PAGE_SIZE), ∀ name0. ino ∈ dirs1 ∧ name0 ∈ entries0 → entries0[name0] ∈ dirs1 ∨ entries0[name0] ∈ files1, ∀ n. ino ∈ files1 ∧ n ∈ content0 → # content0[n] = VFS_PAGE_SIZE ⊦ (ino ∈ dirs1 → m7 = # links(ino, dirs1) ∧ # links(ino, dirs1) ≤ 1 ∧ m6 = # entries0 ∧ m8 = # subdirs(ino, dirs1)) ∧ (ino ∈ dirs1 ∧ name ∈ entries0 → entries0[name] ∈ dirs1 ∨ entries0[name] ∈ files1)

Rule argument

Additional information

Used simplifier rules: ⊦ mkfile(m, md, m0, content).content = content; (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)% ⊦ mkdir(m, md, m0, m1, entries).nsubdirs = m1; (s)% ⊦ mkdir(m, md, m0, m1, entries).size = m; (s)% ⊦ mkdir(m, md, m0, m1, entries).nlink = m0; (s)% ⊦ mkdir(m, md, m0, m1, entries).entries = entries; (s)