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

VALID_IFF_TRUE

⊢ ∀p. p ⇒ (p ⇔ T)

T_AND

⊢ ∀p q. (T ∧ p ⇔ T ∧ q) ⇒ (p ⇔ q)

t035

⊢ (1w = x) ∨ (0 >< 0) x ≠ 1w

t034

⊢ (1w + x = y) ⇒ x ' 0 ⇒ ¬y ' 0

t033

⊢ (0w = 4294967295w * sw2sw x) ⇒ (x ' 2 ⇎ ¬x ' 0 ∧ ¬x ' 1)

t032

⊢ (0w = 4294967295w * sw2sw x) ⇒ (x ' 1 ⇎ ¬x ' 0)

t031

⊢ (0w = 4294967295w * sw2sw x) ⇒ ¬x ' 0

t030

⊢ (p ⇔ (1w = x)) ⇔ (x = if p then 1w else 0w)

t029

⊢ (p ⇔ (x = 1w)) ⇔ (x = if p then 1w else 0w)

t028

⊢ ((1w = x) ⇔ p) ⇔ (x = if p then 1w else 0w)

t027

⊢ ((x = 1w) ⇔ p) ⇔ (x = if p then 1w else 0w)

t026

⊢ (0w = x) ∨ x ' 0 ∨ x ' 1 ∨ x ' 2 ∨ x ' 3 ∨ x ' 4 ∨ x ' 5 ∨ x ' 6 ∨ x ' 7

t025

⊢ (1w = ¬x ‖ ¬y) ∨ ¬(¬x ' 0 ∨ ¬y ' 0)

t024

⊢ (0w = ¬x) ∨ ¬x ' 0

t023

⊢ ¬x ' 0 ⇒ (1w = ¬x)

t022

⊢ ¬x ' 0 ⇒ (0w = x)

t021

⊢ x ' 0 ⇒ (1w = x)

t020

⊢ x ' 0 ⇒ (0w = ¬x)

t019

⊢ (1w = ¬x) ∨ x ' 0

t018

⊢ (x = y) ⇒ x ' i ⇒ y ' i

t017

⊢ x ≠ ¬x

t016

⊢ x ≠ y ∨ x + -1 * y ≥ 0

t015

⊢ x ≥ y ∨ x ≤ y

t014

⊢ ¬(x ≥ 0) ∨ ¬(x ≤ -1)

t013

⊢ ¬(x ≥ 0) ∨ x ≥ -1

t012

⊢ ¬(x ≤ -1) ∨ x ≤ 0

t011

⊢ ¬(x ≤ 0) ∨ x ≤ 1

t010

⊢ (x = y) ∨ ¬(x ≤ y) ∨ ¬(x ≥ y)

t009

⊢ x ≠ y ∨ x + -1 * y ≤ 0

t008

⊢ x ≠ y ∨ x + -1 * y ≥ 0

t007

⊢ x ≠ y ∨ x ≥ y

t006

⊢ x ≠ y ∨ x ≤ y

t005

⊢ (f = g) ∨ f (array_ext f g) ≠ g (array_ext f g)

t004

⊢ (x = y) ∨ (f⦇x ↦ z⦈ y = f y)

t003

⊢ (x = y) ∨ (f⦇y ↦ z⦈ x = f x)

t002

⊢ (x = y) ∨ (f y = f⦇x ↦ z⦈ y)

t001

⊢ (x = y) ∨ (f x = f⦇y ↦ z⦈ x)

r255

⊢ 0w ‖ x = x

r254

⊢ (x && y) && z = x && y && z

r253

⊢ (0 >< 0) x = x

r252

⊢ x * y = y * x

r251

⊢ x <₊ y ⇔ ¬(y ≤₊ x)

r250

⊢ (7 >< 0) x = x

r249

⊢ (1w = x && y) ⇔ (1w = y) ∧ (1w = x)

r248

⊢ (1w = x && y) ⇔ (1w = x) ∧ (1w = y)

r247

⊢ x && y && z = (x && y) && z

r246

⊢ x && y && z = y && x && z

r245

⊢ x && y = y && x

r244

 [...] ⊢ (n2w y = 0w @@ x) ⇔ (n2w y = x)

r243

 [...] ⊢ (n2w y = 0w @@ x) ⇔ (x = n2w y)

r242

 [...] ⊢ (0w @@ x = n2w y) ⇔ (n2w y = x)

r241

 [...] ⊢ (0w @@ x = n2w y) ⇔ (x = n2w y)

r240

 [.] ⊢ w2w (n2w x) = n2w x

r239

 [..] ⊢ 0w @@ n2w x = n2w x

r238

⊢ (x + z = y + x) ⇔ (y = z)

r237

⊢ 1w + (1w + x) = 2w + x

r236

⊢ x + y = y + x

r235

⊢ 0w + x = x

r234

⊢ 1 * x = x

r233

⊢ 0 * x = 0

r232

⊢ x + y − u * z = x + (y + -u * z)

r231

⊢ x + y − u * z = x + (-u * z + y)

r230

⊢ x + y − u * z = -u * z + (x + y)

r229

⊢ x + y − z = x + (-1 * z + y)

r228

⊢ x + y − z = x + (y + -1 * z)

r227

⊢ x − u * y = -u * y + x

r226

⊢ x − u * y = x + -u * y

r225

⊢ x − y = -1 * y + x

r224

⊢ x − y = x + -1 * y

r223

⊢ x − 0 = x

r222

⊢ 0 − u * x = -u * x

r221

⊢ 0 − x = -x

r220

⊢ x + (y + z) = y + (x + z)

r219

⊢ x + (y + z) = y + (z + x)

r218

⊢ x + y + z = x + (z + y)

r217

⊢ x + y + z = x + (y + z)

r216

⊢ x + x = 2 * x

r215

⊢ x + y = y + x

r214

⊢ x + 0 = x

r213

⊢ 0 + x = x

r212

⊢ -u * x + (v * y + -1 * z) < -a ⇔ ¬(u * x + (-v * y + z) ≤ a)

r211

⊢ -u * x + (-1 * y + -w * z) < -a ⇔ ¬(u * x + (y + w * z) ≤ a)

r210

⊢ -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)

