[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 infset-union
- Status: Proved!
- Axioms: 5,
User Theorems: 135
(Proved: 135,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 416,
Interactions: 36
| Delete(0,0) | del-addin-01(2,0) | del-in-03(1,0) | diff-del-01(2,0) | diff-union(2,0) | int-empty-02(3,0) | selsub-diff(8,4) | sub-union-03(1,0) | undel-03(2,0) | union-diff(2,0) |
| Difference(0,0) | del-d(1,0) | del-neq(2,0) | diff-del-02(2,0) | diff-union-01(2,0) | int-eq(2,0) | sub-ade(3,0) | sub-union-04(1,0) | undel-04(2,0) | union-difference(3,0) |
| Intersect(0,0) | del-d-01(1,0) | del-neq-01(3,0) | diff-e(1,0) | diff-union-02(3,1) | int-idem(1,0) | sub-ade-01(3,0) | sub-union-05(1,0) | undel-05(2,0) | union-one(2,0) |
| One(0,0) | del-del-one(2,0) | del-neq-02(3,1) | diff-e-01(1,0) | diff-union-03(4,2) | int-ins(10,2) | sub-ade-02(3,0) | subdef(5,1) | undel-06(1,0) | union-rewone(1,0) |
| Union(0,0) | del-e(11,0) | del-notin(2,0) | diff-empty(3,1) | equal-add-in(3,1) | int-inse(7,0) | sub-ade-03(3,0) | subset-del(1,0) | une(1,0) | union-sub(2,0) |
| del(1,1) | del-e-01(1,0) | del-two(25,0) | diff-idem(1,0) | ext(8,2) | int-inserte(3,0) | sub-del(3,0) | subsub-del(3,0) | une-01(14,1) | union-sub-01(3,0) |
| del-addeq(15,6) | del-e-02(11,0) | delete-insert(1,0) | diff-int(1,0) | indef(2,2) | int-notempty(3,0) | sub-del-01(3,0) | una(1,0) | uneq(2,0) | unrax(1,0) |
| del-addeq-01(1,0) | del-eq(17,0) | delete-subset(1,0) | diff-int-01(1,0) | insdel-sub(3,0) | int-notempty-01(3,0) | sub-del-02(1,0) | unadd(1,0) | unidem(1,0) | unsub(1,0) |
| del-addeq-02(2,0) | del-feq(5,2) | delsw(3,0) | diff-nin(2,0) | int-a(1,0) | int-subs01(1,0) | sub-del-03(3,0) | unadd-01(1,0) | unin(2,0) | unsub-union-01(26,0) |
| del-addeq-03(2,0) | del-feq-01(3,1) | delsw-01(1,0) | diff-one(1,0) | int-c(1,0) | intdel-empty(3,0) | sub-del-04(4,0) | unall(2,0) | unin-01(1,0) | unsubdel(7,0) |
| del-addeq-04(2,0) | del-feq-02(3,0) | delsw-02(1,0) | diff-rc(2,1) | int-del-rew(2,0) | intexin(3,0) | sub-del-05(2,0) | unc(1,0) | unindel(2,0) | unsubdel-01(2,0) |
| del-addeq-05(1,0) | del-in(2,0) | diff-add-del(2,1) | diff-sub(1,0) | int-e(1,0) | intu-empty(14,3) | sub-union(3,0) | undel(2,0) | uninsert(2,0) | unsubins(1,0) |
| del-addeq-06(1,0) | del-in-01(2,0) | diff-add-del-01(2,0) | diff-subset(1,0) | int-empty(3,0) | one-in(1,1) | sub-union-01(3,0) | undel-01(2,0) | uninsubdel(2,0) | unsubins-01(1,0) |
| del-addin(2,0) | del-in-02(2,0) | diff-del(5,2) | diff-subset-01(1,0) | int-empty-01(2,0) | one-min(2,0) | sub-union-02(1,0) | undel-02(2,0) | union-del(1,0) | unsubsub(7,0) |