Theory "HolSmt"

Parents     transc   Omega   int_arith   blast   bitstring

Signature

Constant Type
array_ext :(α -> β) -> (α -> β) -> α
xor :bool reln

Definitions

xor_def 
|- ∀x y. xor x y ⇔ (x ⇎ y)
array_ext_def 
|- ∀A B. array_ext A B = @i. A i ≠ B i

Theorems

ALL_DISTINCT_NIL 
|- ALL_DISTINCT [] ⇔ T
ALL_DISTINCT_CONS 
|- ∀h t. ALL_DISTINCT (h::t) ⇔ ¬MEM h t ∧ ALL_DISTINCT t
NOT_MEM_NIL 
|- ∀x. ¬MEM x [] ⇔ T
NOT_MEM_CONS 
|- ∀x h t. ¬MEM x (h::t) ⇔ x ≠ h ∧ ¬MEM x t
AND_T 
|- ∀p. p ∧ T ⇔ p
T_AND 
|- ∀p q. (T ∧ p ⇔ T ∧ q) ⇒ (p ⇔ q)
F_OR 
|- ∀p q. (F ∨ p ⇔ F ∨ q) ⇒ (p ⇔ q)
CONJ_CONG 
|- ∀p q r s. (p ⇔ q) ⇒ (r ⇔ s) ⇒ (p ∧ r ⇔ q ∧ s)
NOT_NOT_ELIM 
|- ∀p. ¬ ¬p ⇒ p
NOT_FALSE 
|- ∀p. p ⇒ ¬p ⇒ F
NNF_CONJ 
|- ∀p q r s. (¬p ⇔ r) ⇒ (¬q ⇔ s) ⇒ (¬(p ∧ q) ⇔ r ∨ s)
NNF_DISJ 
|- ∀p q r s. (¬p ⇔ r) ⇒ (¬q ⇔ s) ⇒ (¬(p ∨ q) ⇔ r ∧ s)
NNF_NOT_NOT 
|- ∀p q. (p ⇔ q) ⇒ (¬ ¬p ⇔ q)
NEG_IFF_1_1 
|- ∀p q. (q ⇔ p) ⇒ (p ⇎ ¬q)
NEG_IFF_1_2 
|- ∀p q. (p ⇎ ¬q) ⇒ (q ⇔ p)
NEG_IFF_2_1 
|- ∀p q. (p ⇔ ¬q) ⇒ (p ⇎ q)
NEG_IFF_2_2 
|- ∀p q. (p ⇎ q) ⇒ (p ⇔ ¬q)
DISJ_ELIM_1 
|- ∀p q r. (p ∨ q ⇒ r) ⇒ p ⇒ r
DISJ_ELIM_2 
|- ∀p q r. (p ∨ q ⇒ r) ⇒ q ⇒ r
IMP_DISJ_1 
|- ∀p q. (p ⇒ q) ⇒ ¬p ∨ q
IMP_DISJ_2 
|- ∀p q. (¬p ⇒ q) ⇒ p ∨ q
IMP_FALSE 
|- ∀p. (¬p ⇒ F) ⇒ p
AND_IMP_INTRO_SYM 
|- ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r
VALID_IFF_TRUE 
|- ∀p. p ⇒ (p ⇔ T)
d001 
|- (p ⇎ q) ∨ ¬p ∨ q
d002 
|- (p ⇎ q) ∨ p ∨ ¬q
d003 
|- (p ⇔ ¬q) ∨ ¬p ∨ q
d004 
|- (¬p ⇔ q) ∨ p ∨ ¬q
d005 
|- (p ⇔ q) ∨ ¬p ∨ ¬q
d006 
|- (p ⇔ q) ∨ p ∨ q
d007 
|- (¬p ⇎ q) ∨ p ∨ q
d008 
|- (p ⇎ ¬q) ∨ p ∨ q
d009 
|- ¬p ∨ q ∨ (p ⇎ q)
d010 
|- p ∨ ¬q ∨ (p ⇎ q)
d011 
|- p ∨ q ∨ (¬p ⇎ q)
d012 
|- p ∨ q ∨ (p ⇎ ¬q)
d013 
|- ¬p ∧ ¬q ∨ p ∨ q
d014 
|- ¬p ∧ q ∨ p ∨ ¬q
d015 
|- p ∧ ¬q ∨ ¬p ∨ q
d016 
|- p ∧ q ∨ ¬p ∨ ¬q
d017 
|- p ∨ (y = if p then x else y)
d018 
|- ¬p ∨ (x = if p then x else y)
d019 
|- p ∨ ((if p then x else y) = y)
d020 
|- ¬p ∨ ((if p then x else y) = x)
d021 
|- p ∨ q ∨ ¬if p then r else q
d022 
|- ¬p ∨ q ∨ ¬if p then q else r
d023 
|- (if p then q else r) ∨ ¬p ∨ ¬q
d024 
|- (if p then q else r) ∨ p ∨ ¬r
d025 
|- (if p then ¬q else r) ∨ ¬p ∨ q
d026 
|- (if p then q else ¬r) ∨ p ∨ r
d027 
|- ¬(if p then q else r) ∨ ¬p ∨ q
d028 
|- ¬(if p then q else r) ∨ p ∨ r
r001 
|- (x = y) ⇔ (y = x)
r002 
|- (x = x) ⇔ T
r003 
|- (p ⇔ T) ⇔ p
r004 
|- (T ⇔ p) ⇔ p
r005 
|- (p ⇔ F) ⇔ ¬p
r006 
|- (F ⇔ p) ⇔ ¬p
r007 
|- (¬p ⇔ ¬q) ⇔ (p ⇔ q)
r008 
|- (p ⇎ ¬q) ⇔ (p ⇔ q)
r009 
|- (¬p ⇎ q) ⇔ (p ⇔ q)
r010 
|- (if T then x else y) = x
r011 
|- (if F then x else y) = y
r012 
|- (if p then q else T) ⇔ ¬p ∨ q
r013 
|- (if p then q else T) ⇔ q ∨ ¬p
r014 
|- (if p then q else ¬q) ⇔ (p ⇔ q)
r015 
|- (if p then q else ¬q) ⇔ (q ⇔ p)
r016 
|- (if p then ¬q else q) ⇔ (p ⇔ ¬q)
r017 
|- (if p then ¬q else q) ⇔ (¬q ⇔ p)
r018 
|- (if ¬p then x else y) = if p then y else x
r019 
|- (if p then if q then x else y else x) = if p ∧ ¬q then y else x
r020 
|- (if p then if q then x else y else x) = if ¬q ∧ p then y else x
r021 
|- (if p then if q then x else y else y) = if p ∧ q then x else y
r022 
|- (if p then if q then x else y else y) = if q ∧ p then x else y
r023 
|- (if p then x else if p then y else z) = if p then x else z
r024 
|- (if p then x else if q then x else y) = if p ∨ q then x else y
r025 
|- (if p then x else if q then x else y) = if q ∨ p then x else y
r026 
|- (if p then x = y else (x = z)) ⇔ (x = if p then y else z)
r027 
|- (if p then x = y else (y = z)) ⇔ (y = if p then x else z)
r028 
|- (if p then x = y else (z = y)) ⇔ (y = if p then x else z)
r029 
|- ¬p ⇒ q ⇔ p ∨ q
r030 
|- ¬p ⇒ q ⇔ q ∨ p
r031 
|- p ⇒ q ⇔ ¬p ∨ q
r032 
|- p ⇒ q ⇔ q ∨ ¬p
r033 
|- T ⇒ p ⇔ p
r034 
|- p ⇒ T ⇔ T
r035 
|- F ⇒ p ⇔ T
r036 
|- p ⇒ p ⇔ T
r037 
|- (p ⇔ q) ⇒ r ⇔ r ∨ (q ⇔ ¬p)
r038 
|- ¬T ⇔ F
r039 
|- ¬F ⇔ T
r040 
|- ¬ ¬p ⇔ p
r041 
|- p ∨ q ⇔ q ∨ p
r042 
|- p ∨ T ⇔ T
r043 
|- p ∨ ¬p ⇔ T
r044 
|- ¬p ∨ p ⇔ T
r045 
|- T ∨ p ⇔ T
r046 
|- p ∨ F ⇔ p
r047 
|- F ∨ p ⇔ p
r048 
|- p ∧ q ⇔ q ∧ p
r049 
|- p ∧ T ⇔ p
r050 
|- T ∧ p ⇔ p
r051 
|- p ∧ F ⇔ F
r052 
|- F ∧ p ⇔ F
r053 
|- p ∧ q ⇔ ¬(¬p ∨ ¬q)
r054 
|- ¬p ∧ q ⇔ ¬(p ∨ ¬q)
r055 
|- p ∧ ¬q ⇔ ¬(¬p ∨ q)
r056 
|- ¬p ∧ ¬q ⇔ ¬(p ∨ q)
r057 
|- p ∧ q ⇔ ¬(¬q ∨ ¬p)
r058 
|- ¬p ∧ q ⇔ ¬(¬q ∨ p)
r059 
|- p ∧ ¬q ⇔ ¬(q ∨ ¬p)
r060 
|- ¬p ∧ ¬q ⇔ ¬(q ∨ p)
r061 
|- (x =+ f x) f = f
r062 
|- ALL_DISTINCT [x; x] ⇔ F
r063 
|- ALL_DISTINCT [x; y] ⇔ x ≠ y
r064 
|- ALL_DISTINCT [x; y] ⇔ y ≠ x
r065 
|- (x = y) ⇔ (x + -1 * y = 0)
r066 
|- (x = y + z) ⇔ (x + -1 * z = y)
r067 
|- (x = y + -1 * z) ⇔ (x + (-1 * y + z) = 0)
r068 
|- (x = -1 * y + z) ⇔ (y + (-1 * z + x) = 0)
r069 
|- (x = y + z) ⇔ (x + (-1 * y + -1 * z) = 0)
r070 
|- (x = y + z) ⇔ (y + (z + -1 * x) = 0)
r071 
|- (x = y + z) ⇔ (y + (-1 * x + z) = 0)
r072 
|- (x = y + z) ⇔ (z + -1 * x = -y)
r073 
|- (x = -y + z) ⇔ (z + -1 * x = y)
r074 
|- (-1 * x = -y) ⇔ (x = y)
r075 
|- (-1 * x + y = z) ⇔ (x + -1 * y = -z)
r076 
|- (x + y = 0) ⇔ (y = -x)
r077 
|- (x + y = z) ⇔ (y + -1 * z = -x)
r078 
|- (a + (-1 * x + (v * y + w * z)) = 0) ⇔ (x + (-v * y + -w * z) = a)
r079 
|- 0 + x = x
r080 
|- x + 0 = x
r081 
|- x + y = y + x
r082 
|- x + x = 2 * x
r083 
|- x + y + z = x + (y + z)
r084 
|- x + y + z = x + (z + y)
r085 
|- x + (y + z) = y + (z + x)
r086 
|- x + (y + z) = y + (x + z)
r087 
|- x + (y + (z + u)) = y + (z + (u + x))
r088 
|- x ≥ x ⇔ T
r089 
|- x ≥ y ⇔ x + -1 * y ≥ 0
r090 
|- x ≥ y ⇔ y + -1 * x ≤ 0
r091 
|- x ≥ y + z ⇔ y + (z + -1 * x) ≤ 0
r092 
|- -1 * x ≥ 0 ⇔ x ≤ 0
r093 
|- -1 * x ≥ -y ⇔ x ≤ y
r094 
|- -1 * x + y ≥ 0 ⇔ x + -1 * y ≤ 0
r095 
|- x + -1 * y ≥ 0 ⇔ y ≤ x
r096 
|- x > y ⇔ ¬(y ≥ x)
r097 
|- x > y ⇔ ¬(x ≤ y)
r098 
|- x > y ⇔ ¬(x + -1 * y ≤ 0)
r099 
|- x > y ⇔ ¬(y + -1 * x ≥ 0)
r100 
|- x > y + z ⇔ ¬(z + -1 * x ≥ -y)
r101 
|- x ≤ x ⇔ T
r102 
|- 0 ≤ 1 ⇔ T
r103 
|- x ≤ y ⇔ y ≥ x
r104 
|- 0 ≤ -x + y ⇔ y ≥ x
r105 
|- -1 * x ≤ 0 ⇔ x ≥ 0
r106 
|- x ≤ y ⇔ x + -1 * y ≤ 0
r107 
|- x ≤ y ⇔ y + -1 * x ≥ 0
r108 
|- -1 * x + y ≤ 0 ⇔ x + -1 * y ≥ 0
r109 
|- -1 * x + y ≤ -z ⇔ x + -1 * y ≥ z
r110 
|- -x + y ≤ z ⇔ y + -1 * z ≤ x
r111 
|- x + -1 * y ≤ z ⇔ x + (-1 * y + -1 * z) ≤ 0
r112 
|- x ≤ y + z ⇔ x + -1 * z ≤ y
r113 
|- x ≤ y + z ⇔ z + -1 * x ≥ -y
r114 
|- x ≤ y + z ⇔ x + (-1 * y + -1 * z) ≤ 0
r115 
|- x < y ⇔ ¬(y ≤ x)
r116 
|- x < y ⇔ ¬(x ≥ y)
r117 
|- x < y ⇔ ¬(y + -1 * x ≤ 0)
r118 
|- x < y ⇔ ¬(x + -1 * y ≥ 0)
r119 
|- x < y + -1 * z ⇔ ¬(x + -1 * y + z ≥ 0)
r120 
|- x < y + -1 * z ⇔ ¬(x + (-1 * y + z) ≥ 0)
r121 
|- x < -y + z ⇔ ¬(z + -1 * x ≤ y)
r122 
|- x < -y + (z + u) ⇔ ¬(z + (u + -1 * x) ≤ y)
r123 
|- x < -y + (z + (u + v)) ⇔ ¬(z + (u + (v + -1 * x)) ≤ y)
r124 
|- -x + y < z ⇔ ¬(y + -1 * z ≥ x)
r125 
|- x + y < z ⇔ ¬(z + -1 * y ≤ x)
r126 
|- 0 < -x + y ⇔ ¬(y ≤ x)
r127 
|- x − 0 = x
r128 
|- 0 − x = -x
r129 
|- 0 − x = -1 * x
r130 
|- x − y = -y + x
r131 
|- x − y = x + -1 * y
r132 
|- x − y = -1 * y + x
r133 
|- x − 1 = -1 + x
r134 
|- x + y − z = x + (y + -1 * z)
r135 
|- x + y − z = x + (-1 * z + y)
r136 
|- (0 = -u * x) ⇔ (u * x = 0)
r137 
|- (a = -u * x) ⇔ (u * x = -a)
r138 
|- (a = x + (y + z)) ⇔ (x + (y + (-1 * a + z)) = 0)
r139 
|- (a = x + (y + z)) ⇔ (x + (y + (z + -1 * a)) = 0)
r140 
|- (a = -u * y + v * z) ⇔ (u * y + (-v * z + a) = 0)
r141 
|- (a = -u * y + -v * z) ⇔ (u * y + (a + v * z) = 0)
r142 
|- (-a = -u * x + v * y) ⇔ (u * x + -v * y = a)
r143 
|- (a = -u * x + (-v * y + w * z)) ⇔ (u * x + (v * y + (-w * z + a)) = 0)
r144 
|- (a = -u * x + (v * y + w * z)) ⇔ (u * x + (-v * y + -w * z) = -a)
r145 
|- (a = -u * x + (v * y + -w * z)) ⇔ (u * x + (-v * y + w * z) = -a)
r146 
|- (a = -u * x + (-v * y + w * z)) ⇔ (u * x + (v * y + -w * z) = -a)
r147 
|- (a = -u * x + (-v * y + -w * z)) ⇔ (u * x + (v * y + w * z) = -a)
r148 
|- (-a = -u * x + (v * y + w * z)) ⇔ (u * x + (-v * y + -w * z) = a)
r149 
|- (-a = -u * x + (v * y + -w * z)) ⇔ (u * x + (-v * y + w * z) = a)
r150 
|- (-a = -u * x + (-v * y + w * z)) ⇔ (u * x + (v * y + -w * z) = a)
r151 
|- (-a = -u * x + (-v * y + -w * z)) ⇔ (u * x + (v * y + w * z) = a)
r152 
|- (a = -u * x + (-1 * y + w * z)) ⇔ (u * x + (y + -w * z) = -a)
r153 
|- (a = -u * x + (-1 * y + -w * z)) ⇔ (u * x + (y + w * z) = -a)
r154 
|- (-u * x + -v * y = -a) ⇔ (u * x + v * y = a)
r155 
|- (-1 * x + (-v * y + -w * z) = -a) ⇔ (x + (v * y + w * z) = a)
r156 
|- (-u * x + (v * y + w * z) = -a) ⇔ (u * x + (-v * y + -w * z) = a)
r157 
|- (-u * x + (-v * y + w * z) = -a) ⇔ (u * x + (v * y + -w * z) = a)
r158 
|- (-u * x + (-v * y + -w * z) = -a) ⇔ (u * x + (v * y + w * z) = a)
r159 
|- x + -1 * y ≥ 0 ⇔ y ≤ x
r160 
|- x ≥ y ⇔ x + -1 * y ≥ 0
r161 
|- x > y ⇔ ¬(x + -1 * y ≤ 0)
r162 
|- x ≤ y ⇔ x + -1 * y ≤ 0
r163 
|- x ≤ y + z ⇔ x + -1 * z ≤ y
r164 
|- -u * x ≤ a ⇔ u * x ≥ -a
r165 
|- -u * x ≤ -a ⇔ u * x ≥ a
r166 
|- -u * x + v * y ≤ 0 ⇔ u * x + -v * y ≥ 0
r167 
|- -u * x + v * y ≤ a ⇔ u * x + -v * y ≥ -a
r168 
|- -u * x + v * y ≤ -a ⇔ u * x + -v * y ≥ a
r169 
|- -u * x + -v * y ≤ a ⇔ u * x + v * y ≥ -a
r170 
|- -u * x + -v * y ≤ -a ⇔ u * x + v * y ≥ a
r171 
|- -u * x + (v * y + w * z) ≤ 0 ⇔ u * x + (-v * y + -w * z) ≥ 0
r172 
|- -u * x + (v * y + -w * z) ≤ 0 ⇔ u * x + (-v * y + w * z) ≥ 0
r173 
|- -u * x + (-v * y + w * z) ≤ 0 ⇔ u * x + (v * y + -w * z) ≥ 0
r174 
|- -u * x + (-v * y + -w * z) ≤ 0 ⇔ u * x + (v * y + w * z) ≥ 0
r175 
|- -u * x + (v * y + w * z) ≤ a ⇔ u * x + (-v * y + -w * z) ≥ -a
r176 
|- -u * x + (v * y + w * z) ≤ -a ⇔ u * x + (-v * y + -w * z) ≥ a
r177 
|- -u * x + (v * y + -w * z) ≤ a ⇔ u * x + (-v * y + w * z) ≥ -a
r178 
|- -u * x + (v * y + -w * z) ≤ -a ⇔ u * x + (-v * y + w * z) ≥ a
r179 
|- -u * x + (-v * y + w * z) ≤ a ⇔ u * x + (v * y + -w * z) ≥ -a
r180 
|- -u * x + (-v * y + w * z) ≤ -a ⇔ u * x + (v * y + -w * z) ≥ a
r181 
|- -u * x + (-v * y + -w * z) ≤ a ⇔ u * x + (v * y + w * z) ≥ -a
r182 
|- -u * x + (-v * y + -w * z) ≤ -a ⇔ u * x + (v * y + w * z) ≥ a
r183 
|- -1 * x + (v * y + w * z) ≤ -a ⇔ x + (-v * y + -w * z) ≥ a
r184 
|- x < y ⇔ ¬(x ≥ y)
r185 
|- -u * x < a ⇔ ¬(u * x ≤ -a)
r186 
|- -u * x < -a ⇔ ¬(u * x ≤ a)
r187 
|- -u * x + v * y < 0 ⇔ ¬(u * x + -v * y ≤ 0)
r188 
|- -u * x + -v * y < 0 ⇔ ¬(u * x + v * y ≤ 0)
r189 
|- -u * x + v * y < a ⇔ ¬(u * x + -v * y ≤ -a)
r190 
|- -u * x + v * y < -a ⇔ ¬(u * x + -v * y ≤ a)
r191 
|- -u * x + -v * y < a ⇔ ¬(u * x + v * y ≤ -a)
r192 
|- -u * x + -v * y < -a ⇔ ¬(u * x + v * y ≤ a)
r193 
|- -u * x + (v * y + w * z) < a ⇔ ¬(u * x + (-v * y + -w * z) ≤ -a)
r194 
|- -u * x + (v * y + w * z) < -a ⇔ ¬(u * x + (-v * y + -w * z) ≤ a)
r195 
|- -u * x + (v * y + -w * z) < a ⇔ ¬(u * x + (-v * y + w * z) ≤ -a)
r196 
|- -u * x + (v * y + -w * z) < -a ⇔ ¬(u * x + (-v * y + w * z) ≤ a)
r197 
|- -u * x + (-v * y + w * z) < a ⇔ ¬(u * x + (v * y + -w * z) ≤ -a)
r198 
|- -u * x + (-v * y + w * z) < -a ⇔ ¬(u * x + (v * y + -w * z) ≤ a)
r199 
|- -u * x + (-v * y + -w * z) < a ⇔ ¬(u * x + (v * y + w * z) ≤ -a)
r200 
|- -u * x + (-v * y + -w * z) < -a ⇔ ¬(u * x + (v * y + w * z) ≤ a)
r201 
|- -u * x + (-v * y + w * z) < 0 ⇔ ¬(u * x + (v * y + -w * z) ≤ 0)
r202 
|- -u * x + (-v * y + -w * z) < 0 ⇔ ¬(u * x + (v * y + w * z) ≤ 0)
r203 
|- -1 * x + (v * y + w * z) < a ⇔ ¬(x + (-v * y + -w * z) ≤ -a)
r204 
|- -1 * x + (v * y + w * z) < -a ⇔ ¬(x + (-v * y + -w * z) ≤ a)
r205 
|- -1 * x + (v * y + -w * z) < a ⇔ ¬(x + (-v * y + w * z) ≤ -a)
r206 
|- -1 * x + (v * y + -w * z) < -a ⇔ ¬(x + (-v * y + w * z) ≤ a)
r207 
|- -1 * x + (-v * y + w * z) < a ⇔ ¬(x + (v * y + -w * z) ≤ -a)
r208 
|- -1 * x + (-v * y + w * z) < -a ⇔ ¬(x + (v * y + -w * z) ≤ a)
r209 
|- -1 * x + (-v * y + -w * z) < a ⇔ ¬(x + (v * y + w * z) ≤ -a)
r210 
|- -1 * x + (-v * y + -w * z) < -a ⇔ ¬(x + (v * y + w * z) ≤ a)
r211 
|- -u * x + (-1 * y + -w * z) < -a ⇔ ¬(u * x + (y + w * z) ≤ a)
r212 
|- -u * x + (v * y + -1 * z) < -a ⇔ ¬(u * x + (-v * y + z) ≤ a)
r213 
|- 0 + x = x
r214 
|- x + 0 = x
r215 
|- x + y = y + x
r216 
|- x + x = 2 * x
r217 
|- x + y + z = x + (y + z)
r218 
|- x + y + z = x + (z + y)
r219 
|- x + (y + z) = y + (z + x)
r220 
|- x + (y + z) = y + (x + z)
r221 
|- 0 − x = -x
r222 
|- 0 − u * x = -u * x
r223 
|- x − 0 = x
r224 
|- x − y = x + -1 * y
r225 
|- x − y = -1 * y + x
r226 
|- x − u * y = x + -u * y
r227 
|- x − u * y = -u * y + x
r228 
|- x + y − z = x + (y + -1 * z)
r229 
|- x + y − z = x + (-1 * z + y)
r230 
|- x + y − u * z = -u * z + (x + y)
r231 
|- x + y − u * z = x + (-u * z + y)
r232 
|- x + y − u * z = x + (y + -u * z)
r233 
|- 0 * x = 0
r234 
|- 1 * x = x
r235 
|- 0w + x = x
r236 
|- x + y = y + x
r237 
|- 1w + (1w + x) = 2w + x
r238 
|- (x + z = y + x) ⇔ (y = z)
r239 
 [..] |- 0w @@ n2w x = n2w x
