[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
Used from specification list-last
- list-last/bitlista/mk-elem
is used by
inmklist-01,
inmklist,
- list-last/bitlista/mk-empty
is used by
mklist-03,
- list-last/bitlista/mk-last
is used by
mklist-num-01,
mklist-num,
mklist-03,
mklist-02,
- list-last/bitlista/mk-plus
is used by
mklist-num-01,
mklist-num,
mklist-intro,
mklist-03,
mklist-02,
mklist-01,
mklist,
- list-last/bitlista/mk-zero
is used by
mklist-intro,
mklist-01,
mklist,
- list-last/bitlista/mklist-one
is used by
mklist-num-01,
mklist-num,
mklist-intro,
mklist-03,
mklist-02,
mklist-01,
mklist,
Used from specification list-data
- list-data/bitlista/l
is used by
leone-true,
leone-false,
- list-data/bitlista/le-one
is used by
leone-true,
leone-false,
leone,
- list-data/bitlista/lf-01
is used by
one-02,
leone-true,
leone-false,
- list-data/bitlista/size-01
is used by
mklist-intro,
mklist-01,
mklist,
Used from specification list
- list/bitlista/Nil
is used by
nottrue-02,
nottrue-01,
nottrue,
notfalse-01,
notfalse,
- list/bitlista/a
is used by
somein,
one-02,
nottrue-02,
nottrue-01,
nottrue,
notfalse-01,
notfalse,
mklist-num-01,
mklist-num,
mklist-intro,
mklist-03,
mklist-02,
mklist-01,
mklist,
leone-true,
leone-false,
last-first-01,
last-first,
- list/bitlista/app
is used by
one-02,
nottrue-01,
nottrue,
notfalse-01,
notfalse,
leone-true,
leone-false,
- list/bitlista/app-01
is used by
nottrue-02,
nottrue-01,
nottrue,
notfalse-01,
notfalse,
mklist-num-01,
mklist-num,
mklist-intro,
- list/bitlista/app-02-ant
is used by
mklist-03,
- list/bitlista/c
is used by
somein,
one-02,
nottrue-02,
nottrue-01,
nottrue,
notfalse-01,
notfalse,
mklist-intro,
mklist-01,
mklist,
leone-true,
leone-false,
- list/bitlista/c-03
is used by
one-02,
mklist-03,
- list/bitlista/c-04
is used by
nottrue,
notfalse,
leone-true,
leone-false,
- list/bitlista/c-06
is used by
mklist-intro,
mklist-02,
mklist-01,
mklist,
- list/bitlista/c-08
is used by
one-02,
- list/bitlista/e
is used by
one-02,
leone-true,
leone-false,
- list/bitlista/e-01
is used by
somein,
- list/bitlista/first
is used by
leone-true,
leone-false,
- list/bitlista/in-06
is used by
somein,
nottrue-02,
nottrue-01,
nottrue,
notfalse-01,
notfalse,
mklist-intro,
mklist-01,
mklist,
- list/bitlista/in-14
is used by
nottrue-01,
nottrue,
notfalse-01,
notfalse,
mklist-02,
- list/bitlista/in-15
is used by
nottrue-01,
nottrue,
notfalse-01,
notfalse,
- list/bitlista/in-append
is used by
mklist-02,
- list/bitlista/in-empty
is used by
mklist-intro,
- list/bitlista/len
is used by
mklist-intro,
mklist-01,
mklist,
- list/bitlista/len-02
is used by
mklist-intro,
mklist-01,
mklist,
Used from specification nat-basic2
- nat-basic2/a
is used by
mklist-num-01,
mklist-num,
mklist-intro,
mklist-03,
mklist-02,
mklist-01,
mklist,
- nat-basic2/c
is used by
mklist-num-01,
mklist-num,
mklist-intro,
mklist-03,
mklist-02,
mklist-01,
mklist,
- nat-basic2/oz
is used by
mklist-num-01,
mklist-num,
- nat-basic2/succ
is used by
mklist-03,
mklist-02,
Used from specification nat-basic1