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

fs1[ri1[key]].key = key, fo1.inodes?, ro1.inodes?, log-cons(log1, fs1), ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0), key ∈ ri1, ri1[key] ∈ fs1, fo1 ⊆ dom fi1, ro1 ⊆ dom ri1, inodekey(key.ino) ∈ ri1 → ri1[inodekey(key.ino)] ∈ fs1 ∧ fs1[ri1[inodekey(key.ino)]].inode? ∧ fs1[ri1[inodekey(key.ino)]].key = inodekey(key.ino) ∧ key.ino ≠ 0, inodekey(fs1[ri1[key]].ino) ∈ ri1 → ri1[inodekey(fs1[ri1[key]].ino)] ∈ fs1 ∧ node-closed(fs1[ri1[inodekey(fs1[ri1[key]].ino)]], ri1, fs1, ro1), key.data? → fs1[ri1[key]].data?, key.dentry? → fs1[ri1[key]].dentry?, key.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0, key ∈ ri0 → ri0[key] ∈ fs0 ∧ fs0[ri0[key]].key = key ∧ (key.inode? → fs0[ri0[key]].inode? ∧ key.ino ≠ 0) ∧ ( key.dentry? → fs0[ri0[key]].dentry? ∧ inodekey(key.ino) ∈ ri0 ∧ inodekey(fs0[ri0[key]].ino) ∈ ri0 ∧ ¬ inodekey(key.ino) ∈ ro0 ∧ ¬ inodekey(fs0[ri0[key]].ino) ∈ ro0 ∧ fs0[ri0[inodekey(key.ino)]].directory) ∧ (key.data? → fs0[ri0[key]].data? ∧ inodekey(key.ino) ∈ ri0 ∧ ¬ fs0[ri0[inodekey(key.ino)]].directory ∧ # fs0[ri0[key]].data = VFS_PAGE_SIZE), fs1[ri1[key]].dentry? → inodekey(key.ino) ∈ ri1 ∧ ¬ inodekey(key.ino) ∈ ro1 ∧ fs1[ri1[inodekey(key.ino)]].directory ∧ inodekey(fs1[ri1[key]].ino) ∈ ri1 ∧ ¬ inodekey(fs1[ri1[key]].ino) ∈ ro1, fs1[ri1[key]].data? → inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE, inodekey(key.ino) ∈ ri1 → ri1[inodekey(key.ino)] ∈ fs1 ∧ node-closed(fs1[ri1[inodekey(key.ino)]], ri1, fs1, ro1), inodekey(fs1[ri1[key]].ino) ∈ ri1 → ri1[inodekey(fs1[ri1[key]].ino)] ∈ fs1 ∧ key-cons(inodekey(fs1[ri1[key]].ino), fs1[ri1[inodekey(fs1[ri1[key]].ino)]]), ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ node-closed(fs1[ri1[key]], ri1, fs1, ro1), ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ key-cons(key, fs1[ri1[key]]) ⊦ dups(log1), inodekey(0) ∈ ri1, ( key.dentry? → fs1[ri1[key]].dentry? ∧ inodekey(key.ino) ∈ ri1 ∧ inodekey(fs1[ri1[key]].ino) ∈ ri1 ∧ ¬ inodekey(key.ino) ∈ ro1 ∧ ¬ inodekey(fs1[ri1[key]].ino) ∈ ro1 ∧ fs1[ri1[inodekey(key.ino)]].directory) ∧ (key.data? → fs1[ri1[key]].data? ∧ inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 29:
fs1[ri1[key]].key = key, ro1.inodes?, fo1.inodes?, log-cons(log1, fs1), ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0), ri1[key] ∈ fs1, key ∈ ri1, ro1 ⊆ dom ri1, fo1 ⊆ dom fi1, inodekey(key.ino) ∈ ri1 → ri1[inodekey(key.ino)] ∈ fs1 ∧ node-closed(fs1[ri1[inodekey(key.ino)]], ri1, fs1, ro1), fs1[ri1[key]].data? → inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE, fs1[ri1[key]].dentry? → inodekey(key.ino) ∈ ri1 ∧ ¬ inodekey(key.ino) ∈ ro1 ∧ fs1[ri1[inodekey(key.ino)]].directory ∧ inodekey(fs1[ri1[key]].ino) ∈ ri1 ∧ ¬ inodekey(fs1[ri1[key]].ino) ∈ ro1, key ∈ ri0 → ri0[key] ∈ fs0 ∧ fs0[ri0[key]].key = key ∧ (key.inode? → fs0[ri0[key]].inode? ∧ key.ino ≠ 0) ∧ ( key.dentry? → fs0[ri0[key]].dentry? ∧ inodekey(key.ino) ∈ ri0 ∧ inodekey(fs0[ri0[key]].ino) ∈ ri0 ∧ ¬ inodekey(key.ino) ∈ ro0 ∧ ¬ inodekey(fs0[ri0[key]].ino) ∈ ro0 ∧ fs0[ri0[inodekey(key.ino)]].directory) ∧ (key.data? → fs0[ri0[key]].data? ∧ inodekey(key.ino) ∈ ri0 ∧ ¬ fs0[ri0[inodekey(key.ino)]].directory ∧ # fs0[ri0[key]].data = VFS_PAGE_SIZE), key.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0, key.dentry? → fs1[ri1[key]].dentry?, key.data? → fs1[ri1[key]].data?, inodekey(fs1[ri1[key]].ino) ∈ ri1 → ri1[inodekey(fs1[ri1[key]].ino)] ∈ fs1 ∧ node-closed(fs1[ri1[inodekey(fs1[ri1[key]].ino)]], ri1, fs1, ro1), inodekey(key.ino) ∈ ri1 → ri1[inodekey(key.ino)] ∈ fs1 ∧ fs1[ri1[inodekey(key.ino)]].inode? ∧ fs1[ri1[inodekey(key.ino)]].key = inodekey(key.ino) ∧ key.ino ≠ 0, inodekey(fs1[ri1[key]].ino) ∈ ri1 → ri1[inodekey(fs1[ri1[key]].ino)] ∈ fs1 ∧ fs1[ri1[inodekey(fs1[ri1[key]].ino)]].inode? ∧ fs1[ri1[inodekey(fs1[ri1[key]].ino)]].key = inodekey(fs1[ri1[key]].ino) ∧ fs1[ri1[key]].ino ≠ 0, ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ key-cons(key, fs1[ri1[key]]), ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ node-closed(fs1[ri1[key]], ri1, fs1, ro1) ⊦ dups(log1), inodekey(0) ∈ ri1, ( key.dentry? → fs1[ri1[key]].dentry? ∧ inodekey(key.ino) ∈ ri1 ∧ inodekey(fs1[ri1[key]].ino) ∈ ri1 ∧ ¬ inodekey(key.ino) ∈ ro1 ∧ ¬ inodekey(fs1[ri1[key]].ino) ∈ ro1 ∧ fs1[ri1[inodekey(key.ino)]].directory) ∧ (key.data? → fs1[ri1[key]].data? ∧ inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE)

Rule argument

Additional information

Used simplifier rules: ⊦ key-cons(inodekey(ino), nd) ↔ nd.inode? ∧ nd.key = inodekey(ino) ∧ ino ≠ 0; (s)