Theorem append-a

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: ls, s,
• Comment:
• Used by: append-at, append-eq-emptyar, append-eq-left, append-eq-right, append-inj, append-left-size0, append-prefix-left, append-right-size0, append-zero-left, append-zero-right, array-split-elim-size, array-split1, array-split2, copy-append, copy-exact-append, copy-shift-append, copy-shift-right, copy2append, copy2append0, copy2append00, fill-append-shift, fill2append, mkemparray-append, mkemparray0-append-right, range-eq-append-shift, range-eq-shift-right, same-size-append, subarray-append-consec, subarray-append-elim, subarray-append-elim-left, subarray-append-elim-left0, subarray-append-elim-left0-simp, subarray-append-left, subarray-append-left-01, subarray-append-shift-left, subarray-append-shift-right, subarray-append-shift-right-simp-0, subarray-elim, subarray-eq-elim, subarray-split-at, subarray-split-first, subarray-split-size,
• Used by units in proved state: encoding-aligned, encoding, checksum, datasize, eraseblock,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 4
• Proof steps: 11
• Used lemmas: append-atp2, append-at2, append-at1, append-len,
• Used spec theorems:
  • array/Extension
• Used simplifier rules:
  • nat-basic/eq-01
  • nat/lep-02
  • nat/le-ls-simp
  • nat-basic/l-01
  • nat/lels
  • nat/lep
  • nat-basic/a
  • nat-basic/c
  • nat-basic/l-08
  • nat-basic/l
  • nat-basic/f
  • nat/fle-01
  • nat-basic/l-02
  • nat/elim-sub