Theorem get-append-notls

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: contractinf-from1, contractinf-tl, from-append-add, from-append-tofrom, swap-to-from-app, to-append-add,
• Used by units in proved state: stut-mon, mon-lim-filter-count, streamseq-mon-lim,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 3
• Proof steps: 8
• Used lemmas: size-inf, append-inf, append-fininf, sel-inf, sel-fin, append-assoc, get-append2-fin, size-fin,
• Used spec theorems:
  • Used simplifier rules:
    • nat-inf/less-inf2
    • nat/lels
    • nat-inf/less-fin
    • nat-inf-basic/sel
    • nat/elim-sub
    • nat/lep
    • list-del/get-append-grt-02
    • list/a
    • nat-basic2/l-02
    • nat-basic2/a
    • nat-basic2/c
    • nat/eq-01