[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 int-basic2
Used from specification typefuns
- typefuns/le-noreftype
is used by
okval-supertype,
okval-subtype-01,
- typefuns/le-noreftype-01
is used by
okval-subtype-01,
- typefuns/array
is used by
okprim-letype,
- typefuns/hasct
is used by
hasclasstype,
- typefuns/hasct-01
is used by
hasclasstype,
- typefuns/hasct-02
is used by
hasclasstype,
- typefuns/hasct-03
is used by
hasclasstype,
- typefuns/hasct-04
is used by
hasclasstype,
- typefuns/hasct-05
is used by
hasclasstype,
- typefuns/hasct-06
is used by
hasclasstype,
- typefuns/hasct-07
is used by
hasclasstype,
- typefuns/hasct-08
is used by
hasclasstype,
- typefuns/hasct-09
is used by
hasclasstype,
- typefuns/hasct-10
is used by
hasclasstype,
- typefuns/hasct-11
is used by
hasclasstype,
- typefuns/isreftype
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-01
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-02
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-03
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-04
is used by
okval-refval,
okval-reftype,
okprim-ref,
initval-ref,
initial-value-01,
coerce-okval,
- typefuns/isreftype-05
is used by
okval-refval,
okval-reftype,
okprim-ref,
initval-ref,
initial-value-01,
coerce-okval,
- typefuns/isreftype-06
is used by
okval-reftype,
okprim-ref,
initval-ref,
initial-value-01,
- typefuns/isreftype-07
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-08
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-09
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-10
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/isreftype-11
is used by
okval-refval,
okval-reftype,
okprim-ref,
initial-value-02,
initial-value-01,
- typefuns/le
is used by
okprim-letype,
- typefuns/le-01
is used by
okprim-letype,
- typefuns/le-02
is used by
okprim-letype,
- typefuns/le-03
is used by
okprim-letype,
- typefuns/le-04
is used by
okprim-letype,
- typefuns/le-05
is used by
okprim-letype,
- typefuns/le-06
is used by
okprim-letype,
- typefuns/le-07
is used by
okprim-letype,
- typefuns/le-08
is used by
okprim-letype,
- typefuns/le-09
is used by
okprim-letype,
- typefuns/le-10
is used by
okprim-letype,
- typefuns/le-11
is used by
okprim-letype,
- typefuns/le-12
is used by
okprim-letype,
- typefuns/le-13
is used by
okprim-letype,
- typefuns/le-14
is used by
okprim-letype,
- typefuns/le-15
is used by
okprim-letype,
- typefuns/le-16
is used by
okprim-letype,
- typefuns/le-17
is used by
okprim-letype,
- typefuns/le-18
is used by
okprim-letype,
- typefuns/le-19
is used by
okprim-letype,
- typefuns/le-noreftype-01
is used by
okval-supertype,
Used from specification int-basic1
Used from specification javatype
- javatype/disj-01
is used by
okval-case,
- javatype/disj-02
is used by
okval-refval,
okval-case,
initial-value-01,
initial-okval,
coerce-ref,
coerce-okval,
- javatype/disj-03
is used by
initial-okval,
coerce-okval,
- javatype/disj-04
is used by
okval-case,
- javatype/disj-05
is used by
okval-case,
- javatype/disj-06
is used by
typeval-04,
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-07
is used by
initial-okval,
coerce-okval,
- javatype/disj-08
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-09
is used by
typeval-01,
okval-refval,
coerce-okval,
- javatype/disj-10
is used by
okval-case,
- javatype/disj-11
is used by
okval-case,
- javatype/disj-12
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-13
is used by
okval-case,
- javatype/disj-14
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-16
is used by
okval-case,
- javatype/disj-17
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-18
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-19
is used by
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-20
is used by
okval-case,
- javatype/disj-21
is used by
typeval-05,
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-22
is used by
typeval-02,
okval-refval,
coerce-okval,
- javatype/disj-23
is used by
okval-case,
- javatype/disj-24
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-25
is used by
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-26
is used by
typeval-06,
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-27
is used by
typeval-03,
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-28
is used by
okval-case,
- javatype/disj-29
is used by
okval-case,
- javatype/disj-30
is used by
okval-case,
- javatype/disj-31
is used by
okval-case,
- javatype/disj-32
is used by
okval-case,
- javatype/disj-33
is used by
okval-case,
- javatype/disj-34
is used by
okval-case,
- javatype/disj-35
is used by
okval-case,
- javatype/disj-36
is used by
okval-case,
- javatype/disj-37
is used by
okval-case,
- javatype/disj-38
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-39
is used by
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-40
is used by
okval-case,
- javatype/disj-41
is used by
okval-case,
- javatype/disj-42
is used by
okval-case,
- javatype/disj-43
is used by
okval-case,
- javatype/disj-44
is used by
okval-case,
initial-okval,
coerce-okval,
- javatype/disj-45
is used by
okval-refval,
okval-case,
initial-value-01,
coerce-ref,
- javatype/disj-46
is used by
okval-case,
- javatype/disj-47
is used by
okval-case,
- javatype/disj-48
is used by
okval-case,
- javatype/disj-49
is used by
okval-case,
- javatype/disj-50
is used by
okval-case,
- javatype/disj-51
is used by
okval-case,
- javatype/disj-52
is used by
okval-case,
- javatype/disj-53
is used by
okval-case,
- javatype/disj-54
is used by
okval-case,
- javatype/disj-55
is used by
okval-case,
- javatype/disj-56
is used by
okval-case,
- javatype/disj-57
is used by
okval-case,
- javatype/disj-58
is used by
okval-case,
- javatype/disj-59
is used by
okval-case,
- javatype/disj-60
is used by
okval-case,
- javatype/disj-61
is used by
okval-case,
- javatype/disj-62
is used by
okval-case,
- javatype/disj-63
is used by
okval-case,
- javatype/disj-64
is used by
okval-case,
- javatype/disj-65
is used by
okval-case,
- javatype/disj-66
is used by
okval-case,
- javatype/test-01
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-02
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-03
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-04
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-07
is used by
okval-case,
coerce-ref,
- javatype/test-08
is used by
okval-case,
coerce-ref,
- javatype/test-09
is used by
okval-case,
coerce-ref,
- javatype/test-10
is used by
okval-case,
coerce-ref,
- javatype/test-12
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-13
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-14
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-15
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-16
is used by
okval-case,
coerce-ref,
- javatype/test-18
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-19
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-20
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-21
is used by
okval-case,
okprim-class,
coerce-ref,
- javatype/test-22
is used by
okval-case,
coerce-ref,
- javatype/test-23
is used by
okval-case,
coerce-ref,
- javatype/test-26
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-27
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-31
is used by
okval-case,
okprim-array,
coerce-ref,
- javatype/test-32
is used by
okval-case,
okprim-array,
coerce-ref,
Used from specification javavalue
- javavalue/ex-02
is used by
noval-01,
- javavalue/ex-04
is used by
okval-refval-01,
- javavalue/concat-red
is used by
typeval,
throw,
stringval,
shortval,
return,
refval,
noval,
intval,
initval,
flatten-char,
continue,
byteval,
break,
boolval,
- javavalue/diff-02
is used by
okval-case,
- javavalue/diff-03
is used by
okval-case,
- javavalue/diff-04
is used by
okval-case,
- javavalue/diff-06
is used by
okval-case,
- javavalue/diff-07
is used by
okval-case,
- javavalue/diff-08
is used by
okval-case,
- javavalue/diff-09
is used by
okval-case,
- javavalue/diff-14
is used by
okval-case,
- javavalue/diff-15
is used by
okval-case,
- javavalue/diff-18
is used by
okval-case,
- javavalue/disj-01
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-05
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-125
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-126
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-127
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-150
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-19
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-42
is used by
noval-01,
- javavalue/disj-64
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/disj-74
is used by
initval-ref,
initial-value-02,
initial-value,
- javavalue/elim-02
is used by
val2int-int-01,
- javavalue/elim-11
is used by
refin-not-11,
- javavalue/elim-12
is used by
refin-not-12,
- javavalue/elim-13
is used by
refp-01,
refin-not-04,
- javavalue/ex-01
is used by
refin-not-06,
- javavalue/inj-02
is used by
base-boolval,
- javavalue/inj-03
is used by
initval-ref,
initial-value-02,
initial-value,
base-refval,
- javavalue/inj-04
is used by
incdec-int,
base-intval,
- javavalue/inj-05
is used by
base-continue,
- javavalue/inj-06
is used by
base-break,
- javavalue/inj-07
is used by
incdec-byte-01,
base-byteval,
- javavalue/inj-08
is used by
incdec-short-01,
base-shortval,
- javavalue/inj-09
is used by
base-typeval,
- javavalue/inj-12
is used by
base-initval,
- javavalue/inj-13
is used by
base-stringval,
- javavalue/sel-04
is used by
incdec-int,
- javavalue/sel-08
is used by
incdec-byte-01,
- javavalue/sel-09
is used by
refp-02,
- javavalue/sel-16
is used by
incdec-short-01,
- javavalue/test-01
is used by
refin-not,
okval-noval,
- javavalue/test-02
is used by
okval-noval,
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-03
is used by
refin-not-03,
okval-noval,
- javavalue/test-04
is used by
noval,
base-noval,
- javavalue/test-07
is used by
refin-not,
- javavalue/test-08
is used by
boolval,
base-boolval,
- javavalue/test-09
is used by
refval,
base-refval,
- javavalue/test-10
is used by
intval,
base-intval,
- javavalue/test-101
is used by
refin-not,
- javavalue/test-102
is used by
refin-not,
- javavalue/test-105
is used by
refin-not-03,
- javavalue/test-106
is used by
refin-not-03,
- javavalue/test-107
is used by
return,
base-return,
- javavalue/test-108
is used by
throw,
base-throw,
- javavalue/test-111
is used by
refin-not-07,
- javavalue/test-112
is used by
refin-not-07,
- javavalue/test-113
is used by
refin-not-09,
- javavalue/test-114
is used by
refin-not-09,
- javavalue/test-115
is used by
refin-not-10,
- javavalue/test-116
is used by
refin-not-10,
- javavalue/test-121
is used by
refin-not-02,
- javavalue/test-122
is used by
refin-not-02,
- javavalue/test-123
is used by
refin-not-02,
okval-noval,
- javavalue/test-124
is used by
refin-not-02,
- javavalue/test-125
is used by
refin-not-02,
- javavalue/test-126
is used by
refin-not-02,
- javavalue/test-127
is used by
refin-not-02,
- javavalue/test-128
is used by
refin-not-02,
- javavalue/test-129
is used by
refin-not-02,
- javavalue/test-13
is used by
refin-not-03,
initial-okval,
coerce-okval,
- javavalue/test-130
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-131
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-133
is used by
refin-not-03,
- javavalue/test-134
is used by
refin-not-03,
- javavalue/test-135
is used by
refin-not-03,
- javavalue/test-136
is used by
byteval,
base-byteval,
- javavalue/test-137
is used by
shortval,
base-shortval,
- javavalue/test-138
is used by
initval,
base-initval,
- javavalue/test-14
is used by
refin-not-03,
okval-refval,
okprimtype-refval,
- javavalue/test-142
is used by
refin-not-07,
- javavalue/test-143
is used by
refin-not-07,
- javavalue/test-144
is used by
refin-not-07,
- javavalue/test-145
is used by
refin-not-08,
- javavalue/test-146
is used by
refin-not-08,
- javavalue/test-147
is used by
refin-not-08,
- javavalue/test-148
is used by
refin-not-08,
- javavalue/test-149
is used by
refin-not-08,
- javavalue/test-15
is used by
refin-not-03,
- javavalue/test-150
is used by
refin-not-08,
- javavalue/test-151
is used by
refin-not-08,
- javavalue/test-152
is used by
refin-not-08,
- javavalue/test-153
is used by
refin-not-08,
- javavalue/test-154
is used by
refin-not-08,
- javavalue/test-155
is used by
refin-not-08,
- javavalue/test-156
is used by
refin-not-08,
- javavalue/test-157
is used by
refin-not-08,
- javavalue/test-158
is used by
refin-not-09,
- javavalue/test-159
is used by
refin-not-09,
- javavalue/test-160
is used by
refin-not-09,
- javavalue/test-161
is used by
refin-not-10,
- javavalue/test-162
is used by
refin-not-10,
- javavalue/test-163
is used by
refin-not-10,
- javavalue/test-170
is used by
refin-not,
- javavalue/test-171
is used by
refin-not-01,
- javavalue/test-172
is used by
refin-not-02,
- javavalue/test-174
is used by
refin-not-03,
- javavalue/test-175
is used by
refin-not-05,
- javavalue/test-176
is used by
refin-not-05,
- javavalue/test-177
is used by
refin-not-05,
- javavalue/test-178
is used by
refin-not-05,
- javavalue/test-179
is used by
refin-not-05,
- javavalue/test-18
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-180
is used by
refin-not-05,
- javavalue/test-181
is used by
refin-not-05,
- javavalue/test-182
is used by
refin-not-05,
- javavalue/test-183
is used by
refin-not-05,
- javavalue/test-184
is used by
refin-not-05,
- javavalue/test-185
is used by
refin-not-05,
- javavalue/test-186
is used by
refin-not-05,
- javavalue/test-187
is used by
refin-not-05,
- javavalue/test-188
is used by
refin-not-05,
- javavalue/test-189
is used by
stringval,
base-stringval,
- javavalue/test-19
is used by
refp-02,
okval-refval,
initial-value-01,
initial-okval,
coerce-ref,
- javavalue/test-191
is used by
refin-not-07,
- javavalue/test-192
is used by
refin-not-08,
- javavalue/test-193
is used by
refin-not-09,
- javavalue/test-194
is used by
refin-not-10,
- javavalue/test-197
is used by
refin-not,
- javavalue/test-198
is used by
refin-not,
- javavalue/test-199
is used by
refin-not,
- javavalue/test-20
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-200
is used by
refin-not-01,
- javavalue/test-201
is used by
refin-not-01,
- javavalue/test-202
is used by
refin-not-01,
- javavalue/test-203
is used by
refin-not-02,
- javavalue/test-204
is used by
refin-not-02,
- javavalue/test-205
is used by
refin-not-02,
- javavalue/test-206
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-207
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-208
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-209
is used by
refin-not-03,
- javavalue/test-210
is used by
refin-not-03,
- javavalue/test-211
is used by
refin-not-03,
- javavalue/test-215
is used by
okval-refval,
okprimtype-refval,
- javavalue/test-217
is used by
initial-okval,
coerce-okval,
- javavalue/test-22
is used by
refin-not-03,
- javavalue/test-222
is used by
okval-noval,
- javavalue/test-23
is used by
refin-not,
- javavalue/test-232
is used by
okval-refval,
okprimtype-refval,
- javavalue/test-235
is used by
initial-okval,
coerce-okval,
- javavalue/test-239
is used by
okval-noval,
- javavalue/test-24
is used by
refin-not,
okval-refval,
okprimtype-refval,
- javavalue/test-249
is used by
okval-refval,
okprimtype-refval,
- javavalue/test-25
is used by
refin-not,
initial-okval,
coerce-okval,
- javavalue/test-253
is used by
initial-okval,
coerce-okval,
- javavalue/test-256
is used by
okval-noval,
- javavalue/test-26
is used by
refin-not,
- javavalue/test-263
is used by
refin-not-05,
- javavalue/test-264
is used by
refin-not-05,
- javavalue/test-265
is used by
refin-not-05,
- javavalue/test-266
is used by
flatten-long,
- javavalue/test-267
is used by
flatten-float,
- javavalue/test-268
is used by
flatten-double,
- javavalue/test-272
is used by
refin-not-07,
- javavalue/test-273
is used by
refin-not-07,
- javavalue/test-274
is used by
refin-not-07,
- javavalue/test-275
is used by
refin-not-08,
- javavalue/test-276
is used by
refin-not-08,
- javavalue/test-277
is used by
refin-not-08,
- javavalue/test-278
is used by
refin-not-09,
- javavalue/test-279
is used by
refin-not-09,
- javavalue/test-28
is used by
refin-not,
- javavalue/test-280
is used by
refin-not-09,
- javavalue/test-281
is used by
refin-not-10,
- javavalue/test-282
is used by
refin-not-10,
- javavalue/test-283
is used by
refin-not-10,
- javavalue/test-29
is used by
refin-not,
- javavalue/test-290
is used by
refin-not,
- javavalue/test-291
is used by
refin-not-01,
- javavalue/test-292
is used by
refin-not-02,
- javavalue/test-293
is used by
initial-value-01,
initial-value,
coerce-ref,
- javavalue/test-294
is used by
refin-not-03,
- javavalue/test-298
is used by
okval-refval,
okprimtype-refval,
- javavalue/test-30
is used by
refin-not,
- javavalue/test-300
is used by
initial-okval,
coerce-okval,
- javavalue/test-306
is used by
okval-noval,
- javavalue/test-316
is used by
refin-not-05,
- javavalue/test-317
is used by
flatten-char,
- javavalue/test-319
is used by
refin-not-07,
- javavalue/test-32
is used by
refin-not,
- javavalue/test-320
is used by
refin-not-08,
- javavalue/test-321
is used by
refin-not-09,
- javavalue/test-322
is used by
refin-not-10,
- javavalue/test-33
is used by
refin-not-01,
incdec-int,
- javavalue/test-36
is used by
refin-not-01,
initial-okval,
incdec-byte-01,
coerce-okval,
- javavalue/test-37
is used by
refin-not-01,
- javavalue/test-40
is used by
refin-not-01,
okval-refval,
okprimtype-refval,
- javavalue/test-41
is used by
refin-not-01,
- javavalue/test-42
is used by
refin-not-03,
- javavalue/test-43
is used by
refin-not-10,
- javavalue/test-44
is used by
refin-not-01,
- javavalue/test-45
is used by
refin-not-01,
okval-noval,
- javavalue/test-46
is used by
refin-not-09,
- javavalue/test-47
is used by
refin-not-09,
- javavalue/test-48
is used by
refin-not-09,
- javavalue/test-49
is used by
refin-not-10,
- javavalue/test-50
is used by
refin-not-09,
- javavalue/test-51
is used by
refin-not-03,
- javavalue/test-52
is used by
refin-not-10,
- javavalue/test-53
is used by
refin-not-01,
- javavalue/test-54
is used by
refin-not-01,
- javavalue/test-55
is used by
refin-not-10,
- javavalue/test-56
is used by
refin-not-10,
- javavalue/test-57
is used by
refin-not-10,
- javavalue/test-58
is used by
typeval,
throw,
shortval,
return,
refval,
noval-01,
noval,
flatten-char,
exlist,
byteval,
- javavalue/test-59
is used by
refin-not-10,
- javavalue/test-60
is used by
break,
base-break,
- javavalue/test-61
is used by
refin-not-09,
- javavalue/test-62
is used by
refin-not-01,
- javavalue/test-63
is used by
refin-not-01,
- javavalue/test-67
is used by
refin-not-09,
- javavalue/test-69
is used by
continue,
base-continue,
- javavalue/test-70
is used by
refin-not-09,
- javavalue/test-71
is used by
refin-not-01,
- javavalue/test-72
is used by
refin-not-01,
- javavalue/test-79
is used by
refin-not-07,
- javavalue/test-80
is used by
refin-not-02,
incdec-int,
- javavalue/test-81
is used by
refin-not-02,
- javavalue/test-82
is used by
refin-not,
- javavalue/test-84
is used by
refin-not-03,
- javavalue/test-85
is used by
typeval,
base-typeval,
- javavalue/test-87
is used by
refin-not-07,
- javavalue/test-88
is used by
refin-not-07,
- javavalue/test-89
is used by
refin-not-07,
- javavalue/test-90
is used by
refin-not-07,
- javavalue/test-91
is used by
refin-not-07,
- javavalue/test-92
is used by
refin-not-07,
- javavalue/test-94
is used by
refin-not-07,
- javavalue/test-95
is used by
refin-not-02,
initial-okval,
incdec-short-01,
coerce-okval,
- javavalue/test-96
is used by
refin-not-02,
okval-refval,
okprimtype-refval,
- javavalue/test-97
is used by
refin-not-09,
- javavalue/test-98
is used by
refin-not-10,
- javavalue/typeval
is used by
typeval-06,
typeval-05,
typeval-04,
typeval-03,
typeval-02,
typeval-01,