Structure HolSmtTheory


Source File Identifier index Theory binding index

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


Source File Identifier index Theory binding index

HOL 4, Kananaskis-11