r208

⊢ -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)

r206

⊢ -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)

r204

⊢ -1 * x + (v * y + w * z) < -a ⇔ ¬(x + (-v * y + -w * z) ≤ a)

r203

⊢ -1 * x + (v * y + w * z) < a ⇔ ¬(x + (-v * y + -w * z) ≤ -a)

r202

⊢ -u * x + (-v * y + -w * z) < 0 ⇔ ¬(u * x + (v * y + w * z) ≤ 0)

r201

⊢ -u * x + (-v * y + w * z) < 0 ⇔ ¬(u * x + (v * y + -w * z) ≤ 0)

r200

⊢ -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)

r198

⊢ -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)

r196

⊢ -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)

r194

⊢ -u * x + (v * y + w * z) < -a ⇔ ¬(u * x + (-v * y + -w * z) ≤ a)

r193

⊢ -u * x + (v * y + w * z) < a ⇔ ¬(u * x + (-v * y + -w * z) ≤ -a)

r192

⊢ -u * x + -v * y < -a ⇔ ¬(u * x + v * y ≤ a)

r191

⊢ -u * x + -v * y < a ⇔ ¬(u * x + v * y ≤ -a)

r190

⊢ -u * x + v * y < -a ⇔ ¬(u * x + -v * y ≤ a)

r189

⊢ -u * x + v * y < a ⇔ ¬(u * x + -v * y ≤ -a)

r188

⊢ -u * x + -v * y < 0 ⇔ ¬(u * x + v * y ≤ 0)

r187

⊢ -u * x + v * y < 0 ⇔ ¬(u * x + -v * y ≤ 0)

r186

⊢ -u * x < -a ⇔ ¬(u * x ≤ a)

r185

⊢ -u * x < a ⇔ ¬(u * x ≤ -a)

r184

⊢ x < y ⇔ ¬(x ≥ y)

r183

⊢ -1 * x + (v * y + w * z) ≤ -a ⇔ x + (-v * y + -w * z) ≥ a

r182

⊢ -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

r180

⊢ -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

r178

⊢ -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

r176

⊢ -u * x + (v * y + w * z) ≤ -a ⇔ u * x + (-v * y + -w * z) ≥ a

r175

⊢ -u * x + (v * y + w * z) ≤ a ⇔ u * x + (-v * y + -w * z) ≥ -a

r174

⊢ -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

r172

⊢ -u * x + (v * y + -w * z) ≤ 0 ⇔ u * x + (-v * y + w * z) ≥ 0

r171

⊢ -u * x + (v * y + w * z) ≤ 0 ⇔ u * x + (-v * y + -w * z) ≥ 0

r170

⊢ -u * x + -v * y ≤ -a ⇔ u * x + v * y ≥ a

r169

