[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 store

store/linheap/size is used by path-nodups-subset,
store/linheap/In-empty is used by path-nodups-subset,
store/linheap/Size-empty is used by path-nodups-subset,
store/linheap/empty is used by path-nodups-subset, cyclic-weak-def,
store/linheap/empty-01 is used by path-nodups-subset,

Used from specification nat-mult

nat-mult/dist-merge is used by cyclic-floyd-def,
nat-mult/zero-01 is used by cyclic-floyd-def,
nat-mult/ax-03 is used by cyclic-ncyclic, cyclic-floyd-def, cyclic-alt-def,
nat-mult/coef-21 is used by cyclic-floyd-def,
nat-mult/le-01 is used by cyclic-weak-def,
nat-mult/le-02 is used by cyclic-floyd-def,
nat-mult/ls is used by cyclic-brent-def,
nat-mult/ls-01 is used by cyclic-floyd-def,
nat-mult/ls-04 is used by cyclic-floyd-def,
nat-mult/ls-08 is used by cyclic-weak-def,
nat-mult/mult-a is used by cyclic-weak-def, cyclic-ncyclic, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def, cyclic-all-ncyclic,
nat-mult/mult-c is used by cyclic-weak-def, cyclic-ncyclic, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def, cyclic-all-ncyclic,
nat-mult/one is used by cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat-mult/one-01 is used by cyclic-floyd-def,
nat-mult/rsucc-02 is used by cyclic-weak-def, cyclic-ncyclic, cyclic-floyd-def, cyclic-alt-def,
nat-mult/two-02 is used by cyclic-floyd-def,
nat-mult/two-zero-01 is used by cyclic-floyd-def, cyclic-brent-def,

Used from specification list

list/reflist/a is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,
list/reflist/app is used by path-nodups-subset,
list/reflist/c is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,
list/reflist/c-08 is used by path-dups, cyclic-weak-def,
list/reflist/e-01 is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,
list/reflist/e-02 is used by legal-noncylic-equiv-reaches-null,
list/reflist/in-06 is used by path-nodups-subset,
list/reflist/in-empty is used by path-nodups-subset,
list/reflist/len is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,
list/reflist/len-02 is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,

Used from specification nat-basic1

nat-basic1/f is used by path-nodups-subset, path-dups, cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat-basic1/lf is used by cyclic-brent-def,
nat-basic1/lf-01 is used by cyclic-brent-def,
nat-basic1/lf-02 is used by path-dups, cyclic-weak-def, cyclic-brent-def,
nat-basic1/ls-02 is used by cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat-basic1/neq-01 is used by path-dups,
nat-basic1/one-01 is used by path-nodups-subset,
nat-basic1/ref-1 is used by cyclic-floyd-def,
nat-basic1/trans-1 is used by cyclic-brent-def,
nat-basic1/zero is used by path-dups,
nat-basic1/zero-01 is used by path-dups,

Used from specification nat-pot

nat-pot/potex is used by cyclic-brent-def,
nat-pot/add is used by cyclic-brent-def,
nat-pot/pot-mon is used by cyclic-brent-def,
nat-pot/pot2-def is used by cyclic-brent-def,
nat-pot/two-pot-zero is used by cyclic-brent-def,

Used from specification list-dup

list-dup/reflist/dups-cons is used by path-nodups-subset, cyclic-weak-def,
list-dup/reflist/e-01 is used by path-nodups-subset,
list-dup/reflist/rec is used by cyclic-weak-def,

Used from specification path-reachable

path-reachable/k-reachable-def is used by legal-noncylic-equiv-reaches-null,
path-reachable/path-delnonmember is used by path-nodups-subset,
path-reachable/path-prefix is used by path-dups,
path-reachable/reach-n-path-n is used by path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,
path-reachable/reach-n-split is used by cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
path-reachable/reach-n-split-le is used by cyclic-brent-def,
path-reachable/reachable-1-def is used by reach-n-next-legal, legal-noncylic-equiv-reaches-null,
path-reachable/reachable-n-base is used by cyclic-ncyclic, cyclic-all-cyclic,
path-reachable/reachable-n-rec-1 is used by cyclic-floyd-def, cyclic-all-cyclic,
path-reachable/reachable-n-rec-rev is used by reach-n-next-legal, legal-noncylic-equiv-reaches-null, cyclic-all-cyclic,
path-reachable/reachable-n-trans is used by cyclic-floyd-def,
path-reachable/reachable-star-def is used by legal-noncylic-equiv-reaches-null,
path-reachable/id-reachable is used by legal-noncylic-equiv-reaches-null,
path-reachable/path-cons is used by path-nodups-subset,
path-reachable/path-empty is used by path-nodups-subset,
path-reachable/path-first-in-H is used by path-nodups-subset,
path-reachable/path-last is used by legal-noncylic-equiv-reaches-null,
path-reachable/path-last-not-null is used by legal-noncylic-equiv-reaches-null,
path-reachable/path-one is used by path-nodups-subset,
path-reachable/reach-alloc is used by legal-noncylic-equiv-reaches-null,
path-reachable/reach-n-unique is used by legal-noncylic-equiv-reaches-null, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
path-reachable/reachable-1-def is used by reach-n-next-legal, legal-noncylic-equiv-reaches-null, cyclic-floyd-def, cyclic-all-cyclic,
path-reachable/reachable-n-1 is used by cyclic-floyd-def,
path-reachable/reachable-n-base is used by reach-n-next-legal, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def, cyclic-all-cyclic,
path-reachable/reachable-n-trans is used by cyclic-ncyclic, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,

Used from specification list-data

list-data/reflist/elim-list-c is used by path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,
list-data/reflist/l is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null,
list-data/reflist/size-01 is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def,

Used from specification list-del

list-del/reflist/dups-def is used by path-dups,
list-del/reflist/firstn-last is used by path-dups,
list-del/reflist/firstn-restn-eq is used by path-dups,
list-del/reflist/first-length is used by path-dups,
list-del/reflist/firstN-empty is used by path-dups,
list-del/reflist/get-succ is used by path-dups,
list-del/reflist/get-zero-01 is used by path-dups,
list-del/reflist/weak-firstN-rec is used by path-dups,

Used from specification nat

nat/one-02 is used by cyclic-floyd-def,
nat/add-01 is used by cyclic-brent-def,
nat/add-num-01 is used by cyclic-weak-def, cyclic-floyd-def,
nat/ax-02 is used by cyclic-brent-def,
nat/cancel-01 is used by cyclic-floyd-def,
nat/elim-pred-c is used by path-dups, cyclic-floyd-def, cyclic-brent-def,
nat/elim-sub is used by cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat/eq-01 is used by cyclic-floyd-def, cyclic-brent-def,
nat/eqle-one is used by path-dups,
nat/fle is used by path-dups, cyclic-brent-def,
nat/fle-01 is used by cyclic-brent-def,
nat/le-add is used by cyclic-weak-def, cyclic-floyd-def,
nat/le-ls-simp is used by path-nodups-subset, cyclic-brent-def,
nat/lels is used by path-nodups-subset, path-dups, cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def,
nat/lels-01 is used by path-nodups-subset, cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat/lels-03 is used by path-dups, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat/lep is used by cyclic-brent-def,
nat/lep-02 is used by cyclic-floyd-def,
nat/let is used by path-dups,
nat/lez is used by path-nodups-subset,
nat/lez-01 is used by path-nodups-subset, cyclic-brent-def,
nat/ls-01 is used by path-nodups-subset,
nat/ls-le-simp is used by path-dups, cyclic-brent-def,
nat/pred-03 is used by path-nodups-subset, path-dups,
nat/succ-01 is used by path-dups, cyclic-weak-def,

Used from specification list-last

list-last/reflist/l-02 is used by path-dups,
list-last/reflist/l-02 is used by path-dups, legal-noncylic-equiv-reaches-null,
list-last/reflist/last-elim is used by legal-noncylic-equiv-reaches-null,

Used from specification nat-basic2

nat-basic2/a is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def, cyclic-ncyclic, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat-basic2/c is used by path-nodups-subset, path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def, cyclic-ncyclic, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def, cyclic-all-cyclic,
nat-basic2/eq-01 is used by path-dups, legal-noncylic-equiv-reaches-null, cyclic-floyd-def,
nat-basic2/l is used by cyclic-floyd-def,
nat-basic2/l-01 is used by cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat-basic2/l-02 is used by path-dups, cyclic-weak-def, cyclic-brent-def,
nat-basic2/oz is used by path-dups, legal-noncylic-equiv-reaches-null, cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def,
nat-basic2/s is used by path-nodups-subset, path-dups, cyclic-floyd-def, cyclic-brent-def,
nat-basic2/succ is used by reach-n-next-legal, legal-noncylic-equiv-reaches-null, cyclic-weak-def, cyclic-ncyclic, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def, cyclic-all-cyclic,
nat-basic2/z is used by cyclic-weak-def, cyclic-floyd-def, cyclic-brent-def, cyclic-alt-def,
nat-basic2/z-01 is used by cyclic-weak-def,