A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| union-split3 | proved | all subs proved
| uni-ac3-true,
uni-inj,
uni-ass,
disj-com-rw,
union-split2,
disj-distr-uni-com,
disj-distr-uni,
|
| union-split2 | proved | all subs proved
| uni-ac3-true,
uni-inj,
uni-ass,
disj,
disj-l,
disj-diffb,
disj-com-rw,
uni-com,
diff-at,
at-uni,
disj-r,
diff-in,
subset-union,
disj-union-diff,
in-uni,
disj-distr-uni,
disj-distr-uni-com,
|
| uni-acall-true | proved | all subs proved
| uni-ass-true,
disj-com-rw,
disj-distr-uni-com,
uni-com,
|
| uni-ac2-true | proved | all subs proved
| uni-ass-true,
disj-com-rw,
disj-distr-uni-com,
uni-com,
|
| uni-ass-true | proved | all subs proved
| uni-ass,
|
| uni-ac3-true | proved | all subs proved
| uni-ac1-true,
uni-ass,
disj-com-rw,
disj-distr-uni-com,
uni-com,
|
| uni-ac1-true | proved | all subs proved
| uni-com-true,
disj-com-rw,
disj-distr-uni,
uni-inj,
|
| uni-ass | proved | all subs proved
| disj-l,
disj-r,
at-uni,
disj-distr-uni,
disj-com-rw,
disj-distr-uni-com,
in-uni,
|
| subset-uni | proved | all subs proved
| subset-union2,
disj,
diff-in,
diff-at,
disj-l,
at-uni,
in-uni,
uni-com,
|
| union-diff1 | proved | all subs proved
| uni-emp-l,
disj-diff-id2,
same-diff-empty,
union-diff-distr,
|
| union-diff2 | proved | all subs proved
| uni-emp,
same-diff-empty,
disj-diff-id1,
union-diff-distr,
|
| union-diff-distr | proved | all subs proved
| disj-l,
disj-diffb,
at-uni,
diff-at,
in-uni,
diff-in,
|
| uni-emp-l | proved | all subs proved
| uni-emp,
disj-emp-r,
uni-com,
|
| subset-union2 | proved | all subs proved
| disj-com-rw,
subset-union,
|
| uni-com-true | proved | all subs proved
| uni-com,
|
| disj-distr-uni-com | proved | all subs proved
| disj-distr-uni,
disj-com,
|
| union-add-singleton-left | proved | all subs proved
| union-add-singleton-right,
disj-emp-r,
disj-write,
uni-com,
|
| write-left | proved | all subs proved
| uni-put,
disj-com-rw,
disj-r,
disj,
uni-com,
|
| disj-com | proved | all subs proved
| disj-com-rw,
|
| disj-union-diff | proved | all subs proved
| at-uni,
in-uni,
diff-in,
disj,
|
| subset-union | proved | all subs proved
| at-uni,
in-uni,
|
| uni-com | proved | all subs proved
| disj-l,
at-uni,
disj-com-rw,
in-uni,
|
| disj-diffb | proved | all subs proved
| disj-diffl,
disj-diffr,
|
| uni-inj | proved | all subs proved
| disj-r,
disj-l,
at-uni,
in-uni,
|
| union-left-singleton-at | proved | all subs proved
| disj-singleton-write,
in-uni,
at-uni,
|
| union-left-singleton | proved | all subs proved
| at-uni,
disj-singleton-write,
in-uni,
|
| del-uni | proved | all subs proved
| disj-r,
disj-rem,
at-uni,
in-uni,
|
| disj-rem | proved | all subs proved
| disj-l,
disj,
|
| disj-diff-id1 | proved | all subs proved
| diff-at,
disj-l,
diff-in,
|
| disj-diffr | proved | all subs proved
| disj-l,
diff-in,
disj,
|
| disj-distr-uni | proved | all subs proved
| disj-r,
disj-l,
in-uni,
disj,
|
| at-uni | proved | all subs proved
| disj-write,
uni-put,
disj-emp-r,
uni-emp,
in-uni,
|
| disj-com-rw | proved | all subs proved
| disj-l,
disj,
|
| delswr | proved | all subs proved
| diffs-sw,
diffs-ins,
|
| size-uni | proved | all subs proved
| in-uni,
disj-write,
size-put,
uni-put,
uni-emp,
|
| diff-size | proved | all subs proved
| rm-size,
diffs-sw,
in-diffs,
diffs-ins,
diffs-emp,
|
| same-diff-empty | proved | all subs proved
| diff-in,
|
| disj-diff-id2 | proved | all subs proved
| diff-at,
disj-r,
diff-in,
|
| diffs-sw | proved | all subs proved
| at-diffs,
in-diffs,
|
| union-add-singleton-right | proved | all subs proved
| uni-emp,
uni-put,
disj-emp-r,
|
| disj-diffl | proved | all subs proved
| disj-r,
diff-in,
disj,
|
| disj-write | proved | all subs proved
| disj,
disj-add,
|
| disj-l | proved | all subs proved
| disj-r,
|
| disj-diff | proved | all subs proved
| diff-in,
disj,
|
| exin-uni | proved | all subs proved
| uni-emp,
uni-put,
disj-emp-r,
|
| subset-diffempty | proved | all subs proved
| diff-in,
|
| sw-del-add-new | proved | all subs proved
| at-diffs,
in-diffs,
|
| disj-diff-same | proved | all subs proved
| diff-in,
disj,
|
| diffs-twice | proved | all subs proved
| at-diffs,
in-diffs,
|
| disj-singleton-write | proved | all subs proved
| disj,
|
| in-diffs | proved | all subs proved
| diffs-ins,
diffs-emp,
|
| at-diffs | proved | all subs proved
| diffs-ins,
diffs-emp,
|
| disj-add | proved | all subs proved
| disj,
|
| disj-emp-r | proved | all subs proved
| disj,
|
| in-uni | proved | all subs proved
| disj,
uni-put,
uni-emp,
|
| diff-in | proved | all subs proved
| diff-put,
diff-emp,
|
| disj-r | proved | all subs proved
| disj,
|
| diff-at | proved | all subs proved
| diff-put,
diff-emp,
|
| write-right | proved | all subs proved
| uni-put,
|
| sw-delswr | proved | all subs proved
| sw-delwr,
diffs-ins,
diffs-emp,
|
| disj-emp-l | proved | all subs proved
| disj,
|
| sw-delwr | proved | all subs proved
| |
| rm-size | proved | all subs proved
| |
| size-put | proved | all subs proved
| |
| diffs-emp | axiom | | |
| diffs-ins | axiom | | |
| uni-put | axiom | | |
| uni-emp | axiom | | |
| diff-emp | axiom | | |
| diff-put | axiom | | |
| disj | axiom | | |