Theory: HolSmt

Theorems

ALL_DISTINCT_CONS

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

ALL_DISTINCT_NIL

⊢ ALL_DISTINCT [] ⇔ T

AND_IMP_INTRO_SYM

⊢ p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r

AND_T

⊢ ∀p. p ∧ T ⇔ p

CONJ_CONG

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

DISJ_ELIM_1

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

DISJ_ELIM_2

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

F_OR

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

IMP_DISJ_1

⊢ (p ⇒ q) ⇒ ¬p ∨ q

IMP_DISJ_2

⊢ (¬p ⇒ q) ⇒ p ∨ q

IMP_FALSE

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

NEG_IFF_1_1

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

NEG_IFF_1_2

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

NEG_IFF_2_1

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

NEG_IFF_2_2

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

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)

NOT_FALSE

⊢ ∀p. p ⇒ ¬p ⇒ F

NOT_MEM_CONS

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

NOT_MEM_NIL

⊢ ∀x. ¬MEM x [] ⇔ T

NOT_NOT_ELIM

⊢ ∀p. ¬¬p ⇒ p

NOT_NOT_INTRO

⊢ ∀p. p ⇔ ¬¬p

NOT_P_OR_P

⊢ ¬p ∨ p

NOT_REVERSE

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

SKOLEM_EXISTS

⊢ ∃a. (∃x. P x) ⇔ P a

SKOLEM_FORALL

⊢ ∃a. ¬(∀x. P x) ⇔ ¬P a

T_AND

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

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

i001

[oracles: DISK_THM] [axioms: ] [n = t] ⊢ n = t

i002

[oracles: DISK_THM] [axioms: ] [n ⇔ t] ⊢ ¬n ∨ t

i003

[oracles: DISK_THM] [axioms: ] [n ⇔ t] ⊢ (n ∨ ¬t) ∧ (¬n ∨ t)

i004

[oracles: DISK_THM] [axioms: ] [n = if c then t1 else t2]
⊢ (¬c ∨ (n = t1)) ∧ (c ∨ (n = t2))

int_ceiling_floor

⊢ ∀r. ⌈r⌉ = -⌊-r⌋

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)

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

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

r011

⊢ (if T then x else y) = x

r012

⊢ (if F then x else y) = y

r013

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

r014

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

r015

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

r016

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

r017

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

r018

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

r019

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

r020

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

r021

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

r022

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

r023

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

r024

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

r025

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

r026

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

r027

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

r028

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

r029

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

r030

⊢ ¬p ⇒ q ⇔ p ∨ q

r031

⊢ ¬p ⇒ q ⇔ q ∨ p

r032

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

r033

⊢ ¬(∃x. P x ⇒ Q) ⇔ ¬∃x. ¬P x ∨ Q

r034

⊢ ¬(∃x. P x ⇒ Q) ⇔ ¬∃x. Q ∨ ¬P x

r035

⊢ ¬(∃x. ¬P x ∨ Q) ⇔ ¬∃x. ¬P x ∨ Q

r036

⊢ ¬(∃x. ¬P x ∨ Q) ⇔ ¬∃x. Q ∨ ¬P x

r037

⊢ p ⇒ q ⇔ ¬p ∨ q

r038

⊢ p ⇒ q ⇔ q ∨ ¬p

r039

⊢ T ⇒ p ⇔ p

r040

⊢ p ⇒ T ⇔ T

r041

⊢ F ⇒ p ⇔ T

r042

⊢ p ⇒ p ⇔ T

r043

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

r044

⊢ ¬T ⇔ F

r045

⊢ ¬F ⇔ T

r046

⊢ ¬¬p ⇔ p

r047

⊢ p ∨ q ⇔ q ∨ p

r048

⊢ p ∨ T ⇔ T

r049

⊢ p ∨ ¬p ⇔ T

r050

⊢ ¬p ∨ p ⇔ T

r051

⊢ T ∨ p ⇔ T

r052

⊢ p ∨ F ⇔ p

r053

⊢ F ∨ p ⇔ p

r054

⊢ p ∧ q ⇔ q ∧ p

r055

⊢ p ∧ T ⇔ p

r056

⊢ T ∧ p ⇔ p

r057

⊢ p ∧ F ⇔ F

r058

⊢ F ∧ p ⇔ F

r059

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

r060

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

r061

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

r062

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

r063

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

r064

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

r065

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

r066

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

r067

⊢ f⦇x ↦ f x⦈ = f

r068

⊢ ALL_DISTINCT [x; x] ⇔ F

r069

⊢ ALL_DISTINCT [x; y] ⇔ x ≠ y

r070

⊢ ALL_DISTINCT [x; y] ⇔ y ≠ x

r071

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

r072

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

r073

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

r074

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

r075

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

r076

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

r077

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

r078

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

r079

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

r080

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

r081

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

r082

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

r083

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

r084

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

r085

⊢ 0 + x = x

r086

⊢ x + 0 = x

r087

⊢ x + y = y + x

r088

⊢ x + x = 2 * x

r089

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

r090

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

r091

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

r092

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

r093

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

r094

⊢ x ≥ x ⇔ T

r095

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

r096

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

r097

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

r098