⊢ -u * x + -v * y ≤ a ⇔ u * x + v * y ≥ -a

r168

⊢ -u * x + v * y ≤ -a ⇔ u * x + -v * y ≥ a

r167

⊢ -u * x + v * y ≤ a ⇔ u * x + -v * y ≥ -a

r166

⊢ -u * x + v * y ≤ 0 ⇔ u * x + -v * y ≥ 0

r165

⊢ -u * x ≤ -a ⇔ u * x ≥ a

r164

⊢ -u * x ≤ a ⇔ u * x ≥ -a

r163

⊢ x ≤ y + z ⇔ x + -1 * z ≤ y

r162

⊢ x ≤ y ⇔ x + -1 * y ≤ 0

r161

⊢ x > y ⇔ ¬(x + -1 * y ≤ 0)

r160

⊢ x ≥ y ⇔ x + -1 * y ≥ 0

r159

⊢ x + -1 * y ≥ 0 ⇔ y ≤ x

r158

⊢ (-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)

r156

⊢ (-u * x + (v * y + w * z) = -a) ⇔ (u * x + (-v * y + -w * z) = a)

r155

⊢ (-1 * x + (-v * y + -w * z) = -a) ⇔ (x + (v * y + w * z) = a)

r154

⊢ (-u * x + -v * y = -a) ⇔ (u * x + v * y = a)

r153

⊢ (a = -u * x + (-1 * y + -w * z)) ⇔ (u * x + (y + w * z) = -a)

r152

⊢ (a = -u * x + (-1 * y + w * z)) ⇔ (u * x + (y + -w * z) = -a)

r151

⊢ (-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)

r149

⊢ (-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)

r147

⊢ (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)

r145

⊢ (a = -u * x + (v * y + -w * z)) ⇔ (u * x + (-v * y + w * z) = -a)

r144

⊢ (a = -u * x + (v * y + w * z)) ⇔ (u * x + (-v * y + -w * z) = -a)

r143

⊢ (a = -u * x + (-v * y + w * z)) ⇔ (u * x + (v * y + (-w * z + a)) = 0)

r142

⊢ (-a = -u * x + v * y) ⇔ (u * x + -v * y = a)

r141

⊢ (a = -u * y + -v * z) ⇔ (u * y + (a + v * z) = 0)

r140

⊢ (a = -u * y + v * z) ⇔ (u * y + (-v * z + a) = 0)

r139

⊢ (a = x + (y + z)) ⇔ (x + (y + (z + -1 * a)) = 0)

r138

⊢ (a = x + (y + z)) ⇔ (x + (y + (-1 * a + z)) = 0)

r137

⊢ (a = -u * x) ⇔ (u * x = -a)

r136

⊢ (0 = -u * x) ⇔ (u * x = 0)

r135

⊢ x + y − z = x + (-1 * z + y)

r134

⊢ x + y − z = x + (y + -1 * z)

r133

⊢ x − 1 = -1 + x

r132

⊢ x − y = -1 * y + x

r131

⊢ x − y = x + -1 * y

r130

⊢ x − y = -y + x

r129

⊢ 0 − x = -1 * x

r128

⊢ 0 − x = -x

r127

⊢ x − 0 = x

r126

⊢ 0 < -x + y ⇔ ¬(y ≤ x)

r125

⊢ x + y < z ⇔ ¬(z + -1 * y ≤ x)

r124

⊢ -x + y < z ⇔ ¬(y + -1 * z ≥ x)

r123

⊢ x < -y + (z + (u + v)) ⇔ ¬(z + (u + (v + -1 * x)) ≤ y)

r122

⊢ x < -y + (z + u) ⇔ ¬(z + (u + -1 * x) ≤ y)

r121

⊢ x < -y + z ⇔ ¬(z + -1 * x ≤ y)

r120

⊢ x < y + -1 * z ⇔ ¬(x + (-1 * y + z) ≥ 0)

r119

⊢ x < y + -1 * z ⇔ ¬(x + -1 * y + z ≥ 0)

r118

⊢ x < y ⇔ ¬(x + -1 * y ≥ 0)

r117

⊢ x < y ⇔ ¬(y + -1 * x ≤ 0)

r116

⊢ x < y ⇔ ¬(x ≥ y)

r115

⊢ x < y ⇔ ¬(y ≤ x)

r114

⊢ x ≤ y + z ⇔ x + (-1 * y + -1 * z) ≤ 0

r113

⊢ x ≤ y + z ⇔ z + -1 * x ≥ -y

r112

