[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

nat/elim-pred-c is used by forall-get-def, exists-get-def,
nat/l-num-06 is used by indexWhere-length-ls,
nat/le-def is used by indexWhere-le-length,
nat/lels is used by indexWhere-length-notle, forall-get-def, exists-get-def,
nat/lez is used by forall-get-def, exists-get-def,
nat/ls-le-simp is used by indexWhere-length-notle,
nat/succ-01 is used by indexWhere-length-notle, forall-get-def, exists-get-def,

Used from specification list-data

list-data/l is used by indexWhere-length-notle, forall-get-def, indexWhere-length-eq, exists-get-def,
list-data/size-nil is used by indexWhere-length-notle, indexWhere-length-ls, forall-get-def, indexWhere-length-eq, exists-get-def, indexWhere-app-split,

Used from specification filter-count

filter-count/filter-base is used by filter-forall2, filter-exists, filter-forall,
filter-count/filter-in is used by filter-forall2,
filter-count/filter-rec is used by filter-forall2, filter-exists, filter-forall,

Used from specification nat-basic

nat-basic/a is used by indexWhere-length-notle, indexWhere-length-ls, indexWhere-get, forall-get-def, indexWhere-length-eq, forall-rmpos, exists-get-def, indexWhere-app-split, indexWhere-one,
nat-basic/add-base is used by indexWhere-app-split,
nat-basic/c is used by indexWhere-length-notle, indexWhere-length-ls, indexWhere-get, forall-get-def, indexWhere-length-eq, forall-rmpos, exists-get-def, indexWhere-app-split, indexWhere-one,
nat-basic/eq-01 is used by indexWhere-length-eq, indexWhere-app-split,
nat-basic/f is used by indexWhere-length-notle, indexWhere-length-ls, forall-get-def, exists-get-def,
nat-basic/l is used by indexWhere-length-ls,
nat-basic/less-zero is used by indexWhere-length-notle, forall-get-def, exists-get-def,
nat-basic/one-01 is used by forall-get-def, exists-get-def,
nat-basic/oz is used by forall-get-def, exists-get-def,
nat-basic/s-04 is used by indexWhere-length-notle, forall-get-def, exists-get-def,
nat-basic/succ is used by indexWhere-length-notle, indexWhere-length-ls, forall-get-def, indexWhere-length-eq, forall-rmpos, exists-get-def, indexWhere-app-split,
nat-basic/z-01 is used by indexWhere-length-eq,

Used from specification list

list/Nil is used by filter-forall2, forall-append, exists-append, indexWhere-app-split,
list/a is used by indexWhere-length-notle, indexWhere-length-ls, filter-forall2, forall-exists, indexWhere-get, forall-append, forall-get-def, filter-exists, exists-append, filter-forall, forall-in-def, exists-in-def, indexWhere-length-eq, forall-rmpos, exists-get-def, exists-forall, forall-l, forall-1l, indexWhere-app-split, indexWhere-one,
list/app is used by indexWhere-one,
list/app-02 is used by filter-exists,
list/c is used by indexWhere-length-notle, indexWhere-length-ls, filter-forall2, forall-exists, indexWhere-get, forall-append, forall-get-def, filter-exists, exists-append, filter-forall, forall-in-def, exists-in-def, indexWhere-length-eq, forall-rmpos, exists-get-def, exists-forall, forall-l, forall-1l, indexWhere-app-split,
list/e is used by filter-exists,
list/in-14 is used by filter-forall2,
list/in-17 is used by forall-one, exists-one,
list/in-append is used by filter-forall2,
list/in-empty is used by filter-forall2, forall-in-def, exists-in-def,
list/in-rec is used by forall-in-def, exists-in-def,
list/len-01 is used by filter-forall2, filter-forall,
list/len-02 is used by forall-get-def, exists-get-def,
list/len-05 is used by indexWhere-length-notle, indexWhere-length-ls, forall-get-def, indexWhere-length-eq, exists-get-def, indexWhere-app-split,

Used from specification list-del

list-del/del-n is used by forall-l,
list-del/del1-n is used by forall-1l,
list-del/get-append-grt is used by forall-get-def, exists-get-def,
list-del/del-e is used by forall-l,
list-del/del-y is used by forall-l,
list-del/del1-e is used by forall-1l,
list-del/del1-y is used by forall-1l,
list-del/delpos-base is used by forall-rmpos,
list-del/delpos-empty is used by forall-rmpos,
list-del/delpos-rec is used by forall-rmpos,
list-del/get-append-less is used by exists-get-def,
list-del/get-succ is used by indexWhere-get, forall-get-def, exists-get-def,
list-del/get-zero is used by indexWhere-get, forall-get-def, exists-get-def,
list-del/one-03 is used by exists-get-def,