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

fs1[ri1[key]].key = key, log-cons(log1, fs1), ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0), key ∈ ri1, ri1[key] ∈ fs1, fo1 ⊆ dom fi1, ro1 ⊆ dom ri1, key.data? → fs1[ri1[key]].data?, key.dentry? → fs1[ri1[key]].dentry?, key.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0, 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, ∀ adr. ( adr ∈ log0 → (fs0[adr].inode? → fs0[adr].key.inode? ∧ fs0[adr].key.ino ≠ 0) ∧ (fs0[adr].dentry? → fs0[adr].key.dentry?) ∧ (fs0[adr].data? → fs0[adr].key.data?) ∧ (fs0[adr].trunc? → fs0[adr].key.inode?)) → adr ∈ log1 → adr ∈ fs1 ∧ (fs1[adr].inode? → fs1[adr].key.inode? ∧ fs1[adr].key.ino ≠ 0) ∧ (fs1[adr].dentry? → fs1[adr].key.dentry?) ∧ (fs1[adr].data? → fs1[adr].key.data?) ∧ (fs1[adr].trunc? → fs1[adr].key.inode?), ∀ key. key ∈ fo1 → key ∈ fi1, ∀ key. key ∈ ro1 → key ∈ ri1, ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ key-cons(key, fs1[ri1[key]]) ⊦ inodekey(0) ∈ ri1, ( 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)

User applied rule constructor cut

And obtained the following new goals

Proof step 86:
fs1[ri1[key]].key = key, key = inodekey(pageno), log-cons(log1, fs1), ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0), ri1[key] ∈ fs1, key ∈ ri1, ro1 ⊆ dom ri1, fo1 ⊆ dom fi1, key.data? → fs1[ri1[key]].data? ∧ inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE, 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.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0, key.dentry? → fs1[ri1[key]].dentry?, key.data? → fs1[ri1[key]].data?, ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ key-cons(key, fs1[ri1[key]]), ∀ key. key ∈ ro1 → key ∈ ri1, ∀ key. key ∈ fo1 → key ∈ fi1, ∀ adr. ( adr ∈ log0 → (fs0[adr].inode? → fs0[adr].key.inode? ∧ fs0[adr].key.ino ≠ 0) ∧ (fs0[adr].dentry? → fs0[adr].key.dentry?) ∧ (fs0[adr].data? → fs0[adr].key.data?) ∧ (fs0[adr].trunc? → fs0[adr].key.inode?)) → adr ∈ log1 → adr ∈ fs1 ∧ (fs1[adr].inode? → fs1[adr].key.inode? ∧ fs1[adr].key.ino ≠ 0) ∧ (fs1[adr].dentry? → fs1[adr].key.dentry?) ∧ (fs1[adr].data? → fs1[adr].key.data?) ∧ (fs1[adr].trunc? → fs1[adr].key.inode?) ⊦ inodekey(0) ∈ ri1, ( 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)
Proof step 88:
fs1[ri1[key]].key = key, key = datakey(pageno, pageno0), log-cons(log1, fs1), ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0), ri1[key] ∈ fs1, key ∈ ri1, ro1 ⊆ dom ri1, fo1 ⊆ dom fi1, key.data? → fs1[ri1[key]].data? ∧ inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE, 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.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0, key.dentry? → fs1[ri1[key]].dentry?, key.data? → fs1[ri1[key]].data?, ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ key-cons(key, fs1[ri1[key]]), ∀ key. key ∈ ro1 → key ∈ ri1, ∀ key. key ∈ fo1 → key ∈ fi1, ∀ adr. ( adr ∈ log0 → (fs0[adr].inode? → fs0[adr].key.inode? ∧ fs0[adr].key.ino ≠ 0) ∧ (fs0[adr].dentry? → fs0[adr].key.dentry?) ∧ (fs0[adr].data? → fs0[adr].key.data?) ∧ (fs0[adr].trunc? → fs0[adr].key.inode?)) → adr ∈ log1 → adr ∈ fs1 ∧ (fs1[adr].inode? → fs1[adr].key.inode? ∧ fs1[adr].key.ino ≠ 0) ∧ (fs1[adr].dentry? → fs1[adr].key.dentry?) ∧ (fs1[adr].data? → fs1[adr].key.data?) ∧ (fs1[adr].trunc? → fs1[adr].key.inode?) ⊦ inodekey(0) ∈ ri1, ( 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)
Proof step 90:
fs1[ri1[key]].key = key, key = dentrykey(pageno, str), log-cons(log1, fs1), ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0), ri1[key] ∈ fs1, key ∈ ri1, ro1 ⊆ dom ri1, fo1 ⊆ dom fi1, key.data? → fs1[ri1[key]].data? ∧ inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE, 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.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0, key.dentry? → fs1[ri1[key]].dentry?, key.data? → fs1[ri1[key]].data?, ∀ key. key ∈ ri1 → ri1[key] ∈ fs1 ∧ key-cons(key, fs1[ri1[key]]), ∀ key. key ∈ ro1 → key ∈ ri1, ∀ key. key ∈ fo1 → key ∈ fi1, ∀ adr. ( adr ∈ log0 → (fs0[adr].inode? → fs0[adr].key.inode? ∧ fs0[adr].key.ino ≠ 0) ∧ (fs0[adr].dentry? → fs0[adr].key.dentry?) ∧ (fs0[adr].data? → fs0[adr].key.data?) ∧ (fs0[adr].trunc? → fs0[adr].key.inode?)) → adr ∈ log1 → adr ∈ fs1 ∧ (fs1[adr].inode? → fs1[adr].key.inode? ∧ fs1[adr].key.ino ≠ 0) ∧ (fs1[adr].dentry? → fs1[adr].key.dentry?) ∧ (fs1[adr].data? → fs1[adr].key.data?) ∧ (fs1[adr].trunc? → fs1[adr].key.inode?) ⊦ inodekey(0) ∈ ri1, ( 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)

Rule argument

var: key

Additional information

Used simplifier rules: key freely generated by inodekey, datakey, dentrykey;;