⊢ x ≤ y + z ⇔ x + -1 * z ≤ y

r111

⊢ x + -1 * y ≤ z ⇔ x + (-1 * y + -1 * z) ≤ 0

r110

⊢ -x + y ≤ z ⇔ y + -1 * z ≤ x

r109

⊢ -1 * x + y ≤ -z ⇔ x + -1 * y ≥ z

r108

⊢ -1 * x + y ≤ 0 ⇔ x + -1 * y ≥ 0

r107

⊢ x ≤ y ⇔ y + -1 * x ≥ 0

r106

⊢ x ≤ y ⇔ x + -1 * y ≤ 0

r105

⊢ -1 * x ≤ 0 ⇔ x ≥ 0

r104

⊢ 0 ≤ -x + y ⇔ y ≥ x

r103

⊢ x ≤ y ⇔ y ≥ x

r102

⊢ 0 ≤ 1 ⇔ T

r101

⊢ x ≤ x ⇔ T

r100

⊢ x > y + z ⇔ ¬(z + -1 * x ≥ -y)

r099

⊢ x > y ⇔ ¬(y + -1 * x ≥ 0)

r098

⊢ x > y ⇔ ¬(x + -1 * y ≤ 0)

r097

⊢ x > y ⇔ ¬(x ≤ y)

r096

⊢ x > y ⇔ ¬(y ≥ x)

r095

⊢ x + -1 * y ≥ 0 ⇔ y ≤ x

r094

⊢ -1 * x + y ≥ 0 ⇔ x + -1 * y ≤ 0

r093

⊢ -1 * x ≥ -y ⇔ x ≤ y

r092

⊢ -1 * x ≥ 0 ⇔ x ≤ 0

r091

⊢ x ≥ y + z ⇔ y + (z + -1 * x) ≤ 0

r090

⊢ x ≥ y ⇔ y + -1 * x ≤ 0

r089

⊢ x ≥ y ⇔ x + -1 * y ≥ 0

r088

⊢ x ≥ x ⇔ T

r087

⊢ x + (y + (z + u)) = y + (z + (u + x))

r086

⊢ x + (y + z) = y + (x + z)

r085

⊢ x + (y + z) = y + (z + x)

r084

⊢ x + y + z = x + (z + y)

r083

⊢ x + y + z = x + (y + z)

r082

⊢ x + x = 2 * x

r081

⊢ x + y = y + x

r080

⊢ x + 0 = x

r079

⊢ 0 + x = x

r078

⊢ (a + (-1 * x + (v * y + w * z)) = 0) ⇔ (x + (-v * y + -w * z) = a)

r077

⊢ (x + y = z) ⇔ (y + -1 * z = -x)

r076

⊢ (x + y = 0) ⇔ (y = -x)

r075

⊢ (-1 * x + y = z) ⇔ (x + -1 * y = -z)

r074

⊢ (-1 * x = -y) ⇔ (x = y)

r073

⊢ (x = -y + z) ⇔ (z + -1 * x = y)

r072

⊢ (x = y + z) ⇔ (z + -1 * x = -y)

r071

⊢ (x = y + z) ⇔ (y + (-1 * x + z) = 0)

r070

⊢ (x = y + z) ⇔ (y + (z + -1 * x) = 0)

r069

⊢ (x = y + z) ⇔ (x + (-1 * y + -1 * z) = 0)

r068

⊢ (x = -1 * y + z) ⇔ (y + (-1 * z + x) = 0)

r067

⊢ (x = y + -1 * z) ⇔ (x + (-1 * y + z) = 0)

r066

⊢ (x = y + z) ⇔ (x + -1 * z = y)

r065

⊢ (x = y) ⇔ (x + -1 * y = 0)

r064

⊢ ALL_DISTINCT [x; y] ⇔ y ≠ x

r063

⊢ ALL_DISTINCT [x; y] ⇔ x ≠ y

r062

⊢ ALL_DISTINCT [x; x] ⇔ F

r061

⊢ f⦇x ↦ f x⦈ = f

r060

⊢ ¬p ∧ ¬q ⇔ ¬(q ∨ p)

r059

⊢ p ∧ ¬q ⇔ ¬(q ∨ ¬p)

r058

⊢ ¬p ∧ q ⇔ ¬(¬q ∨ p)

r057

⊢ p ∧ q ⇔ ¬(¬q ∨ ¬p)

r056

⊢ ¬p ∧ ¬q ⇔ ¬(p ∨ q)

r055

