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