[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 nat-basic

nat-basic/a is used by subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
nat-basic/add-base is used by subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
nat-basic/c is used by subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
nat-basic/eq-01 is used by subarray-inc, subarray-inc-offset0,
nat-basic/f is used by subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
nat-basic/l is used by rev-subarray-last,
nat-basic/l-02 is used by rev-subarray-last,
nat-basic/less-zero is used by rev-mkarray-empty, rev-subarray-last,
nat-basic/lf is used by subarray-prefix-fistn,
nat-basic/lf-01 is used by subarray-inc-offset0,
nat-basic/one-01 is used by subarray-inc-offset0,
nat-basic/oz is used by subarray-inc-offset0, rev-subarray-last,
nat-basic/s-04 is used by subarray-inc, subarray-inc-offset0, rev-subarray-last,
nat-basic/succ is used by subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
nat-basic/trans-nat is used by subarray-prefix-fistn,
nat-basic/zero is used by subarray-inc-offset0,

Used from specification nat

nat/anti is used by subarray-inc,
nat/cancel-01 is used by subarray-inc-offset0,
nat/elim-pred-c is used by subarray-inc-offset0,
nat/eqle-one is used by subarray-inc-offset0,
nat/fle is used by rev-subarray-last,
nat/le-ls-simp is used by subarray-inc, subarray-inc-offset0,
nat/lels is used by subarray-inc, subarray-inc-offset0, rev-subarray-last,
nat/lels-03 is used by subarray-inc-offset0, subarray-prefix-fistn,
nat/les is used by subarray-inc-offset0,
nat/lez is used by subarray-inc-offset0,
nat/succ-01 is used by subarray-inc, subarray-inc-offset0,
nat/zero is used by subarray-inc, subarray-inc-offset0,

Used from specification list-last

list-last/list-as-arrayinstance/rev-rewrite is used by rev-subarray-last,
list-last/list-as-arrayinstance/last-elim is used by rev-subarray-last,
list-last/list-as-arrayinstance/rev-app is used by rev-subarray-last,
list-last/list-as-arrayinstance/rev-e is used by rev-subarray-last,
list-last/list-as-arrayinstance/rev-empty is used by rev-mkarray-empty, rev-subarray-last,
list-last/list-as-arrayinstance/rev-in is used by rev-subarray-last,
list-last/list-as-arrayinstance/rev-length is used by rev-subarray-last,
list-last/list-as-arrayinstance/rev-one is used by rev-subarray-last,

Used from specification list-data

list-data/list-as-arrayinstance/l is used by subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
list-data/list-as-arrayinstance/size-nil is used by rev-mkarray-empty, rev-subarray-last,

Used from specification list

list/list-as-arrayinstance/Last is used by subarray-inc, subarray-inc-offset0, rev-subarray-last,
list/list-as-arrayinstance/a is used by subarray-inc, subarray-inc-offset0, rev-subarray-last,
list/list-as-arrayinstance/c is used by subarray-inc-offset0,
list/list-as-arrayinstance/e-02 is used by rev-subarray-last,
list/list-as-arrayinstance/in-14 is used by rev-subarray-last,
list/list-as-arrayinstance/in-15 is used by rev-subarray-last,
list/list-as-arrayinstance/in-17 is used by rev-subarray-last,
list/list-as-arrayinstance/in-append is used by rev-subarray-last,
list/list-as-arrayinstance/len is used by subarray-inc, subarray-inc-offset0,
list/list-as-arrayinstance/len-02 is used by subarray-inc, subarray-inc-offset0,
list/list-as-arrayinstance/len-05 is used by subarray-inc-offset0, rev-subarray-last,

Used from specification array-copy

array-copy/at-subarray is used by subarray-inc, subarray-inc-offset0,
array-copy/size-subarray is used by subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
array-copy/subarray-at is used by subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,

Used from specification array

array/Extension is used by rev-mkarray-empty, subarray-inc, subarray-inc-offset0, rev-subarray-last, subarray-prefix-fistn,
array/Size-mkarray is used by rev-mkarray-empty,

Used from specification list-del

list-del/list-as-arrayinstance/get-append-less is used by subarray-inc-offset0,
list-del/list-as-arrayinstance/get-butlast is used by subarray-inc,
list-del/list-as-arrayinstance/get-firstn is used by subarray-prefix-fistn,
list-del/list-as-arrayinstance/firstn-length-03 is used by subarray-prefix-fistn,
list-del/list-as-arrayinstance/get-append-grt is used by subarray-inc, subarray-inc-offset0,
list-del/list-as-arrayinstance/get-zero is used by rev-subarray-last,
list-del/list-as-arrayinstance/one-03 is used by subarray-inc, subarray-inc-offset0,