⊢ p ∧ ¬q ⇔ ¬(¬p ∨ q)

r054

⊢ ¬p ∧ q ⇔ ¬(p ∨ ¬q)

r053

⊢ p ∧ q ⇔ ¬(¬p ∨ ¬q)

r052

⊢ F ∧ p ⇔ F

r051

⊢ p ∧ F ⇔ F

r050

⊢ T ∧ p ⇔ p

r049

⊢ p ∧ T ⇔ p

r048

⊢ p ∧ q ⇔ q ∧ p

r047

⊢ F ∨ p ⇔ p

r046

⊢ p ∨ F ⇔ p

r045

⊢ T ∨ p ⇔ T

r044

⊢ ¬p ∨ p ⇔ T

r043

⊢ p ∨ ¬p ⇔ T

r042

⊢ p ∨ T ⇔ T

r041

⊢ p ∨ q ⇔ q ∨ p

r040

⊢ ¬¬p ⇔ p

r039

⊢ ¬F ⇔ T

r038

⊢ ¬T ⇔ F

r037

⊢ (p ⇔ q) ⇒ r ⇔ r ∨ (q ⇔ ¬p)

r036

⊢ p ⇒ p ⇔ T

r035

⊢ F ⇒ p ⇔ T

r034

⊢ p ⇒ T ⇔ T

r033

⊢ T ⇒ p ⇔ p

r032

⊢ p ⇒ q ⇔ q ∨ ¬p

r031

⊢ p ⇒ q ⇔ ¬p ∨ q

r030

⊢ ¬p ⇒ q ⇔ q ∨ p

r029

⊢ ¬p ⇒ q ⇔ p ∨ q

r028

⊢ (if p then x = y else (z = y)) ⇔ (y = if p then x else z)

r027

⊢ (if p then x = y else (y = z)) ⇔ (y = if p then x else z)

r026

⊢ (if p then x = y else (x = z)) ⇔ (x = if p then y else z)

r025

⊢ (if p then x else if q then x else y) = if q ∨ p then x else y

r024

⊢ (if p then x else if q then x else y) = if p ∨ q then x else y

r023

⊢ (if p then x else if p then y else z) = if p then x else z

r022

⊢ (if p then if q then x else y else y) = if q ∧ p then x else y

r021

⊢ (if p then if q then x else y else y) = if p ∧ q then x else y

r020

⊢ (if p then if q then x else y else x) = if ¬q ∧ p then y else x

r019

⊢ (if p then if q then x else y else x) = if p ∧ ¬q then y else x

r018

⊢ (if ¬p then x else y) = if p then y else x

r017

⊢ (if p then ¬q else q) ⇔ (¬q ⇔ p)

r016

⊢ (if p then ¬q else q) ⇔ (p ⇔ ¬q)

r015

⊢ (if p then q else ¬q) ⇔ (q ⇔ p)

r014

⊢ (if p then q else ¬q) ⇔ (p ⇔ q)

r013

⊢ (if p then q else T) ⇔ q ∨ ¬p

r012

⊢ (if p then q else T) ⇔ ¬p ∨ q

r011

⊢ (if F then x else y) = y

r010

⊢ (if T then x else y) = x

r009

⊢ (¬p ⇎ q) ⇔ (p ⇔ q)

r008

⊢ (p ⇎ ¬q) ⇔ (p ⇔ q)

r007

⊢ (¬p ⇔ ¬q) ⇔ (p ⇔ q)

r006

⊢ (F ⇔ p) ⇔ ¬p

r005

⊢ (p ⇔ F) ⇔ ¬p

r004

⊢ (T ⇔ p) ⇔ p

r003

⊢ (p ⇔ T) ⇔ p

r002

⊢ (x = x) ⇔ T

r001

⊢ (x = y) ⇔ (y = x)

p009

⊢ dimindex (:8) ≤ dimindex (:32)

p008

⊢ FINITE 𝕌(:31)

p007

⊢ FINITE 𝕌(:30)

p006

⊢ FINITE 𝕌(:24)

p005

⊢ FINITE 𝕌(:16)

p004

⊢ FINITE 𝕌(:unit)

p003

⊢ 255 < dimword (:8)

p002

⊢ 1 < dimword (:α)

p001

⊢ 0 < dimword (:α)

NOT_NOT_ELIM

⊢ ∀p. ¬¬p ⇒ p

NOT_MEM_NIL

⊢ ∀x. ¬MEM x [] ⇔ T

NOT_MEM_CONS

