[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 set-union

set-union/Intersect is used by intempty,
set-union/Union is used by firstN-01,
set-union/int-empty-01 is used by intempty-02, dups-02,
set-union/Intersect is used by firstN-01,
set-union/Union is used by in-union, dups-01,
set-union/int-a is used by intempty-02, intempty-01, firstN-01, firstN, dups-03,
set-union/int-c is used by intempty-02, intempty-01, firstN-01, firstN, dups-05, dups-04, dups-03,
set-union/int-e is used by firstN,
set-union/int-empty is used by firstN,
set-union/int-inse is used by firstN,
set-union/una is used by list2set-append, in-union, dups-01,
set-union/unadd is used by list2set-append,
set-union/unc is used by list2set-append, in-union, dups-01,
set-union/une is used by list2set-append,

Used from specification nat

nat/eq-02 is used by len,
nat/fle is used by firstN,
nat/fle-01 is used by firstN,
nat/lels is used by in-01, firstN,
nat/lels-01 is used by set2set, len, in-01, dups,
nat/leprf is used by in-01,
nat/ls-01 is used by set2set, len, in-01, dups,

Used from specification set-basic

set-basic/Extension is used by intempty, firstN-01,
set-basic/In-empty is used by intempty, in-01, in, firstN-01,
set-basic/Size-empty is used by len, firstN,
set-basic/ne is used by set2list-one, list2set-empty-01,
set-basic/ne-01 is used by subset, intempty-02, intempty-01, in, firstN-01,
set-basic/rax is used by in,
set-basic/size-zero is used by set2set, len, in-01, firstN-01, firstN, dups-02, dups,
set-basic/size-zero-01 is used by subset, set2set, len, intempty-02, in-01, in, firstN-01, firstN, dups-02, dups,
set-basic/sub-add-03 is used by subset,

Used from specification list-data

list-data/elim-list-c is used by firstN,
list-data/l is used by firstN-01, firstN,
list-data/size-01 is used by len,

Used from specification list

list/Nil is used by list2set-append,
list/a is used by subset, set2set, set2list-one, list2set-one, list2set-empty-01, list2set-append, len, in-01, in, firstN, empty, dups-03, dups-02, dups-01, dups,
list/app is used by set2list-one, list2set-one,
list/app-02-ant is used by empty,
list/c is used by subset, set2set, set2list-one, list2set-empty-01, list2set-append, len, in-01, in, firstN, empty, dups,
list/c-04 is used by set2list-one,
list/e is used by empty,
list/e-01 is used by firstN,
list/in-06 is used by in,
list/in-17 is used by subset, in-01,
list/in-append is used by subset, in-01,
list/in-empty is used by subset, in-01, in,
list/len is used by len, firstN,
list/len-02 is used by len, firstN,

Used from specification list-dup

list-dup/dups-appex is used by dups-03, dups-01,
list-dup/a is used by dups-02, dups-01,
list-dup/e-01 is used by dups,
list-dup/in-06 is used by dups-02,
list-dup/rec is used by dups,

Used from specification nat-basic2

nat-basic2/a is used by set2set, len, in-01, firstN, dups,
nat-basic2/c is used by set2set, len, in-01, firstN, dups,
nat-basic2/l is used by firstN,
nat-basic2/s is used by set2set, len, in-01, dups,
nat-basic2/succ is used by firstN,

Used from specification nat-basic1

nat-basic1/f is used by firstN-01, firstN,
nat-basic1/one-01 is used by set2set, len, in-01, dups,
nat-basic1/ref-1 is used by set2set, len, in-01, firstN, dups,

Used from specification oset

oset/bmin-eq is used by set2set,
oset/bmin-in is used by in-01,
oset/bmin-nin is used by in-01,
oset/bmin-nin-01 is used by dups,
oset/bmin-one is used by set2list-one,
oset/bmin-size-01 is used by set2set, len, in-01, dups,
oset/min-inn is used by in-01,
oset/min-one is used by set2list-one,

Used from specification list-del

list-del/firstN-in-01 is used by firstN-01,
list-del/firstN-in-05 is used by firstN-01,
list-del/firstN-rec is used by firstN,
list-del/firstN-zero is used by firstN,