Proof step 7 from proof transitivity (previous step)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  key0 = inodekey(ino0), key0 < key1, key1.ino ≤ ino, ino < key0.ino ∨ ¬ key0.inode? ∧ ino = key0.ino ⊦ ¬ key1.inode? ∧ ino = key1.ino

• Proof step 11:

  key0 = datakey(ino0, ino1), key0 < key1, key1.ino ≤ ino, ino < key0.ino ∨ ¬ key0.inode? ∧ ino = key0.ino ⊦ ¬ key1.inode? ∧ ino = key1.ino

• Proof step 15:

  key0 = dentrykey(ino0, str), key0 < key1, key1.ino ≤ ino, ino < key0.ino ∨ ¬ key0.inode? ∧ ino = key0.ino ⊦ ¬ key1.inode? ∧ ino = key1.ino

Rule argument

Additional information

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