[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 VF3conc
- Status: Proved!
- Axioms: 227,
User Theorems: 27
(Proved: 27,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 314,
Interactions: 117
| VF3concGInv(0,0) | disj-15(0,0) | disj-41(0,0) | elim-02(0,0) | lstep(0,0) | pre-L2(0,0) | sel-14(0,0) | upd-03(0,0) | updsel-16(0,0) | updsel-42(0,0) |
| VF3concInv(0,0) | disj-16(0,0) | disj-42(0,0) | elim-03(0,0) | lstepf-I-CMULT(0,0) | pre-L3(0,0) | sel-15(0,0) | upd-04(0,0) | updsel-17(0,0) | updsel-43(0,0) |
| VF3concLInv(0,0) | disj-17(0,0) | disj-43(0,0) | gen-01(0,0) | lstepf-L0(0,0) | pre-L4(0,0) | sel-16(0,0) | upd-05(0,0) | updsel-18(0,0) | updsel-44(0,0) |
| VF3concRely(0,0) | disj-18(0,0) | disj-44(0,0) | gen-02(0,0) | lstepf-L1(0,0) | pre-L5(0,0) | sel-17(0,0) | upd-06(0,0) | updsel-19(0,0) | updsel-45(0,0) |
| VF3concstep(0,0) | disj-19(0,0) | disj-45(0,0) | gen-03(0,0) | lstepf-L2-0(0,0) | pre-L6(0,0) | stable-L0(1,0) | upd-07(0,0) | updsel-20(0,0) | updsel-46(0,0) |
| alltids-all(0,0) | disj-20(0,0) | disj-46(0,0) | gen-04(0,0) | lstepf-L2-1(0,0) | pre-L7(0,0) | stable-L1(2,0) | upd-08(0,0) | updsel-21(0,0) | updsel-47(0,0) |
| alltids-nonempty(0,0) | disj-21(0,0) | disj-47(0,0) | gen-05(0,0) | lstepf-L3(0,0) | pre-L8(0,0) | stable-L3(2,0) | upd-09(0,0) | updsel-22(0,0) | updsel-48(0,0) |
| case-01(0,0) | disj-22(0,0) | disj-48(0,0) | gstepf-I(0,0) | lstepf-L4-0(0,0) | rely-L2-L1(8,1) | stable-L4(2,0) | upd-10(0,0) | updsel-23(0,0) | updsel-49(0,0) |
| case-02(0,0) | disj-23(0,0) | disj-49(0,0) | gstepf-L0(0,0) | lstepf-L4-1(0,0) | rely-L2-L3(2,0) | stable-L5(2,0) | upd-11(0,0) | updsel-24(0,0) | updsel-50(0,0) |
| case-03(0,0) | disj-24(0,0) | disj-50(0,0) | gstepf-L1(0,0) | lstepf-L5(0,0) | rely-L5-L6(2,0) | stable-L7-01(2,0) | upd-12(0,0) | updsel-25(0,0) | updsel-51(0,0) |
| case-04(0,0) | disj-25(0,0) | disj-51(0,0) | gstepf-L2-0(0,0) | lstepf-L6(0,0) | rely-L6-L3(2,0) | stable-L8(2,0) | upd-13(0,0) | updsel-26(0,0) | updsel-52(0,0) |
| case-05(0,0) | disj-26(0,0) | disj-52(0,0) | gstepf-L2-1(0,0) | lstepf-L7(0,0) | rely-L6-L7(2,0) | step-L1-L2(2,0) | updsel-01(0,0) | updsel-27(0,0) | updsel-53(0,0) |
| disj-01(0,0) | disj-27(0,0) | disj-53(0,0) | gstepf-L3(0,0) | lstepf-L8(0,0) | rely-reflexive(2,0) | step-L1-L7(2,0) | updsel-02(0,0) | updsel-28(0,0) | updsel-54(0,0) |
| disj-02(0,0) | disj-28(0,0) | disj-54(0,0) | gstepf-L4(0,0) | pcstepf-I-CMULT(0,0) | sel-01(0,0) | step-L1-L8(2,0) | updsel-03(0,0) | updsel-29(0,0) | updsel-55(0,0) |
| disj-03(0,0) | disj-29(0,0) | disj-55(0,0) | gstepf-L5(0,0) | pcstepf-L0(0,0) | sel-02(0,0) | step-L2-L1(7,1) | updsel-04(0,0) | updsel-30(0,0) | updsel-56(0,0) |
| disj-04(0,0) | disj-30(0,0) | disj-56(0,0) | gstepf-L6(0,0) | pcstepf-L1(0,0) | sel-03(0,0) | step-L2-L3(112,51) | updsel-05(0,0) | updsel-31(0,0) | updsel-57(0,0) |
| disj-05(0,0) | disj-31(0,0) | disj-57(0,0) | gstepf-L7(0,0) | pcstepf-L2(0,0) | sel-04(0,0) | step-L3-L1(2,0) | updsel-06(0,0) | updsel-32(0,0) | updsel-58(0,0) |
| disj-06(0,0) | disj-32(0,0) | disj-58(0,0) | gstepf-L8(0,0) | pcstepf-L3(0,0) | sel-05(0,0) | step-L3-L4(2,0) | updsel-07(0,0) | updsel-33(0,0) | updsel-59(0,0) |
| disj-07(0,0) | disj-33(0,0) | disj-59(0,0) | init(17,9) | pcstepf-L4(0,0) | sel-06(0,0) | step-L4-L0(11,2) | updsel-08(0,0) | updsel-34(0,0) | updsel-60(0,0) |
| disj-08(0,0) | disj-34(0,0) | disj-60(0,0) | inj-01(0,0) | pcstepf-L5(0,0) | sel-07(0,0) | step-L4-L5(2,0) | updsel-09(0,0) | updsel-35(0,0) | updsel-61(0,0) |
| disj-09(0,0) | disj-35(0,0) | disj-61(0,0) | inj-02(0,0) | pcstepf-L6(0,0) | sel-08(0,0) | step-L5-L6(2,0) | updsel-10(0,0) | updsel-36(0,0) |
| disj-10(0,0) | disj-36(0,0) | disj-62(0,0) | inj-03(0,0) | pcstepf-L7(0,0) | sel-09(0,0) | step-L6-L3(2,0) | updsel-11(0,0) | updsel-37(0,0) |
| disj-11(0,0) | disj-37(0,0) | disj-63(0,0) | inj-04(0,0) | pcstepf-L8(0,0) | sel-10(0,0) | step-L6-L7(118,53) | updsel-12(0,0) | updsel-38(0,0) |
| disj-12(0,0) | disj-38(0,0) | disj-64(0,0) | inj-05(0,0) | pre-I(0,0) | sel-11(0,0) | step-L7-L3(2,0) | updsel-13(0,0) | updsel-39(0,0) |
| disj-13(0,0) | disj-39(0,0) | disj-65(0,0) | inj-06(0,0) | pre-L0(0,0) | sel-12(0,0) | upd-01(0,0) | updsel-14(0,0) | updsel-40(0,0) |
| disj-14(0,0) | disj-40(0,0) | elim-01(0,0) | inj-07(0,0) | pre-L1(0,0) | sel-13(0,0) | upd-02(0,0) | updsel-15(0,0) | updsel-41(0,0) |