[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,
Theorem base summary for Specification javavalue
- Status: unproved.
- Axioms: 551,
User Theorems:
(Proved: 37,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 65,
Interactions: 6
| byteval(1,0) | disj-121(0,0) | disj-39(0,0) | disj-98(0,0) | inj-17(0,0) | test-120(0,0) | test-174(0,0) | test-228(0,0) | test-281(0,0) | test-44(0,0) |
| case(0,0) | disj-122(0,0) | disj-40(0,0) | disj-99(0,0) | inj-strong(1,0) | test-121(0,0) | test-175(0,0) | test-229(0,0) | test-282(0,0) | test-45(0,0) |
| concat-red(1,0) | disj-123(0,0) | disj-41(0,0) | elim-01(0,0) | int2bytes-shortval(10,5) | test-122(0,0) | test-176(0,0) | test-23(0,0) | test-283(0,0) | test-46(0,0) |
| concat-red-01(1,0) | disj-124(0,0) | disj-42(0,0) | elim-02(0,0) | intval(1,0) | test-123(0,0) | test-177(0,0) | test-230(0,0) | test-284(0,0) | test-47(0,0) |
| diff(2,1) | disj-125(0,0) | disj-43(0,0) | elim-03(0,0) | refva-sel(2,0) | test-124(0,0) | test-178(0,0) | test-231(0,0) | test-285(0,0) | test-48(0,0) |
| diff-01(2,0) | disj-126(0,0) | disj-44(0,0) | elim-04(0,0) | refval(1,0) | test-125(0,0) | test-179(0,0) | test-232(0,0) | test-286(0,0) | test-49(0,0) |
| diff-02(1,0) | disj-127(0,0) | disj-45(0,0) | elim-05(0,0) | sel-01(0,0) | test-126(0,0) | test-18(0,0) | test-233(0,0) | test-287(0,0) | test-50(0,0) |
| diff-03(1,0) | disj-128(0,0) | disj-46(0,0) | elim-06(0,0) | sel-02(0,0) | test-127(0,0) | test-180(0,0) | test-234(0,0) | test-288(0,0) | test-51(0,0) |
| diff-04(1,0) | disj-129(0,0) | disj-47(0,0) | elim-07(0,0) | sel-03(0,0) | test-128(0,0) | test-181(0,0) | test-235(0,0) | test-289(0,0) | test-52(0,0) |
| diff-05(1,0) | disj-13(0,0) | disj-48(0,0) | elim-08(0,0) | sel-04(0,0) | test-129(0,0) | test-182(0,0) | test-236(0,0) | test-29(0,0) | test-53(0,0) |
| diff-06(1,0) | disj-130(0,0) | disj-49(0,0) | elim-09(0,0) | sel-05(0,0) | test-13(0,0) | test-183(0,0) | test-237(0,0) | test-290(0,0) | test-54(0,0) |
| diff-07(1,0) | disj-131(0,0) | disj-50(0,0) | elim-10(0,0) | sel-06(0,0) | test-130(0,0) | test-184(0,0) | test-238(0,0) | test-291(0,0) | test-55(0,0) |
| diff-08(2,0) | disj-132(0,0) | disj-51(0,0) | elim-11(0,0) | sel-07(0,0) | test-131(0,0) | test-185(0,0) | test-239(0,0) | test-292(0,0) | test-56(0,0) |
| diff-09(1,0) | disj-133(0,0) | disj-52(0,0) | elim-12(0,0) | sel-08(0,0) | test-132(0,0) | test-186(0,0) | test-24(0,0) | test-293(0,0) | test-57(0,0) |
| diff-10(1,0) | disj-134(0,0) | disj-53(0,0) | elim-13(0,0) | sel-09(0,0) | test-133(0,0) | test-187(0,0) | test-240(0,0) | test-294(0,0) | test-58(0,0) |
| diff-11(1,0) | disj-135(0,0) | disj-54(0,0) | elim-14(0,0) | sel-10(0,0) | test-134(0,0) | test-188(0,0) | test-241(0,0) | test-295(0,0) | test-59(0,0) |
| diff-12(2,0) | disj-136(0,0) | disj-55(0,0) | elim-15(0,0) | sel-11(0,0) | test-135(0,0) | test-189(0,0) | test-242(0,0) | test-296(0,0) | test-60(0,0) |
| diff-13(2,0) | disj-137(0,0) | disj-56(0,0) | elim-16(0,0) | sel-12(0,0) | test-136(0,0) | test-19(0,0) | test-243(0,0) | test-297(0,0) | test-61(0,0) |
| diff-14(1,0) | disj-138(0,0) | disj-57(0,0) | elim-17(0,0) | sel-13(0,0) | test-137(0,0) | test-190(0,0) | test-244(0,0) | test-298(0,0) | test-62(0,0) |
| diff-15(2,0) | disj-139(0,0) | disj-58(0,0) | elim-refval(2,0) | sel-14(0,0) | test-138(0,0) | test-191(0,0) | test-245(0,0) | test-299(0,0) | test-63(0,0) |
| diff-16(2,0) | disj-14(0,0) | disj-59(0,0) | eqbyteval(1,0) | sel-15(0,0) | test-139(0,0) | test-192(0,0) | test-246(0,0) | test-30(0,0) | test-64(0,0) |
| diff-17(2,0) | disj-140(0,0) | disj-60(0,0) | eqrefval(2,0) | sel-16(0,0) | test-14(0,0) | test-193(0,0) | test-247(0,0) | test-300(0,0) | test-65(0,0) |
| diff-18(2,0) | disj-141(0,0) | disj-61(0,0) | eqrefval-01(2,0) | sel-17(0,0) | test-140(0,0) | test-194(0,0) | test-248(0,0) | test-301(0,0) | test-66(0,0) |
| diff-19(2,0) | disj-142(0,0) | disj-62(0,0) | eqtypeval(2,0) | sel-18(0,0) | test-141(0,0) | test-195(0,0) | test-249(0,0) | test-302(0,0) | test-67(0,0) |
| diff-20(2,0) | disj-143(0,0) | disj-63(0,0) | ex-01(0,0) | sel-19(0,0) | test-142(0,0) | test-196(0,0) | test-25(0,0) | test-303(0,0) | test-68(0,0) |
| diff-21(2,0) | disj-144(0,0) | disj-64(0,0) | ex-02(0,0) | sel-20(0,0) | test-143(0,0) | test-197(0,0) | test-250(0,0) | test-304(0,0) | test-69(0,0) |
| disj-01(0,0) | disj-145(0,0) | disj-65(0,0) | ex-03(0,0) | shortval-sel(2,0) | test-144(0,0) | test-198(0,0) | test-251(0,0) | test-305(0,0) | test-70(0,0) |
| disj-02(0,0) | disj-146(0,0) | disj-66(0,0) | ex-04(0,0) | test-01(0,0) | test-145(0,0) | test-199(0,0) | test-252(0,0) | test-306(0,0) | test-71(0,0) |
| disj-03(0,0) | disj-147(0,0) | disj-67(0,0) | ex-05(0,0) | test-02(0,0) | test-146(0,0) | test-20(0,0) | test-253(0,0) | test-307(0,0) | test-72(0,0) |
| disj-04(0,0) | disj-148(0,0) | disj-68(0,0) | ex-06(0,0) | test-03(0,0) | test-147(0,0) | test-200(0,0) | test-254(0,0) | test-308(0,0) | test-73(0,0) |
| disj-05(0,0) | disj-149(0,0) | disj-69(0,0) | ex-07(0,0) | test-04(0,0) | test-148(0,0) | test-201(0,0) | test-255(0,0) | test-309(0,0) | test-74(0,0) |
| disj-06(0,0) | disj-15(0,0) | disj-70(0,0) | ex-08(0,0) | test-05(0,0) | test-149(0,0) | test-202(0,0) | test-256(0,0) | test-31(0,0) | test-75(0,0) |
| disj-07(0,0) | disj-150(0,0) | disj-71(0,0) | ex-09(0,0) | test-06(0,0) | test-15(0,0) | test-203(0,0) | test-257(0,0) | test-310(0,0) | test-76(0,0) |
| disj-08(0,0) | disj-151(0,0) | disj-72(0,0) | ex-10(0,0) | test-07(0,0) | test-150(0,0) | test-204(0,0) | test-258(0,0) | test-311(0,0) | test-77(0,0) |
| disj-09(0,0) | disj-152(0,0) | disj-73(0,0) | ex-11(0,0) | test-08(0,0) | test-151(0,0) | test-205(0,0) | test-259(0,0) | test-312(0,0) | test-78(0,0) |
| disj-10(0,0) | disj-153(0,0) | disj-74(0,0) | ex-12(0,0) | test-09(0,0) | test-152(0,0) | test-206(0,0) | test-26(0,0) | test-313(0,0) | test-79(0,0) |
| disj-100(0,0) | disj-16(0,0) | disj-75(0,0) | ex-13(0,0) | test-10(0,0) | test-153(0,0) | test-207(0,0) | test-260(0,0) | test-314(0,0) | test-80(0,0) |
| disj-101(0,0) | disj-17(0,0) | disj-76(0,0) | ex-14(0,0) | test-100(0,0) | test-154(0,0) | test-208(0,0) | test-261(0,0) | test-315(0,0) | test-81(0,0) |
| disj-102(0,0) | disj-18(0,0) | disj-77(0,0) | ex-15(0,0) | test-101(0,0) | test-155(0,0) | test-209(0,0) | test-262(0,0) | test-316(0,0) | test-82(0,0) |
| disj-103(0,0) | disj-19(0,0) | disj-78(0,0) | ex-16(0,0) | test-102(0,0) | test-156(0,0) | test-21(0,0) | test-263(0,0) | test-317(0,0) | test-83(0,0) |
| disj-104(0,0) | disj-20(0,0) | disj-79(0,0) | ex-17(0,0) | test-103(0,0) | test-157(0,0) | test-210(0,0) | test-264(0,0) | test-318(0,0) | test-84(0,0) |
| disj-105(0,0) | disj-21(0,0) | disj-80(0,0) | ex-18(0,0) | test-104(0,0) | test-158(0,0) | test-211(0,0) | test-265(0,0) | test-319(0,0) | test-85(0,0) |
| disj-106(0,0) | disj-22(0,0) | disj-81(0,0) | gen(0,0) | test-105(0,0) | test-159(0,0) | test-212(0,0) | test-266(0,0) | test-32(0,0) | test-86(0,0) |
| disj-107(0,0) | disj-23(0,0) | disj-82(0,0) | inj-01(0,0) | test-106(0,0) | test-16(0,0) | test-213(0,0) | test-267(0,0) | test-320(0,0) | test-87(0,0) |
| disj-108(0,0) | disj-24(0,0) | disj-83(0,0) | inj-02(0,0) | test-107(0,0) | test-160(0,0) | test-214(0,0) | test-268(0,0) | test-321(0,0) | test-88(0,0) |
| disj-109(0,0) | disj-25(0,0) | disj-84(0,0) | inj-03(0,0) | test-108(0,0) | test-161(0,0) | test-215(0,0) | test-269(0,0) | test-322(0,0) | test-89(0,0) |
| disj-11(0,0) | disj-26(0,0) | disj-85(0,0) | inj-04(0,0) | test-109(0,0) | test-162(0,0) | test-216(0,0) | test-27(0,0) | test-323(0,0) | test-90(0,0) |
| disj-110(0,0) | disj-27(0,0) | disj-86(0,0) | inj-05(0,0) | test-11(0,0) | test-163(0,0) | test-217(0,0) | test-270(0,0) | test-324(0,0) | test-91(0,0) |
| disj-111(0,0) | disj-28(0,0) | disj-87(0,0) | inj-06(0,0) | test-110(0,0) | test-164(0,0) | test-218(0,0) | test-271(0,0) | test-33(0,0) | test-92(0,0) |
| disj-112(0,0) | disj-29(0,0) | disj-88(0,0) | inj-07(0,0) | test-111(0,0) | test-165(0,0) | test-219(0,0) | test-272(0,0) | test-34(0,0) | test-93(0,0) |
| disj-113(0,0) | disj-30(0,0) | disj-89(0,0) | inj-08(0,0) | test-112(0,0) | test-166(0,0) | test-22(0,0) | test-273(0,0) | test-35(0,0) | test-94(0,0) |
| disj-114(0,0) | disj-31(0,0) | disj-90(0,0) | inj-09(0,0) | test-113(0,0) | test-167(0,0) | test-220(0,0) | test-274(0,0) | test-36(0,0) | test-95(0,0) |
| disj-115(0,0) | disj-32(0,0) | disj-91(0,0) | inj-10(0,0) | test-114(0,0) | test-168(0,0) | test-221(0,0) | test-275(0,0) | test-37(0,0) | test-96(0,0) |
| disj-116(0,0) | disj-33(0,0) | disj-92(0,0) | inj-11(0,0) | test-115(0,0) | test-169(0,0) | test-222(0,0) | test-276(0,0) | test-38(0,0) | test-97(0,0) |
| disj-117(0,0) | disj-34(0,0) | disj-93(0,0) | inj-12(0,0) | test-116(0,0) | test-17(0,0) | test-223(0,0) | test-277(0,0) | test-39(0,0) | test-98(0,0) |
| disj-118(0,0) | disj-35(0,0) | disj-94(0,0) | inj-13(0,0) | test-117(0,0) | test-170(0,0) | test-224(0,0) | test-278(0,0) | test-40(0,0) | test-99(0,0) |
| disj-119(0,0) | disj-36(0,0) | disj-95(0,0) | inj-14(0,0) | test-118(0,0) | test-171(0,0) | test-225(0,0) | test-279(0,0) | test-41(0,0) | typeval(2,0) |
| disj-12(0,0) | disj-37(0,0) | disj-96(0,0) | inj-15(0,0) | test-119(0,0) | test-172(0,0) | test-226(0,0) | test-28(0,0) | test-42(0,0) |
| disj-120(0,0) | disj-38(0,0) | disj-97(0,0) | inj-16(0,0) | test-12(0,0) | test-173(0,0) | test-227(0,0) | test-280(0,0) | test-43(0,0) |