Theory "HolSmt"

Signature

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)