Proof step 35 from proof inv-open (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  ⊦ of-cons(of0, dirs0, files0) → (of-cons(of1, dirs1, files1) ↔ (∀ n. (n ∈ of0 → of0[n].ino ∈ files0) → n ∈ of1 → of1[n].ino ∈ files1))

• Proof step 37:

  dom of < ino1, afs-cons(dirs, files), ispath(p, ROOT_INO, ino0, dirs, files), of-cons(of, dirs, files), px-parent(user, p, ROOT_INO, dirs, files), n ∈ of[ino1, mkfile(ino0, mode, 0)], n ∈ of, of[n].ino ∈ files, ino0 ∈ files ⊦ of[ino1, mkfile(ino0, mode, 0)][n].ino ∈ files, ino0 ∈ dirs, (mode = MODE_W ∨ mode = MODE_RW) ∧ ¬ pw(user, files[ino0].meta), (mode = MODE_R ∨ mode = MODE_RW) ∧ ¬ pr(user, files[ino0].meta)

Rule argument

Additional information

Used simplifier rules: of-cons-reduce: ⊦ of-cons(of0, dirs0, files0) → ( of-cons(of1, dirs1, files1) ↔ (∀ n. (n ∈ of0 → of0[n].ino ∈ files0) → n ∈ of1 → of1[n].ino ∈ files1));% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)%path-in-end: ⊦ ispath(p, n, m, dirs, files) ∧ ¬ m ∈ files → m ∈ dirs; (forward) from specification afs-base% ⊦ mkfile(m, mode, m0).ino = m; (s)% ⊦ fd = fd0 → of[fd0, file][fd] = file; (s)% ⊦ fd ∈ of[fd0, file] ↔ fd = fd0 ∨ fd ∈ of; (ws)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ ns < n → ns < n + 1; (s)% ⊦ ns ++ n < n + 1 ↔ ns < n + 1; (s)% ⊦ dom of[fd, file] = dom of ++ fd; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)% ⊦ pre-iget(ino, dirs, files) ↔ valid-ino(ino, dirs, files); (s)%⊦ 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) ); (s)