Proof step 142 from proof replayone-prog (previous step)

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: elim-inode: ⊦ key.inode? ↔ (∃ ino. key = inodekey(ino));%elim-dentry: ⊦ key.dentry? ↔ (∃ ino, str. key = dentrykey(ino, str));%elim-data: ⊦ key.data? ↔ (∃ ino, n. key = datakey(ino, n));%elim-inode: ⊦ key.inode? ↔ (∃ ino. key = inodekey(ino));%node freely generated by inodenode, dentrynode, datanode, truncnode;;% ⊦ replay-one(adr, truncnode(key, n), ri) = ri \ datakeys(key, n, ri); (s)% ⊦ truncnode(key, m).key = key; (s)% ⊦ node-cons(key0, truncnode(key1, n)) ↔ key0.inode?; (s)% ⊦ ¬ truncnode(key, m).data?; (s)% ⊦ ¬ truncnode(key, m).dentry?; (s)% ⊦ ¬ truncnode(key, m).inode?; (s)% ⊦ truncnode(key, m).trunc?; (s)%⊦ replay-one(adr, datanode(key, buf), ri) = (inodekey(key.ino) ∈ ri ⊃ ri[key, adr];ri); (s)% ⊦ datanode(key, buf).key = key; (s)% ⊦ node-cons(key0, datanode(key1, buf)) ↔ key0.data?; (s)% ⊦ datanode(key, buf).data?; (s)%⊦ replay-one(adr, dentrynode(key, ino), ri) = (ino ≠ 0 ⊃ ri[key, adr];ri -- key); (s)% ⊦ dentrynode(key, m).key = key; (s)% ⊦ node-cons(key0, dentrynode(key1, ino)) ↔ key0.dentry?; (s)% ⊦ ¬ dentrynode(key, m).data?; (s)% ⊦ dentrynode(key, m).dentry?; (s)%⊦ replay-one(adr, inodenode(key, md, boolvar, n, n0, m), ri) = (n ≠ 0 ∨ key.ino = ROOT_INO ⊃ ri[key, adr] ;(boolvar ⊃ ri -- key;ri ⊖ key) ); (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).key = key; (s)%⊦ node-cons(key0, inodenode(key1, md, boolvar, n, n0, m)) ↔ key0.inode? ∧ key0.ino ≠ 0; (s)% ⊦ ¬ inodenode(key, md, boolvar, m, m0, m1).data?; (s)% ⊦ ¬ inodenode(key, md, boolvar, m, m0, m1).dentry?; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).inode?; (s)