Used simplifier rules/spec theorems by specification

Used from specification list-last

• list-last/lapp is used by fw-frag,
• list-last/l-06 is used by weak-lemma_3-15, lemma_3-15,
• list-last/last-01 is used by weakbwsim-implies-bwsiminv-aux,
• list-last/last-def is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
• list-last/last-elim is used by fw-frag,
• list-last/last-one is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• list-last/last-rec is used by weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,

Used from specification nat

• nat/elim-sub is used by fw-frag,
• nat/le-def is used by fw-frag,
• nat/lels is used by fw-frag,
• nat/lep is used by fw-frag,
• nat/succ-01 is used by fw-frag,

Used from specification remtau

• remtau/finremtau-append is used by weak-lemma_3-15, lemma_3-15, fw-frag,
• remtau/finremtau-def is used by weakbwsim-implies-bwsiminv-aux,
• remtau/finremtau-empty is used by weak-lemma_3-15, lemma_3-15, fw-frag,
• remtau/finremtau-one is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-trans-aux, fw-frag, bwsiminv-implies-weakbwsim-aux, bwsim-bwsiminv-aux,

Used from specification list-getput

• list-getput/get-zero-01 is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, fw-frag,

Used from specification nat-basic

• nat-basic/a is used by fw-frag,
• nat-basic/add-base is used by fw-frag,
• nat-basic/c is used by fw-frag,
• nat-basic/eq-01 is used by fw-frag,
• nat-basic/eq-inc-neq is used by fw-frag,
• nat-basic/f is used by fw-frag,
• nat-basic/l-02 is used by fw-frag,
• nat-basic/lf-01 is used by fw-frag,
• nat-basic/lf-02 is used by fw-frag,
• nat-basic/s-04 is used by fw-frag,
• nat-basic/succ is used by fw-frag,
• nat-basic/zero is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, fw-frag,

Used from specification list

• list/Last is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
• list/a is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• list/app is used by weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• list/app-02 is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag,
• list/c is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• list/c-03 is used by weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• list/c-08 is used by fw-frag, bwsiminv-implies-weakbwsim-aux,
• list/e is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag,
• list/in-14 is used by fw-frag,
• list/in-15 is used by fw-frag,
• list/in-17 is used by fw-frag,
• list/in-append is used by fw-frag,
• list/in-append0-not-left is used by fw-frag,
• list/in-rec is used by fw-frag,
• list/inapp-08 is used by fw-frag,
• list/len is used by fw-frag,
• list/len-02 is used by fw-frag,
• list/len-05 is used by fw-frag,
• list/len-06 is used by fw-frag,
• list/ni is used by fw-frag,

Used from specification IOtrace

• IOtrace/finfrag-rec is used by weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• IOtrace/finfrag-rec-end is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
• IOtrace/finfrag-split is used by fw-frag,
• IOtrace/fragstar is used by fw-frag,
• IOtrace/move is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-trans-aux, fw-frag,
• IOtrace/move-trans is used by weak-lemma_3-15, lemma_3-15,
• IOtrace/finexec is used by weakbwsim-implies-bwsiminv-aux, weakbwsim-implies-bwsiminv, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
• IOtrace/finfrag-one is used by weakbwsim-implies-bwsiminv-aux, fw-frag,
• IOtrace/finfrag-onlyone is used by weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• IOtrace/fragfin-size-02 is used by fw-frag,
• IOtrace/fragfin-size-le1 is used by fw-frag,
• IOtrace/fragfin-size-ls-02 is used by fw-frag,
• IOtrace/fragfin-size-notls is used by fw-frag,
• IOtrace/fragstar-onestate is used by fw-frag,
• IOtrace/move-empty is used by weak-lemma_3-15, lemma_3-15,
• IOtrace/not-finfrag-empty is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,

Used from specification stream

• stream/append-from-le is used by fw-frag,
• stream/fin-finlen-tolen is used by fw-frag,
• stream/append-assoc is used by bwsiminv-implies-weakbwsim-aux,
• stream/append-finfin is used by bwsiminv-implies-weakbwsim-aux,
• stream/append-from-size is used by fw-frag,
• stream/hd-fin-lem is used by bwsiminv-implies-weakbwsim-aux,
• stream/to-succ-cons-l-lem is used by fw-frag,

Used from specification IO-Aut-data

• IO-Aut-data/sel-IOAut-dotext is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-trans-aux, fw-frag,
• IO-Aut-data/sel-IOAut-dotstart is used by weakbwsim-implies-bwsiminv-aux, weakbwsim-implies-bwsiminv, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,

Used from specification stream-basic

• stream-basic/sel-rqui-dotl is used by weakbwsim-implies-bwsiminv-aux,

Used from specification list-data

• list-data/elim-add is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, fw-frag,
• list-data/elim-list-c is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag,
• list-data/l is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, fw-frag,
• list-data/size-nil is used by fw-frag,

Used from specification list-del

• list-del/get-append-less is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, fw-frag,
• list-del/rest-app is used by fw-frag,
• list-del/firstN-len is used by fw-frag,
• list-del/get-append-grt is used by fw-frag,
• list-del/get-zero is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, lemma_3-15, fw-frag, bwsiminv-implies-weakbwsim-aux,
• list-del/one-03 is used by weakbwsim-implies-bwsiminv-aux, fw-frag,
• list-del/restN-zero is used by fw-frag,
• list-del/restn-prefix is used by fw-frag,

Used from specification Unknown

• Unknown/Unknown is used by fw-frag,