Proof step 22 from proof transitivity (previous step)

User applied rule constructor cut

And obtained the following new goals

• Proof step 23:

  key0 = inodekey(ino1), key0 < key1, key1.ino ≤ ino, ino < key0.ino ∨ key0.data? ∧ ino = key0.ino ∧ ino0 < key0.part ⊦ key1.data? ∧ ino = key1.ino ∧ ino0 < key1.part

• Proof step 26:

  key0 = datakey(ino1, ino2), key0 < key1, key1.ino ≤ ino, ino < key0.ino ∨ key0.data? ∧ ino = key0.ino ∧ ino0 < key0.part ⊦ key1.data? ∧ ino = key1.ino ∧ ino0 < key1.part

• Proof step 30:

  key0 = dentrykey(ino1, str), key0 < key1, key1.ino ≤ ino, ino < key0.ino ∨ key0.data? ∧ ino = key0.ino ∧ ino0 < key0.part ⊦ key1.data? ∧ ino = key1.ino ∧ ino0 < key1.part

Rule argument

Additional information

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