r240 
 [.] |- w2w (n2w x) = n2w x
r241 
 [...] |- (0w @@ x = n2w y) ⇔ (x = n2w y)
r242 
 [...] |- (0w @@ x = n2w y) ⇔ (n2w y = x)
r243 
 [...] |- (n2w y = 0w @@ x) ⇔ (x = n2w y)
r244 
 [...] |- (n2w y = 0w @@ x) ⇔ (n2w y = x)
r245 
|- x && y = y && x
r246 
|- x && y && z = y && x && z
r247 
|- x && y && z = (x && y) && z
r248 
|- (1w = x && y) ⇔ (1w = x) ∧ (1w = y)
r249 
|- (1w = x && y) ⇔ (1w = y) ∧ (1w = x)
r250 
|- (7 >< 0) x = x
r251 
|- x <₊ y ⇔ ¬(y ≤₊ x)
r252 
|- x * y = y * x
r253 
|- (0 >< 0) x = x
r254 
|- (x && y) && z = x && y && z
r255 
|- 0w ‖ x = x
t001 
|- (x = y) ∨ (f x = (y =+ z) f x)
t002 
|- (x = y) ∨ (f y = (x =+ z) f y)
t003 
|- (x = y) ∨ ((y =+ z) f x = f x)
t004 
|- (x = y) ∨ ((x =+ z) f y = f y)
t005 
|- (f = g) ∨ f (array_ext f g) ≠ g (array_ext f g)
t006 
|- x ≠ y ∨ x ≤ y
t007 
|- x ≠ y ∨ x ≥ y
t008 
|- x ≠ y ∨ x + -1 * y ≥ 0
t009 
|- x ≠ y ∨ x + -1 * y ≤ 0
t010 
|- (x = y) ∨ ¬(x ≤ y) ∨ ¬(x ≥ y)
t011 
|- ¬(x ≤ 0) ∨ x ≤ 1
t012 
|- ¬(x ≤ -1) ∨ x ≤ 0
t013 
|- ¬(x ≥ 0) ∨ x ≥ -1
t014 
|- ¬(x ≥ 0) ∨ ¬(x ≤ -1)
t015 
|- x ≥ y ∨ x ≤ y
t016 
|- x ≠ y ∨ x + -1 * y ≥ 0
t017 
|- x ≠ ¬x
t018 
|- (x = y) ⇒ x ' i ⇒ y ' i
t019 
|- (1w = ¬x) ∨ x ' 0
t020 
|- x ' 0 ⇒ (0w = ¬x)
t021 
|- x ' 0 ⇒ (1w = x)
t022 
|- ¬x ' 0 ⇒ (0w = x)
t023 
|- ¬x ' 0 ⇒ (1w = ¬x)
t024 
|- (0w = ¬x) ∨ ¬x ' 0
t025 
|- (1w = ¬x ‖ ¬y) ∨ ¬(¬x ' 0 ∨ ¬y ' 0)
t026 
|- (0w = x) ∨ x ' 0 ∨ x ' 1 ∨ x ' 2 ∨ x ' 3 ∨ x ' 4 ∨ x ' 5 ∨ x ' 6 ∨ x ' 7
t027 
|- ((x = 1w) ⇔ p) ⇔ (x = if p then 1w else 0w)
t028 
|- ((1w = x) ⇔ p) ⇔ (x = if p then 1w else 0w)
t029 
|- (p ⇔ (x = 1w)) ⇔ (x = if p then 1w else 0w)
t030 
|- (p ⇔ (1w = x)) ⇔ (x = if p then 1w else 0w)
t031 
|- (0w = 4294967295w * sw2sw x) ⇒ ¬x ' 0
t032 
|- (0w = 4294967295w * sw2sw x) ⇒ (x ' 1 ⇎ ¬x ' 0)
t033 
|- (0w = 4294967295w * sw2sw x) ⇒ (x ' 2 ⇎ ¬x ' 0 ∧ ¬x ' 1)
t034 
|- (1w + x = y) ⇒ x ' 0 ⇒ ¬y ' 0
t035 
|- (1w = x) ∨ (0 >< 0) x ≠ 1w
p001 
|- 0 < dimword (:α)
p002 
|- 1 < dimword (:α)
p003 
|- 255 < dimword (:8)
p004 
|- FINITE 𝕌(:unit)
p005 
|- FINITE 𝕌(:16)
p006 
|- FINITE 𝕌(:24)
p007 
|- FINITE 𝕌(:30)
p008 
|- FINITE 𝕌(:31)
p009 
|- dimindex (:8) ≤ dimindex (:32)