forked from jsiek/deduce
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Set.thm
28 lines (15 loc) · 1.12 KB
/
Set.thm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
This file was automatically generated by Deduce.
This file summarizes the theorems proved in the file:
Set.pf
single_member: (all T:type. (all x:T. x ∈ single(x)))
single_equal: (all T:type. (all x:T, y:T. (if y ∈ single(x) then x = y)))
empty_no_members: (all T:type. (all x:T. not (x ∈ char_fun(λ_{false}))))
union_member: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (if (x ∈ A or x ∈ B) then x ∈ A ∪ B)))
member_union: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (if x ∈ A ∪ B then (x ∈ A or x ∈ B))))
union_empty: (all T:type. (all A:Set<T>. A ∪ char_fun(λ_{false}) = A))
empty_union: (all T:type. (all A:Set<T>. @char_fun<T>(λx{false}) ∪ A = A))
union_sym: (all T:type. (all A:Set<T>, B:Set<T>. A ∪ B = B ∪ A))
union_assoc: (all T:type. (all A:Set<T>, B:Set<T>, C:Set<T>. A ∪ B ∪ C = A ∪ B ∪ C))
in_left_union: (all T:type. (all B:Set<T>. (all x:T, A:Set<T>. (if x ∈ A then x ∈ A ∪ B))))
in_right_union: (all T:type. (all A:Set<T>. (all x:T, B:Set<T>. (if x ∈ B then x ∈ A ∪ B))))
subset_equal: (all T:type. (all A:Set<T>, B:Set<T>. (if (A ⊆ B and B ⊆ A) then A = B)))