Theorem is-encoded-empbuf

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by:
• Used by units in proved state: abs-node, abs-list,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 3
• Used lemmas:
• Used spec theorems:
  • encoding-fixed-size-nonempty/encoding-node-header/is-encoded-nonempty
• Used simplifier rules:
  • encoding-fixed-size-nonempty/encoding-node-header/is-encoded-size
  • eraseblock/isempty-empbuf
  • array-splice/buffer/emparray-len
  • array-splice/buffer/mkemparray-eq