⊢ ∀x h t. ¬MEM x (h::t) ⇔ x ≠ h ∧ ¬MEM x t

NOT_FALSE

⊢ ∀p. p ⇒ ¬p ⇒ F

NNF_NOT_NOT

⊢ ∀p q. (p ⇔ q) ⇒ (¬¬p ⇔ q)

NNF_DISJ

⊢ ∀p q r s. (¬p ⇔ r) ⇒ (¬q ⇔ s) ⇒ (¬(p ∨ q) ⇔ r ∧ s)

NNF_CONJ

⊢ ∀p q r s. (¬p ⇔ r) ⇒ (¬q ⇔ s) ⇒ (¬(p ∧ q) ⇔ r ∨ s)

NEG_IFF_2_2

⊢ ∀p q. (p ⇎ q) ⇒ (p ⇔ ¬q)

NEG_IFF_2_1

⊢ ∀p q. (p ⇔ ¬q) ⇒ (p ⇎ q)

NEG_IFF_1_2

⊢ ∀p q. (p ⇎ ¬q) ⇒ (q ⇔ p)

NEG_IFF_1_1

⊢ ∀p q. (q ⇔ p) ⇒ (p ⇎ ¬q)

IMP_FALSE

⊢ ∀p. (¬p ⇒ F) ⇒ p

IMP_DISJ_2

⊢ ∀p q. (¬p ⇒ q) ⇒ p ∨ q

IMP_DISJ_1

⊢ ∀p q. (p ⇒ q) ⇒ ¬p ∨ q

F_OR

⊢ ∀p q. (F ∨ p ⇔ F ∨ q) ⇒ (p ⇔ q)

DISJ_ELIM_2

⊢ ∀p q r. (p ∨ q ⇒ r) ⇒ q ⇒ r

DISJ_ELIM_1

⊢ ∀p q r. (p ∨ q ⇒ r) ⇒ p ⇒ r

d028

⊢ ¬(if p then q else r) ∨ p ∨ r

d027

⊢ ¬(if p then q else r) ∨ ¬p ∨ q

d026

⊢ (if p then q else ¬r) ∨ p ∨ r

d025

⊢ (if p then ¬q else r) ∨ ¬p ∨ q

d024

⊢ (if p then q else r) ∨ p ∨ ¬r

d023

⊢ (if p then q else r) ∨ ¬p ∨ ¬q

d022

⊢ ¬p ∨ q ∨ ¬if p then q else r

d021

⊢ p ∨ q ∨ ¬if p then r else q

d020

⊢ ¬p ∨ ((if p then x else y) = x)

d019

⊢ p ∨ ((if p then x else y) = y)

d018

⊢ ¬p ∨ (x = if p then x else y)

d017

⊢ p ∨ (y = if p then x else y)

d016

⊢ p ∧ q ∨ ¬p ∨ ¬q

d015

⊢ p ∧ ¬q ∨ ¬p ∨ q

d014

⊢ ¬p ∧ q ∨ p ∨ ¬q

d013

⊢ ¬p ∧ ¬q ∨ p ∨ q

d012

⊢ p ∨ q ∨ (p ⇎ ¬q)

d011

⊢ p ∨ q ∨ (¬p ⇎ q)

d010

⊢ p ∨ ¬q ∨ (p ⇎ q)

d009

⊢ ¬p ∨ q ∨ (p ⇎ q)

d008

⊢ (p ⇎ ¬q) ∨ p ∨ q

d007

⊢ (¬p ⇎ q) ∨ p ∨ q

d006

⊢ (p ⇔ q) ∨ p ∨ q

d005

⊢ (p ⇔ q) ∨ ¬p ∨ ¬q

d004

⊢ (¬p ⇔ q) ∨ p ∨ ¬q

d003

⊢ (p ⇔ ¬q) ∨ ¬p ∨ q

d002

⊢ (p ⇎ q) ∨ p ∨ ¬q

d001

⊢ (p ⇎ q) ∨ ¬p ∨ q

CONJ_CONG

⊢ ∀p q r s. (p ⇔ q) ⇒ (r ⇔ s) ⇒ (p ∧ r ⇔ q ∧ s)

AND_T

⊢ ∀p. p ∧ T ⇔ p

AND_IMP_INTRO_SYM

⊢ ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r

ALL_DISTINCT_NIL

⊢ ALL_DISTINCT [] ⇔ T

ALL_DISTINCT_CONS

⊢ ∀h t. ALL_DISTINCT (h::t) ⇔ ¬MEM h t ∧ ALL_DISTINCT t