[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification list-last

list-last/lapp is used by move-trans,
list-last/l-02 is used by shortest-frag,
list-last/lapp is used by move-split, move-trans,
list-last/last-01 is used by move-split,
list-last/last-def is used by move-one,
list-last/last-elim is used by frag-trans, frag-rec-end, move-trans, infappend-moves-gen,
list-last/last-one is used by move-empty, emptymove-splitfirst,
list-last/last-rec is used by moveone-splitstep, emptymove-splitfirst,

Used from specification Unknown

Unknown/Unknown is used by move-trans,

Used from specification nat

nat/add-01 is used by move-split, preserve-INV-fin, infappend-frags, inffrag-rec, infappend-moves-gen,
nat/add-num-01 is used by move-trans,
nat/add-num-03 is used by move-trans, infappend-moves-gen,
nat/add-num-04 is used by finfrag-one-action,
nat/anti is used by frag-rec-end, infappend-frags,
nat/cancel-01 is used by frag-trans, frag-rec-end,
nat/elim-pred-c is used by inffrag-rec2, preserve-INV-fin, infappend-frags, inffrag-rec, infappend-moves-gen, frag-rec, inffrag-rec1,
nat/elim-sub is used by frag-trans, infappend-frags, move-trans, infappend-moves-gen, frag-split,
nat/eq is used by infappend-frags, fragfin-size-le,
nat/eq-01 is used by frag-trans, frag-from-1,
nat/eq-02 is used by frag-split,
nat/eqle-one is used by frag-trans, infappend-frags, move-trans, infappend-moves-gen,
nat/fle is used by frag-trans, infappend-frags, infappend-moves-gen,
nat/fle-01 is used by frag-trans, infappend-frags, infappend-moves-gen, fragfin-size-le1,
nat/le-def is used by shortest-frag, preserve-INV-fin, infappend-frags, infappend-moves-gen, frag-split, fragfin-size-le1,
nat/le-ls-simp is used by frag-to-fin, frag-rec-end, infappend-frags, infappend-moves-gen,
nat/le-one is used by frag-trans,
nat/lels is used by shortest-frag, frag-to-fin, move-split, frag-trans, frag-rec-end, infappend-frags, frag-from-1, exec-step-fin, frag-step-fin, fragfin-size-notls, move-cut-2, move-trans, infappend-moves-gen, frag-split, finfrag-split, frag-to,
nat/lels-03 is used by move-split, frag-rec-end, infappend-frags, move-trans, infappend-moves-gen, frag-split,
nat/lep is used by move-split, frag-trans, infappend-frags, frag-from-1, move-cut-2, move-trans, infappend-moves-gen, frag-split, finfrag-split,
nat/lep-02 is used by frag-trans, infappend-frags, move-trans, infappend-moves-gen,
nat/ler is used by move-split, frag-rec-end, move-trans, frag-split,
nat/les is used by frag-trans, move-trans, infappend-moves-gen,
nat/let is used by frag-trans, infappend-frags, infappend-moves-gen,
nat/lez is used by shortest-frag,
nat/ls-01 is used by preserve-INV-fin, infappend-frags, infappend-moves-gen,
nat/ls-03 is used by infappend-moves-gen,
nat/ls-add-not-01 is used by frag-step-fin, infappend-moves-gen,
nat/ls-le-simp is used by shortest-frag, frag-rec-end, infappend-frags, exec-step-fin, infappend-moves-gen, frag-split, frag-to,
nat/not-zero is used by infappend-frags,
nat/one-01 is used by move-trans,
nat/one-02 is used by move-trans,
nat/succ-01 is used by shortest-frag, move-split, infappend-frags, frag-notsizeleq, infappend-moves-gen,
nat/zero is used by move-split, frag-trans, frag-rec-end, infappend-moves-gen, frag-split,

Used from specification remtau

remtau/finremtau-one is used by moveone-splitstep,
remtau/finremtau-split-weak is used by move-split,
remtau/remtau-append is used by infappend-moves-gen,
remtau/remtau-empty-equiv is used by infappend-moves-gen,
remtau/remtau-split-list-inf is used by infappend-moves-gen,
remtau/remtau-split-list-weak is used by fintrace, infappend-moves-gen,
remtau/remtau-split-weak is used by trace-append,
remtau/remtau_of_to-to_of_rmtau is used by infappend-moves-gen,
remtau/finremtau-append is used by moveone-splitstep, emptymove-splitfirst, move-trans, infappend-moves-gen,
remtau/finremtau-def is used by inftrace, trace-append, fintrace, infappend-moves-gen,
remtau/finremtau-empty is used by move-split, move-empty, moveone-splitstep, emptymove-splitfirst, infappend-moves-gen,
remtau/finremtau-one is used by move-one, emptymove-splitfirst, infappend-moves-gen,
remtau/remtau-one is used by infappend-moves-gen,
remtau/remtau-one-02 is used by move-one-ext,
remtau/remtau-one-03 is used by moveone-splitstep,

Used from specification list-getput

list-getput/extension is used by infappend-frags, infappend-moves-gen,
list-getput/get-zero-01 is used by infappend-moves-gen,
list-getput/get-zero-01 is used by move-split, preserve-INV-fin, move-trans, infappend-moves-gen,

Used from specification nat-basic

nat-basic/a is used by allfragto-frag, shortest-frag, inffrag-rec2, exec-step-fin-2, exec-step, not-finfrag-empty, fraginf, move-split, frag-step-inf-zero, fragstar-onestate, fragfin-size-ls, preserve-INV-fin, finfrag-one, frag-step-zero, trace-append, frag-noactions, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin-zero, frag-notsizeleq, fragfin-size-le, exec-step-fin, frag-step-fin, exec-step-inf, fintrace, finfrag-two, fragfin-size-notls-02, inffrag-rec, inffrag-split, move-cut-2, move-trans, frag-size-2, move-cut, infappend-moves-gen, frag-split, frag-rec, finfrag-one-action, fragfin-size-le1, finfrag-onlyone, finfrag-split, preserve-INV, frag-to,
nat-basic/add-base is used by preserve-INV-fin, infappend-frags, inffrag-rec, infappend-moves-gen,
nat-basic/c is used by allfragto-frag, shortest-frag, inffrag-rec2, exec-step-fin-2, exec-step, not-finfrag-empty, fraginf, move-split, frag-step-inf-zero, fragstar-onestate, fragfin-size-ls, preserve-INV-fin, finfrag-one, frag-step-zero, trace-append, frag-noactions, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin-zero, frag-notsizeleq, fragfin-size-le, exec-step-fin, frag-step-fin, exec-step-inf, fintrace, finfrag-two, fragfin-size-notls-02, inffrag-rec, inffrag-split, move-cut-2, move-trans, frag-size-2, move-cut, infappend-moves-gen, frag-split, frag-rec, finfrag-one-action, fragfin-size-le1, finfrag-onlyone, finfrag-split, preserve-INV, frag-to,
nat-basic/eq-01 is used by preserve-INV-fin, frag-trans, infappend-frags, infappend-moves-gen, frag-split,
nat-basic/eq-inc-neq is used by move-trans,
nat-basic/eqs is used by infappend-frags, move-trans, infappend-moves-gen,
nat-basic/f is used by shortest-frag, move-split, fragfin-size-ls, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin, fragfin-size-notls-02, fragstar, move-trans, infappend-moves-gen, frag-split, fragfin-size-le1, frag-from-fin, finfrag-split, fragfin-size-ls1, frag-to,
nat-basic/l is used by allfragto-frag, shortest-frag, frag-trans, frag-rec-end, infappend-frags, move-trans, infappend-moves-gen, frag-split, frag-to,
nat-basic/l-01 is used by allfragto-frag, move-split, frag-trans, infappend-frags, move-trans, infappend-moves-gen, frag-split,
nat-basic/l-02 is used by move-split, fragfin-size-ls, frag-trans, infappend-frags, frag-from-1, frag-notsizeleq, move-trans, move-cut, infappend-moves-gen, frag-split, fragfin-size-le1, finfrag-split, preserve-INV,
nat-basic/l-05 is used by infappend-frags, infappend-moves-gen,
nat-basic/l-06 is used by infappend-frags, infappend-moves-gen, frag-split,
nat-basic/less-zero is used by finfrag-one, frag-noactions, move-trans,
nat-basic/lf is used by infappend-frags, move-trans, infappend-moves-gen,
nat-basic/lf-01 is used by move-split, frag-trans, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin, fragfin-size-notls-02, move-trans, infappend-moves-gen, frag-split, fragfin-size-ls1,
nat-basic/lf-02 is used by move-split, fragfin-size-ls, fragfin-size-ls-02, infappend-frags, fragfin-size-notls-02, move-trans, infappend-moves-gen, fragfin-size-ls1,
nat-basic/ls-02 is used by move-split, frag-rec-end, fragfin-size-ls-02, infappend-frags, fragfin-size-notls-02, infappend-moves-gen, frag-split, fragfin-size-ls1, frag-to,
nat-basic/neq-03 is used by infappend-frags,
nat-basic/one is used by move-trans,
nat-basic/one-01 is used by inffrag-rec2, preserve-INV-fin, infappend-frags, finfrag-two, inffrag-rec, infappend-moves-gen, frag-rec, inffrag-rec1, finfrag-one-action,
nat-basic/one-04 is used by fragstar-onestate, move-trans, finfrag-onlyone,
nat-basic/one-06 is used by finfrag-one-action,
nat-basic/oz is used by preserve-INV-fin, trace-append, frag-trans, infappend-frags, fintrace, inffrag-rec, infappend-moves-gen, frag-split, frag-rec,
nat-basic/refl-Nat is used by allfragto-frag, preserve-INV-fin, frag-trans, frag-rec-end, infappend-frags, move-trans, frag-size-2, infappend-moves-gen, frag-split,
nat-basic/s-04 is used by allfragto-frag, shortest-frag, move-split, preserve-INV-fin, frag-trans, frag-rec-end, infappend-frags, move-trans, frag-size-2, infappend-moves-gen, frag-split, frag-to,
nat-basic/succ is used by allfragto-frag, frag-step, shortest-frag, frag-step-fin-2, fraginf, move-split, frag-step-inf-zero, fragfin-size-ls, preserve-INV-fin, frag-step-zero, trace-append, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin-zero, frag-notsizeleq, frag-step-inf-inf, frag-step-fin, fintrace, fragfin-size-notls-02, inffrag-rec, fragstar, move-trans, infappend-moves-gen, frag-split, frag-rec, finfrag-one-action, frag-step-inf, finfrag-onlyone, fragfin-size-ls1, preserve-INV, frag-to,
nat-basic/trans-Nat is used by infappend-frags, move-trans, infappend-moves-gen,
nat-basic/z-01 is used by not-finfrag-empty, frag-trans, infappend-frags, infappend-moves-gen,
nat-basic/zero is used by preserve-INV-fin, trace-append, fintrace, move-trans, infappend-moves-gen,

Used from specification list

list/firsteq-01 is used by move-split,
list/Nil is used by move-split, moveone-splitstep, move-trans,
list/a is used by shortest-frag, frag-rec-end2, move-split, frag-two, move-one, preserve-INV-fin, finfrag-rec, frag-noactions, frag-trans, frag-rec-end, finfrag-rec-end, frag-notsizeleq, moveone-splitstep, finfrag-two, emptymove-splitfirst, move-cut-2, move-trans, move-cut, infappend-moves-gen, finfrag-one-action, finfrag-onlyone, finfrag-split, frag-move,
list/app is used by move-split, frag-noactions, emptymove-splitfirst, infappend-moves-gen, finfrag-one-action, finfrag-onlyone,
list/app-02 is used by move-split, preserve-INV-fin, frag-noactions, moveone-splitstep, emptymove-splitfirst, move-trans, infappend-moves-gen, finfrag-onlyone, frag-move,
list/app-04 is used by infappend-moves-gen, finfrag-onlyone,
list/app-06 is used by infappend-moves-gen,
list/c is used by shortest-frag, move-split, preserve-INV-fin, finfrag-rec, frag-noactions, moveone-splitstep, emptymove-splitfirst, move-trans, infappend-moves-gen, finfrag-one-action, finfrag-onlyone, frag-move,
list/c-03 is used by move-split, frag-noactions, moveone-splitstep, emptymove-splitfirst, finfrag-onlyone,
list/c-08 is used by shortest-frag, emptymove-splitfirst, infappend-moves-gen,
list/e is used by move-split, preserve-INV-fin, frag-noactions, moveone-splitstep, emptymove-splitfirst, move-trans, infappend-moves-gen, finfrag-onlyone, frag-move,
list/e-01 is used by shortest-frag,
list/e-02 is used by frag-trans, frag-rec-end,
list/first-02 is used by move-split,
list/fr is used by move-split,
list/in-08 is used by move-split,
list/in-14 is used by move-split, infappend-moves-gen,
list/in-15 is used by move-split, infappend-moves-gen,
list/in-17 is used by move-split,
list/in-append is used by move-split,
list/in-empty is used by move-split,
list/in-rec is used by move-split,
list/len is used by move-split, frag-trans, frag-rec-end, frag-notsizeleq, move-cut-2, move-trans, move-cut, infappend-moves-gen, finfrag-split,
list/len-01 is used by move-trans,
list/len-02 is used by inffrag-rec2, fragstar-onestate, finfrag-one, frag-trans, frag-rec-end, fragfin-size-ls-02, frag-onestate, fragfin-size-02, finfrag-two, fragfin-size-notls-02, inffrag-rec, move-trans, frag-rec, inffrag-rec1, finfrag-one-action,
list/len-05 is used by shortest-frag, move-split, preserve-INV-fin, move-trans, infappend-moves-gen, finfrag-one-action, finfrag-onlyone,

Used from specification stream

stream/add-list-fun-def is used by inffrag-rec2, inffrag-rec, inffrag-rec1,
stream/append-from-le is used by move-trans,
stream/append-le-to is used by infappend-moves-gen,
stream/appinf-to-ge is used by infappend-moves-gen,
stream/extensionality is used by infappend-moves-gen,
stream/extensionality-to is used by infappend-moves-gen,
stream/fin-size-from is used by frag-split,
stream/from-append-tofrom is used by infappend-moves-gen,
stream/get-append-ls is used by frag-rec-end,
stream/get-append-notls is used by frag-rec-end, frag-from-1, frag-rec,
stream/get-finto is used by infappend-frags, infappend-moves-gen,
stream/get-from is used by frag-split,
stream/get-to is used by infappend-moves-gen,
stream/infapp-embed is used by trace-fininf-append,
stream/less-size-from is used by frag-split,
stream/prefix-def is used by infappend-moves-gen,
stream/size-to is used by allfragto-frag, frag-to,
stream/swap-from-to is used by infappend-moves-gen,
stream/swap-to-from is used by infappend-frags,
stream/to-unwind-end-inf is used by infappend-moves-gen,
stream/append-assoc is used by frag-rec-end2, frag-two, finfrag-rec, trace-append, frag-trans, frag-rec-end, fragfin-size-ls-02, frag-from-1, fragfin-size-02, fintrace, finfrag-two, fragfin-size-notls-02, emptymove-splitfirst, infappend-moves-gen, frag-rec, finfrag-split, trace-fininf-append,
stream/append-empty is used by finfrag-rec, infappend-moves-gen,
stream/append-finfin is used by shortest-frag, frag-rec-end2, frag-two, finfrag-rec, finfrag-rec-end, finfrag-two, emptymove-splitfirst, infappend-moves-gen, finfrag-split,
stream/append-from-size is used by move-split, move-trans, move-cut,
stream/append-from-size-01 is used by trace-append, fintrace, finfrag-split,
stream/append-gr-to is used by infappend-moves-gen,
stream/append-inf is used by infappend-moves-gen,
stream/append-split-fin is used by infappend-moves-gen,
stream/append-to-gr-01 is used by infappend-moves-gen,
stream/append-to-size-01 is used by trace-append, fintrace, infappend-moves-gen, finfrag-split,
stream/appendend-equal is used by infappend-moves-gen,
stream/appfin-sel is used by frag-two, finfrag-split,
stream/appinf-get-ge-01 is used by infappend-moves-gen,
stream/appinf-sel is used by infappend-moves-gen,
stream/appinf-selfun is used by infappend-moves-gen,
stream/appinf-to-ge-01 is used by infappend-moves-gen,
stream/cons-append is used by frag-rec,
stream/cons-empty is used by finfrag-rec, frag-rec,
stream/elim-fromto is used by frag-from-1,
stream/elim-fromto-inf is used by infappend-moves-gen,
stream/elim-hd-tl is used by frag-rec,
stream/empty is used by shortest-frag, finfrag-rec, infappend-frags, infappend-moves-gen,
stream/fin-finlen-tolen is used by infappend-moves-gen,
stream/from-fin is used by infappend-frags, infappend-moves-gen, frag-split, frag-from-fin, finfrag-split,
stream/from-inf is used by frag-from-inf, infappend-frags, inffrag-split, infappend-moves-gen, frag-split,
stream/from-zero is used by infappend-moves-gen,
stream/get-append-ls is used by frag-rec-end, frag-from-1,
stream/get-append-notls is used by frag-rec-end,
stream/get-append2-fin is used by frag-trans, frag-rec-end, fragfin-size-ls-02, fragfin-size-notls-02,
stream/get-cons-num is used by finfrag-two,
stream/get-cons-succ is used by fragfin-size-ls-02, fragfin-size-notls-02, frag-rec,
stream/get-cons-zero is used by finfrag-two, frag-rec,
stream/get-from-01 is used by infappend-frags, infappend-moves-gen, frag-split,
stream/get-from-inf is used by infappend-frags, infappend-moves-gen, frag-split,
stream/get-infto is used by infappend-frags, infappend-moves-gen,
stream/get-to is used by allfragto-frag, trace-append, fintrace, infappend-moves-gen, frag-split, frag-to,
stream/hd-fin-lem is used by finfrag-rec, emptymove-splitfirst,
stream/inf-size-from is used by frag-split,
stream/infapp-embed is used by infappend-moves-gen,
stream/length-from is used by infappend-frags, infappend-moves-gen,
stream/length-to is used by infappend-frags,
stream/leq-append-right is used by infappend-moves-gen,
stream/leq-empty is used by infappend-moves-gen,
stream/leq-symm-2 is used by infappend-moves-gen,
stream/neq-fin-inf-03 is used by frag-two, infappend-moves-gen, finfrag-split,
stream/sel-fin is used by allfragto-frag, finexec, frag-step-fin-2, fragfin-size-ls, preserve-INV-fin, exec-fin2, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin-zero, frag-step-fin, fintrace, finfrag-two, fragfin-size-notls-02, fragstar, infappend-moves-gen, frag-split,
stream/sel-inf is used by exec-fin1, inftrace, fraginf, frag-step-inf-zero, infexec, infappend-frags, frag-step-inf-inf, infappend-moves-gen, frag-split, frag-step-inf,
stream/single-to-one is used by move-trans,
stream/size-append is used by trace-append, frag-trans, frag-rec-end, fragfin-size-ls-02, frag-from-1, fragfin-size-02, fintrace, finfrag-two, fragfin-size-notls-02, infappend-moves-gen, frag-rec, finfrag-split,
stream/size-empty is used by finfrag-one, frag-noactions, frag-rec, not-frag-empty,
stream/size-empty-equiv is used by frag-rec-end, frag-onestate, infappend-moves-gen, frag-rec, not-frag-empty,
stream/size-fin is used by exec-fin1, frag-step-fin-2, frag-to-fin, fragfin-size-ls, preserve-INV-fin, exec-fin2, finfrag-one, trace-append, frag-noactions, frag-trans, frag-rec-end, fragfin-size-ls-02, frag-onestate, infappend-frags, fragfin-size, frag-from-1, frag-inf-al, frag-step-fin-zero, fragfin-size-le, fragfin-size-02, frag-step-fin, fintrace, finfrag-two, fragfin-size-notls-02, fragstar, frag-size-2, infappend-moves-gen, frag-split, frag-rec, frag-from-fin, finfrag-split, frag-inf-sl,
stream/size-inf is used by exec-fin1, frag-from-inf, fraginf, frag-step-inf-zero, exec-fin2, frag-noactions, frag-to-inf, infappend-frags, frag-inf-al, frag-step-inf-inf, frag-step-fin, inffrag-split, frag-size-2, infappend-moves-gen, frag-split, frag-step-inf, frag-inf-sl,
stream/size-inf-to is used by infappend-frags, infappend-moves-gen,
stream/size-succ is used by allfragto-frag, trace-append, infappend-frags, fintrace, infappend-moves-gen, frag-split, frag-rec, frag-to,
stream/size-to is used by allfragto-frag, infappend-moves-gen, frag-split, frag-to,
stream/size-to-02 is used by allfragto-frag,
stream/to-empty-inf is used by infappend-moves-gen,
stream/to-fin is used by frag-to-fin, infappend-frags, infappend-moves-gen, finfrag-split,
stream/to-inf is used by frag-to-inf, infappend-frags, inffrag-split, infappend-moves-gen,
stream/to-succ-cons-l-lem is used by move-trans,
stream/to-to-eq-inf is used by infappend-moves-gen,
stream/to-zero is used by infappend-moves-gen,
stream/to-zero-nf is used by infappend-moves-gen,
stream/zero-len is used by frag-step-zero, frag-step-fin-zero,

Used from specification IO-Aut-data

IO-Aut-data/elim-IOAut is used by finexec,
IO-Aut-data/sel-IOAut-dotext is used by move-split, move-one, move-empty, moveone-splitstep, emptymove-splitfirst, move-trans, infappend-moves-gen, frag-move,
IO-Aut-data/sel-IOAut-dotstart is used by exec-fin1, finexec, inftrace, exec-fin2, trace-append, fintrace, infappend-moves-gen,
IO-Aut-data/sel-IOAut-dotstep is used by fraginf, move-split, frag-notsizeleq, inffrag-rec, fragstar, move-trans, infappend-moves-gen, frag-split, finfrag-one-action, fragfin-size-ls1, frag-to,

Used from specification nat-inf

nat-inf/add-all-zero is used by frag-rec-end, fragfin-size-ls-02, fragfin-size-02, fragfin-size-notls-02, frag-split, frag-rec,
nat-inf/add-assoc is used by allfragto-frag, exec-fin1, fraginf, frag-step-inf-zero, fragfin-size-ls, exec-fin2, finfrag-one, trace-append, frag-noactions, frag-trans, frag-rec-end, fragfin-size-ls-02, frag-onestate, infappend-frags, fragfin-size, frag-from-1, frag-size, frag-inf-al, fragfin-size-le, fragfin-size-02, frag-step-inf-inf, frag-step-fin, fintrace, finfrag-two, fragfin-size-notls-02, fragstar, frag-size-2, infappend-moves-gen, frag-split, frag-rec, not-frag-empty, frag-step-inf, finfrag-split, frag-inf-sl, preserve-INV, frag-to,
nat-inf/add-cancel-01 is used by frag-from-1,
nat-inf/add-cancel-03 is used by infappend-moves-gen,
nat-inf/add-cancel-num-01 is used by frag-onestate,
nat-inf/add-cancel-num-03 is used by frag-rec-end, fragfin-size-ls-02, fragfin-size-02, fragfin-size-notls-02, frag-split, frag-rec,
nat-inf/add-cancel-num-04 is used by frag-rec-end, frag-rec,
nat-inf/add-comm is used by allfragto-frag, exec-fin1, fraginf, frag-step-inf-zero, fragfin-size-ls, exec-fin2, finfrag-one, trace-append, frag-noactions, frag-trans, frag-rec-end, fragfin-size-ls-02, frag-onestate, infappend-frags, fragfin-size, frag-from-1, frag-size, frag-inf-al, fragfin-size-le, fragfin-size-02, frag-step-inf-inf, frag-step-fin, fintrace, finfrag-two, fragfin-size-notls-02, fragstar, frag-size-2, infappend-moves-gen, frag-split, frag-rec, not-frag-empty, frag-step-inf, finfrag-split, frag-inf-sl, preserve-INV, frag-to,
nat-inf/add-fin is used by allfragto-frag, trace-append, frag-rec-end, infappend-frags, frag-from-1, fintrace, infappend-moves-gen, frag-split, frag-rec, preserve-INV, frag-to,
nat-inf/add-inf2 is used by fraginf, exec-fin2, infappend-frags, frag-inf-al, frag-step-inf-inf, frag-step-fin, infappend-moves-gen, frag-split, frag-to,
nat-inf/add-ls-cancel-01 is used by frag-from-1, frag-split,
nat-inf/add-ls-cancel-num-04 is used by allfragto-frag, frag-split,
nat-inf/add-not-less is used by trace-append, frag-from-1, fintrace,
nat-inf/addeqinf-cancel is used by exec-fin1, frag-step-inf-zero, infappend-frags, infappend-moves-gen, frag-split, frag-step-inf, frag-inf-sl,
nat-inf/disj-rqui-infty is used by exec-fin1, exec-fin2, frag-noactions, infappend-frags, frag-inf-al, frag-step-fin, infappend-moves-gen, frag-split, frag-inf-sl,
nat-inf/eq-natinf-to-nat-2-1 is used by allfragto-frag, fragfin-size-ls, frag-trans, infappend-frags, fragfin-size, fragfin-size-le, frag-step-fin, fragstar, infappend-moves-gen, frag-split,
nat-inf/eq-natinf-to-nat-2-2 is used by frag-split,
nat-inf/eq-natinf-to-nat-3-2 is used by frag-trans,
nat-inf/eqls-succ is used by preserve-INV,
nat-inf/eqsucc-ls is used by frag-to,
nat-inf/eqsucc-notls is used by frag-size, frag-split,
nat-inf/inf-inseq-reduce is used by infappend-frags, frag-size-2, infappend-moves-gen, frag-split,
nat-inf/inj-rqui is used by finfrag-one, frag-noactions, fragfin-size-ls-02, infappend-frags, fragfin-size-02, finfrag-two, fragfin-size-notls-02, infappend-moves-gen, frag-split,
nat-inf/lele-refl is used by frag-split,
nat-inf/lele-trans is used by frag-split, frag-to,
nat-inf/lels-trans is used by allfragto-frag, frag-split,
nat-inf/less-fin is used by allfragto-frag, frag-to-fin, fragfin-size-ls, preserve-INV-fin, finfrag-one, frag-noactions, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-step-fin, finfrag-two, fragfin-size-notls-02, fragstar, infappend-moves-gen, frag-split, frag-rec, frag-from-fin, finfrag-split, frag-to,
nat-inf/less-inf1 is used by frag-from-inf, frag-to-inf, infappend-frags, inffrag-split, frag-size-2, infappend-moves-gen, frag-to,
nat-inf/less-inf2 is used by fraginf, frag-step-inf-zero, infappend-frags, frag-step-inf-inf, inffrag-split, infappend-moves-gen, frag-split, frag-step-inf, frag-to,
nat-inf/less-less-leftsucc is used by frag-split,
nat-inf/less-succ-leq is used by allfragto-frag, trace-append, frag-rec-end, fintrace, frag-split, frag-rec,
nat-inf/ls-irref is used by allfragto-frag, frag-split,
nat-inf/ls-le is used by frag-from, frag-split,
nat-inf/ls-natinf-to-nat-1-2 is used by frag-trans, frag-split,
nat-inf/ls-natinf-to-nat-2-1 is used by frag-from-1, frag-split, finfrag-split, preserve-INV,
nat-inf/ls-natinf-to-nat-3-1 is used by frag-from-1,
nat-inf/ls-trans is used by infappend-moves-gen, frag-split,
nat-inf/lsle-trans is used by allfragto-frag, frag-from-1, frag-split, preserve-INV,
nat-inf/not-less-zero is used by infappend-moves-gen, frag-rec,
nat-inf/num-add is used by allfragto-frag, finfrag-one, frag-noactions, frag-rec-end, finfrag-two, frag-rec,
nat-inf/sel-rqui-dotn is used by frag-rec-end, frag-from-1, frag-split, frag-rec,
nat-inf/sum-zero-fin is used by frag-rec-end, infappend-moves-gen, frag-rec, not-frag-empty,

Used from specification stream-basic

stream-basic/sel-embed-inf is used by frag-inf-al, frag-inf-sl,
stream-basic/disj-rqui-rqui0 is used by inftrace, frag-two, infappend-moves-gen, finfrag-split,
stream-basic/elim-finp-ant is used by infappend-frags, frag-inf-al, frag-size-2, infappend-moves-gen, frag-split, frag-inf-sl,
stream-basic/elim-finp-suc is used by inftrace, frag-two, infappend-frags, frag-size-2, infappend-moves-gen, frag-split, finfrag-split,
stream-basic/inj-rqui is used by trace-append, frag-noactions, fintrace, infappend-moves-gen,
stream-basic/inj-rqui0 is used by infappend-moves-gen,
stream-basic/sel-rqui-dotl is used by frag-finite-al, infappend-moves-gen, frag-finite-sl,
stream-basic/sel-rqui0-dotf is used by inftrace,
stream-basic/test-finp-rqui is used by frag-finite-al, infappend-frags, infappend-moves-gen, not-frag-fin-inf, frag-finite-sl,
stream-basic/test-finp-rqui0 is used by frag-finite-al, infappend-frags, not-frag-inf-fin, infappend-moves-gen, frag-finite-sl,

Used from specification list-data

list-data/elim-add is used by shortest-frag, move-split, preserve-INV-fin, move-trans, infappend-moves-gen,
list-data/elim-list-c is used by shortest-frag, move-split, finfrag-rec, frag-noactions, moveone-splitstep, emptymove-splitfirst, finfrag-one-action, finfrag-onlyone, frag-move,
list-data/l is used by shortest-frag, not-finfrag-empty, move-split, fragstar-onestate, fragfin-size-ls, preserve-INV-fin, frag-trans, frag-rec-end, fragfin-size-ls-02, infappend-frags, frag-from-1, frag-step-fin, fragfin-size-notls-02, fragstar, move-trans, infappend-moves-gen, frag-split, finfrag-one-action, fragfin-size-le1, finfrag-onlyone, frag-from-fin, finfrag-split, fragfin-size-ls1,
list-data/lf-01 is used by frag-noactions,
list-data/size-nil is used by shortest-frag, not-finfrag-empty, move-split, frag-trans, frag-rec-end, infappend-frags, move-trans, infappend-moves-gen, finfrag-one-action, finfrag-onlyone,

Used from specification option

option/disj-Some-None is used by infappend-moves-gen,
option/elim-Some is used by moveone-splitstep, infappend-moves-gen,

Used from specification list-del

list-del/first-append-02 is used by move-split, move-trans,
list-del/get-append-grt is used by frag-trans,
list-del/get-append-less is used by frag-rec-end, move-trans,
list-del/get-last-nonempty is used by preserve-INV-fin,
list-del/rest-empty is used by move-trans,
list-del/elim-firstn-restn is used by move-split, move-cut-2, move-trans, finfrag-split,
list-del/first-length is used by infappend-moves-gen,
list-del/firstN-len is used by move-split, move-trans, move-cut,
list-del/firstn-one-01 is used by move-split,
list-del/get-app is used by frag-rec-end,
list-del/get-append-grt is used by frag-rec-end,
list-del/get-append-grt-02 is used by frag-trans, frag-rec-end,
list-del/get-append-less is used by frag-trans, frag-rec-end,
list-del/get-butlast is used by frag-trans, frag-rec-end,
list-del/get-last is used by frag-trans, frag-rec-end,
list-del/get-numrec is used by frag-rec-end, infappend-moves-gen, finfrag-one-action,
list-del/get-succ is used by move-trans,
list-del/get-zero is used by move-split, move-one, moveone-splitstep, emptymove-splitfirst, move-trans, finfrag-one-action, frag-move,
list-del/list-select-not-first is used by infappend-moves-gen,
list-del/one-03 is used by inffrag-rec2, move-empty, frag-rec-end, finfrag-two, inffrag-rec, move-trans, inffrag-rec1, finfrag-one-action,
list-del/restN-zero is used by infappend-frags,

Used from specification infinite-append

infinite-append/infinite-append is used by infappend-frags, infappend-moves-gen,
infinite-append/infinite-append-butlast is used by infappend-frags, infappend-moves-gen,
infinite-append/mon-below is used by infappend-frags,