⊢ -1 * x ≥ 0 ⇔ x ≤ 0

r099

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

r100

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

r101

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

r102

⊢ x > y ⇔ ¬(y ≥ x)

r103

⊢ x > y ⇔ ¬(x ≤ y)

r104

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

r105

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

r106

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

r107

⊢ x ≤ x ⇔ T

r108

⊢ 0 ≤ 1 ⇔ T

r109

⊢ x ≤ y ⇔ y ≥ x

r110

⊢ 0 ≤ -x + y ⇔ y ≥ x

r111

⊢ -1 * x ≤ 0 ⇔ x ≥ 0

r112

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

r113

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

r114

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

r115

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

r116

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

r117

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

r118

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

r119

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

r120

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

r121

⊢ x < y ⇔ ¬(y ≤ x)

r122

⊢ x < y ⇔ ¬(x ≥ y)

r123

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

r124

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

r125

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

r126

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

r127

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

r128

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

r129

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

r130

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

r131

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

r132

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

r133

⊢ x − 0 = x

r134

⊢ 0 − x = -x

r135

⊢ 0 − x = -1 * x

r136

⊢ x − y = -y + x

r137

⊢ x − y = x + -1 * y

r138

⊢ x − y = -1 * y + x

r139

⊢ x − 1 = -1 + x

r140

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

r141

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

r142

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

r143

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

r144

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

r145

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

r146

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

r147

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

r148

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

r149

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

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 + (-v * y + w * z)) ⇔ (u * x + (v * y + -w * z) = -a)

r153

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

r154

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

r155

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

r156

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

r157

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

r158

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

r159

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

r160

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

r161

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

r162

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

r163

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

r164

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

r165

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

r166

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

r167

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

r168

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

r169

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

r170

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

r171

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

r172

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

r173

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

r174

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

r175

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

r176

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

r177

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

r178

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

r179

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

r180

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

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

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

r184

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

r185

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

r186

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

r187

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

r188

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

r189

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

r190

⊢ x < y ⇔ ¬(x ≥ y)

r191

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

r192

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

r193

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

r194

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

r195

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

r196

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

r197

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

r198

⊢ -u * x + -v * y < -a ⇔ ¬(u * x + v * y ≤ 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) < a ⇔ ¬(u * x + (-v * y + w * z) ≤ -a)

r202

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

r203

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

r204

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

r205

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

r206

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

r207

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

r208

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

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

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

r212

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

r213

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

r214

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

r215

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

r216

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

r217

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

r218

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

r219

⊢ 0 + x = x

r220

⊢ x + 0 = x

r221

⊢ x + y = y + x

r222

⊢ x + x = 2 * x

r223

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

r224

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

r225

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

r226

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

r227

⊢ 0 − x = -x

r228

⊢ 0 − u * x = -u * x

r229

⊢ x − 0 = x

r230

⊢ x − y = x + -1 * y

r231

⊢ x − y = -1 * y + x

r232

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

r233

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

r234

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

r235

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

r236

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

r237

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

r238

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

r239

⊢ 0 * x = 0

r240

⊢ 1 * x = x

r241

⊢ 0w + x = x

r242

⊢ x + y = y + x

r243

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

r244

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

r245

[oracles: DISK_THM] [axioms: ] [FINITE 𝕌(:α), x < dimword (:β)]
⊢ 0w @@ n2w x = n2w x

r246

[oracles: DISK_THM] [axioms: ] [x < dimword (:α)] ⊢ w2w (n2w x) = n2w x

r247

[oracles: DISK_THM] [axioms: ]
[FINITE 𝕌(:α), y < dimword (:β), dimindex (:β) ≤ dimindex (:γ)]
⊢ (0w @@ x = n2w y) ⇔ (x = n2w y)

r248

[oracles: DISK_THM] [axioms: ]
[FINITE 𝕌(:α), y < dimword (:β), dimindex (:β) ≤ dimindex (:γ)]
⊢ (0w @@ x = n2w y) ⇔ (n2w y = x)

r249

[oracles: DISK_THM] [axioms: ]
[FINITE 𝕌(:α), y < dimword (:β), dimindex (:β) ≤ dimindex (:γ)]
⊢ (n2w y = 0w @@ x) ⇔ (x = n2w y)

r250

[oracles: DISK_THM] [axioms: ]
[FINITE 𝕌(:α), y < dimword (:β), dimindex (:β) ≤ dimindex (:γ)]
⊢ (n2w y = 0w @@ x) ⇔ (n2w y = x)

r251

⊢ x && y = y && x

r252

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

r253

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

r254

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

r255

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

r256

⊢ (7 >< 0) x = x

r257

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

r258

⊢ x * y = y * x

r259

⊢ (0 >< 0) x = x

r260

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

r261

⊢ 0w ‖ x = x

real_div_smt_rdiv

⊢ ∀x y. x / y = if y = 0 then 0 else smt_rdiv x y

t001

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

t002

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

t003

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

t004

⊢ (x = y) ∨ (f⦇x ↦ z⦈ 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 = 0xFFFFFFFFw * sw2sw x) ⇒ ¬x ' 0

t032

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

t033

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

t034

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

t035

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

Theory HolSmt

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems