[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 fieldspec
- fieldspec/inj
is used by
type-neq,
type-12,
type-11,
type-10,
type-09,
type-08,
type-07,
type-05,
type-04,
type-02,
th-01,
out-05,
mode-neq,
mode-05,
length-diff,
length-05,
length-02,
length-01,
endfin-diff-02,
endfin-diff-01,
endfin-diff,
diff-06,
diff-05,
diff-04,
diff-03,
diff-02,
diff-01,
diff,
- fieldspec/inj-01
is used by
type-fieldspec,
Used from specification storekey
- storekey/disj
is used by
type-03,
out-04,
mode-04,
len,
diff-07,
- storekey/inj-03
is used by
uninit-02,
type-neq,
type-12,
type-11,
type-10,
type-09,
type-08,
type-07,
type-05,
type-04,
type-02,
type-01,
th-01,
out-05,
mode-neq,
mode-key,
mode-05,
length-diff,
length-05,
length-03,
length-02,
length-01,
endfin-key,
endfin-diff-02,
endfin-diff-01,
endfin-diff,
diff-06,
diff-05,
diff-04,
diff-03,
diff-02,
diff-01,
diff,
- storekey/sel-05
is used by
type-fieldspec,
- storekey/test-05
is used by
type-06,
length-04,
Used from specification fieldname
- fieldname/elim
is used by
initfield-01,
- fieldname/inj
is used by
length-01,
endfin-diff-02,
endfin-diff-01,
endfin-diff,
diff-05,
diff-04,
diff-03,
diff-02,
diff-01,
diff,
- fieldname/sel
is used by
initfield-01,
Used from specification refkey
- refkey/inj
is used by
uninit-eq,
uninit-02,
uninit-01,
th-01,
out-05,
out-04,
out-03,
out-02,
mode-neq,
mode-06,
mode-05,
mode-04,
mode-03,
mode-02,
endfin-eq,
endfin-diff-02,
endfin-diff-01,
endfin-diff,
diff-07,
diff-06,
diff-05,
diff-04,
diff-03,
diff-02,
diff-01,
diff,
- refkey/inj-01
is used by
uninit-eq,
uninit-02,
out-03,
out-01,
mode-02,
mode-01,
endfin-eq,
- refkey/sel-01
is used by
mode-ref,
endfin-ref,
- refkey/sel-02
is used by
mode-key,
endfin-key,
Used from specification javatype
Used from specification classname