| fs0[ri[key]].key = key, replay-log(log0, fs0, fi0 ⊖ fo0) = ri ⊖ ro, ro.inodes?, fo0.inodes?, file-node-cons(fs0, ri), log-cons(log0, fs0), orphans-cons(fs0, ri, ro), replay-safe(log0, fs0, fi0 ⊖ fo0), ri-closed(ri, fs0, ro), ri-inj(fi0), ri-inj(ri), ri[key] ∈ fs0, inodekey(key.ino) ∈ ro, key ∈ ri, inodekey(key.ino) ∈ ri, fo0 ⊆ dom fi0, ro ⊆ dom ri, key.inode? → fs0[ri[key]].inode? ∧ key.ino ≠ 0, key.dentry? → fs0[ri[key]].dentry?, key.data? → fs0[ri[key]].data? ⊦ # ro = 0, ro = ∅, key.data?, dups(log0), inodekey(0) ∈ ri ⊖ ro, inodekey(0) ∈ ri, key ∈ ro, (¬ fs0[ri[key]].dentry? ∧ ¬ fs0[ri[inodekey(key.ino)]].directory ∧ # fs0[ri[key]].data = VFS_PAGE_SIZE → key ∈ ri ⊖ ro → ¬ fs0[ri[key]].data?) ∧ file-node-cons(fs0, ri ⊖ ro) ∧ orphans-cons(fs0, ri ⊖ ro, ∅) |
fs0[ri[key]].key = key, replay-log(log0, fs0, fi0 ⊖ fo0) = ri ⊖ ro, fo0.inodes?, ro.inodes?, file-node-cons(fs0, ri), log-cons(log0, fs0), orphans-cons(fs0, ri, ro), replay-safe(log0, fs0, fi0 ⊖ fo0), ri-closed(ri, fs0, ro), ri-inj(ri), ri-inj(fi0), inodekey(key.ino) ∈ ri, key ∈ ri, inodekey(key.ino) ∈ ro, ri[key] ∈ fs0, ro ⊆ dom ri, fo0 ⊆ dom fi0, key.dentry? → fs0[ri[key]].dentry?, key.inode? → fs0[ri[key]].inode? ∧ key.ino ≠ 0 ⊦ # ro = 0, ro = ∅, key.data?, dups(log0), key ∈ ro, inodekey(0) ∈ ri, inodekey(0) ∈ ri ⊖ ro, (¬ fs0[ri[key]].dentry? ∧ ¬ fs0[ri[inodekey(key.ino)]].directory ∧ # fs0[ri[key]].data = VFS_PAGE_SIZE → key ∈ ri ⊖ ro → ¬ fs0[ri[key]].data?) ∧ file-node-cons(fs0, ri ⊖ ro) ∧ orphans-cons(fs0, ri ⊖ ro, ∅)