Proof step 5 from proof key-node-cons (previous step)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  key = inodekey(ino), key-cons(key, nd) ⊦ (nd.inode? → key.inode? ∧ key.ino ≠ 0) ∧ (nd.dentry? → key.dentry?) ∧ (nd.data? → key.data?) ∧ (nd.trunc? → key.inode?)

• Proof step 8:

  key = datakey(ino, ino0), key-cons(key, nd) ⊦ (nd.inode? → key.inode? ∧ key.ino ≠ 0) ∧ (nd.dentry? → key.dentry?) ∧ (nd.data? → key.data?) ∧ (nd.trunc? → key.inode?)

• Proof step 10:

  key = dentrykey(ino, str), key-cons(key, nd) ⊦ (nd.inode? → key.inode? ∧ key.ino ≠ 0) ∧ (nd.dentry? → key.dentry?) ∧ (nd.data? → key.data?) ∧ (nd.trunc? → key.inode?)

Rule argument

Additional information

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