Proof step 24 from proof afs-cons-inode-sync (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  dirs[ino] = mkdir(m2, md1, m3, m4, entries), files[ino] = mkfile(m0, md0, m1, content), afs-cons(dirs, files), m ∈ dirs, ROOT_INO ∈ dirs, ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → entries = ∅, ino ∈ files → ¬ ino ∈ dirs ∧ m1 = # links(ino, dirs), ino ∈ dirs ∧ name ∈ entries → entries[name] ∈ dirs ∨ entries[name] ∈ files, ino ∈ dirs → m3 = # links(ino, dirs) ∧ # links(ino, dirs) ≤ 1 ∧ m2 = # entries ∧ m4 = # subdirs(ino, dirs) ⊦ ( ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs[m, dirs[m].meta:= md]) = ∅ → (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).entries = ∅) ∧ ( ino ∈ dirs → (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).nlink = # links(ino, dirs[m, dirs[m].meta:= md]) ∧ (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).nlink ≤ 1 ∧ (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).size = # (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).entries ∧ (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).nsubdirs = # subdirs(ino, dirs[m, dirs[m].meta:= md])) ∧ (ino ∈ files → ¬ ino ∈ dirs ∧ m1 = # links(ino, dirs[m, dirs[m].meta:= md])) ∧ ( ino ∈ dirs ∧ name ∈ (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).entries → (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).entries[name] ∈ dirs ∨ (ino = m ⊃ dirs[m].meta:= md;mkdir(m2, md1, m3, m4, entries)).entries[name] ∈ files)

Rule argument

Additional information