tt('const/HolSmt/array_ext', ty, ![A : $t, B : $t]: ((A > B) > ((A > B) > A))).
tt('const/HolSmt/xor', ty, ($o > ($o > $o))).
tt('thm/HolSmt/xor_def_', def, (![x : $o, y : $o]: (('const/HolSmt/xor' x y) = (~ (x = y))))).
tt('thm/HolSmt/array_ext_def_', def, ![A : $t, B : $t]: (![A0 : (A > B), B0 : (A > B)]: ((('const/HolSmt/array_ext' A B) A0 B0) = (('const/min/@' A) (^[i : A]: (~ ((A0 i) = (B0 i)))))))).
tt('thm/HolSmt/ALL_DISTINCT_NIL_', ax, ![A : $t]: ((('const/list/ALL_DISTINCT' A) ('const/list/NIL' A)) = $true)).
tt('thm/HolSmt/ALL_DISTINCT_CONS_', ax, ![A : $t]: (![h : A, t : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) (('const/list/CONS' A) h t)) = ((~ (('const/bool/IN' A) h (('const/list/LIST_TO_SET' A) t))) & (('const/list/ALL_DISTINCT' A) t))))).
tt('thm/HolSmt/NOT_MEM_NIL_', ax, ![A : $t]: (![x : A]: ((~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) ('const/list/NIL' A)))) = $true))).
tt('thm/HolSmt/NOT_MEM_CONS_', ax, ![A : $t]: (![x : A, h : A, t : ('type/list/list' A)]: ((~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/CONS' A) h t)))) = ((~ (x = h)) & (~ (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) t))))))).
tt('thm/HolSmt/AND_T_', ax, (![p : $o]: ((p & $true) = p))).
tt('thm/HolSmt/T_AND_', ax, (![p : $o, q : $o]: ((($true & p) = ($true & q)) => (p = q)))).
tt('thm/HolSmt/F_OR_', ax, (![p : $o, q : $o]: ((($false | p) = ($false | q)) => (p = q)))).
tt('thm/HolSmt/CONJ_CONG_', ax, (![p : $o, q : $o, r : $o, s : $o]: ((p = q) => ((r = s) => ((p & r) = (q & s)))))).
tt('thm/HolSmt/NOT_NOT_ELIM_', ax, (![p : $o]: ((~ (~ p)) => p))).
tt('thm/HolSmt/NOT_FALSE_', ax, (![p : $o]: (p => ((~ p) => $false)))).
tt('thm/HolSmt/NNF_CONJ_', ax, (![p : $o, q : $o, r : $o, s : $o]: (((~ p) = r) => (((~ q) = s) => ((~ (p & q)) = (r | s)))))).
tt('thm/HolSmt/NNF_DISJ_', ax, (![p : $o, q : $o, r : $o, s : $o]: (((~ p) = r) => (((~ q) = s) => ((~ (p | q)) = (r & s)))))).
tt('thm/HolSmt/NNF_NOT_NOT_', ax, (![p : $o, q : $o]: ((p = q) => ((~ (~ p)) = q)))).
tt('thm/HolSmt/NEG_IFF_1_1_', ax, (![p : $o, q : $o]: ((q = p) => (~ (p = (~ q)))))).
tt('thm/HolSmt/NEG_IFF_1_2_', ax, (![p : $o, q : $o]: ((~ (p = (~ q))) => (q = p)))).
tt('thm/HolSmt/NEG_IFF_2_1_', ax, (![p : $o, q : $o]: ((p = (~ q)) => (~ (p = q))))).
tt('thm/HolSmt/NEG_IFF_2_2_', ax, (![p : $o, q : $o]: ((~ (p = q)) => (p = (~ q))))).
tt('thm/HolSmt/DISJ_ELIM_1_', ax, (![p : $o, q : $o, r : $o]: (((p | q) => r) => (p => r)))).
tt('thm/HolSmt/DISJ_ELIM_2_', ax, (![p : $o, q : $o, r : $o]: (((p | q) => r) => (q => r)))).
tt('thm/HolSmt/IMP_DISJ_1_', ax, (![p : $o, q : $o]: ((p => q) => ((~ p) | q)))).
tt('thm/HolSmt/IMP_DISJ_2_', ax, (![p : $o, q : $o]: (((~ p) => q) => (p | q)))).
tt('thm/HolSmt/IMP_FALSE_', ax, (![p : $o]: (((~ p) => $false) => p))).
tt('thm/HolSmt/AND_IMP_INTRO_SYM_', ax, (![p : $o, q : $o, r : $o]: (((p & q) => r) = (p => (q => r))))).
tt('thm/HolSmt/VALID_IFF_TRUE_', ax, (![p : $o]: (p => (p = $true)))).
tt('thm/HolSmt/d001_', ax, (![q : $o, p : $o]: ((~ (p = q)) | ((~ p) | q)))).
tt('thm/HolSmt/d002_', ax, (![q : $o, p : $o]: ((~ (p = q)) | (p | (~ q))))).
tt('thm/HolSmt/d003_', ax, (![q : $o, p : $o]: ((p = (~ q)) | ((~ p) | q)))).
tt('thm/HolSmt/d004_', ax, (![q : $o, p : $o]: (((~ p) = q) | (p | (~ q))))).
tt('thm/HolSmt/d005_', ax, (![q : $o, p : $o]: ((p = q) | ((~ p) | (~ q))))).
tt('thm/HolSmt/d006_', ax, (![q : $o, p : $o]: ((p = q) | (p | q)))).
tt('thm/HolSmt/d007_', ax, (![q : $o, p : $o]: ((~ ((~ p) = q)) | (p | q)))).
tt('thm/HolSmt/d008_', ax, (![q : $o, p : $o]: ((~ (p = (~ q))) | (p | q)))).
tt('thm/HolSmt/d009_', ax, (![q : $o, p : $o]: ((~ p) | (q | (~ (p = q)))))).
tt('thm/HolSmt/d010_', ax, (![q : $o, p : $o]: (p | ((~ q) | (~ (p = q)))))).
tt('thm/HolSmt/d011_', ax, (![q : $o, p : $o]: (p | (q | (~ ((~ p) = q)))))).
tt('thm/HolSmt/d012_', ax, (![q : $o, p : $o]: (p | (q | (~ (p = (~ q))))))).
tt('thm/HolSmt/d013_', ax, (![q : $o, p : $o]: (((~ p) & (~ q)) | (p | q)))).
tt('thm/HolSmt/d014_', ax, (![q : $o, p : $o]: (((~ p) & q) | (p | (~ q))))).
tt('thm/HolSmt/d015_', ax, (![q : $o, p : $o]: ((p & (~ q)) | ((~ p) | q)))).
tt('thm/HolSmt/d016_', ax, (![q : $o, p : $o]: ((p & q) | ((~ p) | (~ q))))).
tt('thm/HolSmt/d017_', ax, ![A : $t]: (![y : A, x : A, p : $o]: (p | (y = (('const/bool/COND' A) p x y))))).
tt('thm/HolSmt/d018_', ax, ![A : $t]: (![y : A, x : A, p : $o]: ((~ p) | (x = (('const/bool/COND' A) p x y))))).
tt('thm/HolSmt/d019_', ax, ![A : $t]: (![y : A, x : A, p : $o]: (p | ((('const/bool/COND' A) p x y) = y)))).
tt('thm/HolSmt/d020_', ax, ![A : $t]: (![y : A, x : A, p : $o]: ((~ p) | ((('const/bool/COND' A) p x y) = x)))).
tt('thm/HolSmt/d021_', ax, (![r : $o, q : $o, p : $o]: (p | (q | (~ (('const/bool/COND' $o) p r q)))))).
tt('thm/HolSmt/d022_', ax, (![r : $o, q : $o, p : $o]: ((~ p) | (q | (~ (('const/bool/COND' $o) p q r)))))).
tt('thm/HolSmt/d023_', ax, (![r : $o, q : $o, p : $o]: ((('const/bool/COND' $o) p q r) | ((~ p) | (~ q))))).
tt('thm/HolSmt/d024_', ax, (![r : $o, q : $o, p : $o]: ((('const/bool/COND' $o) p q r) | (p | (~ r))))).
tt('thm/HolSmt/d025_', ax, (![r : $o, q : $o, p : $o]: ((('const/bool/COND' $o) p (~ q) r) | ((~ p) | q)))).
tt('thm/HolSmt/d026_', ax, (![r : $o, q : $o, p : $o]: ((('const/bool/COND' $o) p q (~ r)) | (p | r)))).
tt('thm/HolSmt/d027_', ax, (![r : $o, q : $o, p : $o]: ((~ (('const/bool/COND' $o) p q r)) | ((~ p) | q)))).
tt('thm/HolSmt/d028_', ax, (![r : $o, q : $o, p : $o]: ((~ (('const/bool/COND' $o) p q r)) | (p | r)))).
tt('thm/HolSmt/r001_', ax, ![A : $t]: (![y : A, x : A]: ((x = y) = (y = x)))).
tt('thm/HolSmt/r002_', ax, ![A : $t]: (![x : A]: ((x = x) = $true))).
tt('thm/HolSmt/r003_', ax, (![p : $o]: ((p = $true) = p))).
tt('thm/HolSmt/r004_', ax, (![p : $o]: (($true = p) = p))).
tt('thm/HolSmt/r005_', ax, (![p : $o]: ((p = $false) = (~ p)))).
tt('thm/HolSmt/r006_', ax, (![p : $o]: (($false = p) = (~ p)))).
tt('thm/HolSmt/r007_', ax, (![q : $o, p : $o]: (((~ p) = (~ q)) = (p = q)))).
tt('thm/HolSmt/r008_', ax, (![q : $o, p : $o]: ((~ (p = (~ q))) = (p = q)))).
tt('thm/HolSmt/r009_', ax, (![q : $o, p : $o]: ((~ ((~ p) = q)) = (p = q)))).
tt('thm/HolSmt/r010_', ax, ![A : $t]: (![y : A, x : A]: ((('const/bool/COND' A) $true x y) = x))).
tt('thm/HolSmt/r011_', ax, ![A : $t]: (![y : A, x : A]: ((('const/bool/COND' A) $false x y) = y))).
tt('thm/HolSmt/r012_', ax, (![q : $o, p : $o]: ((('const/bool/COND' $o) p q $true) = ((~ p) | q)))).
tt('thm/HolSmt/r013_', ax, (![q : $o, p : $o]: ((('const/bool/COND' $o) p q $true) = (q | (~ p))))).
tt('thm/HolSmt/r014_', ax, (![q : $o, p : $o]: ((('const/bool/COND' $o) p q (~ q)) = (p = q)))).
tt('thm/HolSmt/r015_', ax, (![q : $o, p : $o]: ((('const/bool/COND' $o) p q (~ q)) = (q = p)))).
tt('thm/HolSmt/r016_', ax, (![q : $o, p : $o]: ((('const/bool/COND' $o) p (~ q) q) = (p = (~ q))))).
tt('thm/HolSmt/r017_', ax, (![q : $o, p : $o]: ((('const/bool/COND' $o) p (~ q) q) = ((~ q) = p)))).
tt('thm/HolSmt/r018_', ax, ![A : $t]: (![y : A, x : A, p : $o]: ((('const/bool/COND' A) (~ p) x y) = (('const/bool/COND' A) p y x)))).
tt('thm/HolSmt/r019_', ax, ![A : $t]: (![y : A, x : A, q : $o, p : $o]: ((('const/bool/COND' A) p (('const/bool/COND' A) q x y) x) = (('const/bool/COND' A) (p & (~ q)) y x)))).
tt('thm/HolSmt/r020_', ax, ![A : $t]: (![y : A, x : A, q : $o, p : $o]: ((('const/bool/COND' A) p (('const/bool/COND' A) q x y) x) = (('const/bool/COND' A) ((~ q) & p) y x)))).
tt('thm/HolSmt/r021_', ax, ![A : $t]: (![y : A, x : A, q : $o, p : $o]: ((('const/bool/COND' A) p (('const/bool/COND' A) q x y) y) = (('const/bool/COND' A) (p & q) x y)))).
tt('thm/HolSmt/r022_', ax, ![A : $t]: (![y : A, x : A, q : $o, p : $o]: ((('const/bool/COND' A) p (('const/bool/COND' A) q x y) y) = (('const/bool/COND' A) (q & p) x y)))).
tt('thm/HolSmt/r023_', ax, ![A : $t]: (![z : A, y : A, x : A, p : $o]: ((('const/bool/COND' A) p x (('const/bool/COND' A) p y z)) = (('const/bool/COND' A) p x z)))).
tt('thm/HolSmt/r024_', ax, ![A : $t]: (![y : A, x : A, q : $o, p : $o]: ((('const/bool/COND' A) p x (('const/bool/COND' A) q x y)) = (('const/bool/COND' A) (p | q) x y)))).
tt('thm/HolSmt/r025_', ax, ![A : $t]: (![y : A, x : A, q : $o, p : $o]: ((('const/bool/COND' A) p x (('const/bool/COND' A) q x y)) = (('const/bool/COND' A) (q | p) x y)))).
tt('thm/HolSmt/r026_', ax, ![A : $t]: (![z : A, y : A, x : A, p : $o]: ((('const/bool/COND' $o) p (x = y) (x = z)) = (x = (('const/bool/COND' A) p y z))))).
tt('thm/HolSmt/r027_', ax, ![A : $t]: (![z : A, y : A, x : A, p : $o]: ((('const/bool/COND' $o) p (x = y) (y = z)) = (y = (('const/bool/COND' A) p x z))))).
tt('thm/HolSmt/r028_', ax, ![A : $t]: (![z : A, y : A, x : A, p : $o]: ((('const/bool/COND' $o) p (x = y) (z = y)) = (y = (('const/bool/COND' A) p x z))))).
tt('thm/HolSmt/r029_', ax, (![q : $o, p : $o]: (((~ p) => q) = (p | q)))).
tt('thm/HolSmt/r030_', ax, (![q : $o, p : $o]: (((~ p) => q) = (q | p)))).
tt('thm/HolSmt/r031_', ax, (![q : $o, p : $o]: ((p => q) = ((~ p) | q)))).
tt('thm/HolSmt/r032_', ax, (![q : $o, p : $o]: ((p => q) = (q | (~ p))))).
tt('thm/HolSmt/r033_', ax, (![p : $o]: (($true => p) = p))).
tt('thm/HolSmt/r034_', ax, (![p : $o]: ((p => $true) = $true))).
tt('thm/HolSmt/r035_', ax, (![p : $o]: (($false => p) = $true))).
tt('thm/HolSmt/r036_', ax, (![p : $o]: ((p => p) = $true))).
tt('thm/HolSmt/r037_', ax, (![r : $o, q : $o, p : $o]: (((p = q) => r) = (r | (q = (~ p)))))).
tt('thm/HolSmt/r038_', ax, ((~ $true) = $false)).
tt('thm/HolSmt/r039_', ax, ((~ $false) = $true)).
tt('thm/HolSmt/r040_', ax, (![p : $o]: ((~ (~ p)) = p))).
tt('thm/HolSmt/r041_', ax, (![q : $o, p : $o]: ((p | q) = (q | p)))).
tt('thm/HolSmt/r042_', ax, (![p : $o]: ((p | $true) = $true))).
tt('thm/HolSmt/r043_', ax, (![p : $o]: ((p | (~ p)) = $true))).
tt('thm/HolSmt/r044_', ax, (![p : $o]: (((~ p) | p) = $true))).
tt('thm/HolSmt/r045_', ax, (![p : $o]: (($true | p) = $true))).
tt('thm/HolSmt/r046_', ax, (![p : $o]: ((p | $false) = p))).
tt('thm/HolSmt/r047_', ax, (![p : $o]: (($false | p) = p))).
tt('thm/HolSmt/r048_', ax, (![q : $o, p : $o]: ((p & q) = (q & p)))).
tt('thm/HolSmt/r049_', ax, (![p : $o]: ((p & $true) = p))).
tt('thm/HolSmt/r050_', ax, (![p : $o]: (($true & p) = p))).
tt('thm/HolSmt/r051_', ax, (![p : $o]: ((p & $false) = $false))).
tt('thm/HolSmt/r052_', ax, (![p : $o]: (($false & p) = $false))).
tt('thm/HolSmt/r053_', ax, (![q : $o, p : $o]: ((p & q) = (~ ((~ p) | (~ q)))))).
tt('thm/HolSmt/r054_', ax, (![q : $o, p : $o]: (((~ p) & q) = (~ (p | (~ q)))))).
tt('thm/HolSmt/r055_', ax, (![q : $o, p : $o]: ((p & (~ q)) = (~ ((~ p) | q))))).
tt('thm/HolSmt/r056_', ax, (![q : $o, p : $o]: (((~ p) & (~ q)) = (~ (p | q))))).
tt('thm/HolSmt/r057_', ax, (![q : $o, p : $o]: ((p & q) = (~ ((~ q) | (~ p)))))).
tt('thm/HolSmt/r058_', ax, (![q : $o, p : $o]: (((~ p) & q) = (~ ((~ q) | p))))).
tt('thm/HolSmt/r059_', ax, (![q : $o, p : $o]: ((p & (~ q)) = (~ (q | (~ p)))))).
tt('thm/HolSmt/r060_', ax, (![q : $o, p : $o]: (((~ p) & (~ q)) = (~ (q | p))))).
tt('thm/HolSmt/r061_', ax, ![A : $t, B : $t]: (![x : A, f : (A > B)]: ((('const/combin/UPDATE' A B) x (f x) f) = f))).
tt('thm/HolSmt/r062_', ax, ![A : $t]: (![x : A]: ((('const/list/ALL_DISTINCT' A) (('const/list/CONS' A) x (('const/list/CONS' A) x ('const/list/NIL' A)))) = $false))).
tt('thm/HolSmt/r063_', ax, ![A : $t]: (![y : A, x : A]: ((('const/list/ALL_DISTINCT' A) (('const/list/CONS' A) x (('const/list/CONS' A) y ('const/list/NIL' A)))) = (~ (x = y))))).
tt('thm/HolSmt/r064_', ax, ![A : $t]: (![y : A, x : A]: ((('const/list/ALL_DISTINCT' A) (('const/list/CONS' A) x (('const/list/CONS' A) y ('const/list/NIL' A)))) = (~ (y = x))))).
tt('thm/HolSmt/r065_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((x = y) = (('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r066_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' y z)) = (('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) = y)))).
tt('thm/HolSmt/r067_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) = (('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) z)) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r068_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) z)) = (('const/integer/int_add' y ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z) x)) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r069_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' y z)) = (('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r070_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' y z)) = (('const/integer/int_add' y ('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x))) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r071_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' y z)) = (('const/integer/int_add' y ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) z)) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r072_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' y z)) = (('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) = ('const/integer/int_neg' y))))).
tt('thm/HolSmt/r073_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((x = ('const/integer/int_add' ('const/integer/int_neg' y) z)) = (('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) = y)))).
tt('thm/HolSmt/r074_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) = ('const/integer/int_neg' y)) = (x = y)))).
tt('thm/HolSmt/r075_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) y) = z) = (('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) = ('const/integer/int_neg' z))))).
tt('thm/HolSmt/r076_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((('const/integer/int_add' x y) = ('const/integer/int_of_num' 'const/num/0')) = (y = ('const/integer/int_neg' x))))).
tt('thm/HolSmt/r077_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: ((('const/integer/int_add' x y) = z) = (('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) = ('const/integer/int_neg' x))))).
tt('thm/HolSmt/r078_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int', w : 'type/integer/int', v : 'type/integer/int', a : 'type/integer/int']: ((('const/integer/int_add' a ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/integer/int_add' ('const/integer/int_mul' v y) ('const/integer/int_mul' w z)))) = ('const/integer/int_of_num' 'const/num/0')) = (('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' v) y) ('const/integer/int_mul' ('const/integer/int_neg' w) z))) = a)))).
tt('thm/HolSmt/r079_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_of_num' 'const/num/0') x) = x))).
tt('thm/HolSmt/r080_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_of_num' 'const/num/0')) = x))).
tt('thm/HolSmt/r081_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' x y) = ('const/integer/int_add' y x)))).
tt('thm/HolSmt/r082_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' x x) = ('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)))).
tt('thm/HolSmt/r083_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_add' x y) z) = ('const/integer/int_add' x ('const/integer/int_add' y z))))).
tt('thm/HolSmt/r084_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_add' x y) z) = ('const/integer/int_add' x ('const/integer/int_add' z y))))).
tt('thm/HolSmt/r085_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_add' y z)) = ('const/integer/int_add' y ('const/integer/int_add' z x))))).
tt('thm/HolSmt/r086_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_add' y z)) = ('const/integer/int_add' y ('const/integer/int_add' x z))))).
tt('thm/HolSmt/r087_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int', u : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_add' y ('const/integer/int_add' z u))) = ('const/integer/int_add' y ('const/integer/int_add' z ('const/integer/int_add' u x)))))).
tt('thm/HolSmt/r088_', ax, (![x : 'type/integer/int']: (('const/integer/int_ge' x x) = $true))).
tt('thm/HolSmt/r089_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' x y) = ('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r090_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' x y) = ('const/integer/int_le' ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r091_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' x ('const/integer/int_add' y z)) = ('const/integer/int_le' ('const/integer/int_add' y ('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x))) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r092_', ax, (![x : 'type/integer/int']: (('const/integer/int_ge' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_le' x ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r093_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/integer/int_neg' y)) = ('const/integer/int_le' x y)))).
tt('thm/HolSmt/r094_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) y) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r095_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_le' y x)))).
tt('thm/HolSmt/r096_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_gt' x y) = (~ ('const/integer/int_ge' y x))))).
tt('thm/HolSmt/r097_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_gt' x y) = (~ ('const/integer/int_le' x y))))).
tt('thm/HolSmt/r098_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_gt' x y) = (~ ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r099_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_gt' x y) = (~ ('const/integer/int_ge' ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r100_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_gt' x ('const/integer/int_add' y z)) = (~ ('const/integer/int_ge' ('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) ('const/integer/int_neg' y)))))).
tt('thm/HolSmt/r101_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' x x) = $true))).
tt('thm/HolSmt/r102_', ax, (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = $true)).
tt('thm/HolSmt/r103_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x y) = ('const/integer/int_ge' y x)))).
tt('thm/HolSmt/r104_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' ('const/integer/int_neg' x) y)) = ('const/integer/int_ge' y x)))).
tt('thm/HolSmt/r105_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_ge' x ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r106_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x y) = ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r107_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x y) = ('const/integer/int_ge' ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r108_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) y) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r109_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) y) ('const/integer/int_neg' z)) = ('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) z)))).
tt('thm/HolSmt/r110_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_add' ('const/integer/int_neg' x) y) z) = ('const/integer/int_le' ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) x)))).
tt('thm/HolSmt/r111_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) z) = ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r112_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x ('const/integer/int_add' y z)) = ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) y)))).
tt('thm/HolSmt/r113_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x ('const/integer/int_add' y z)) = ('const/integer/int_ge' ('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) ('const/integer/int_neg' y))))).
tt('thm/HolSmt/r114_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x ('const/integer/int_add' y z)) = ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r115_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x y) = (~ ('const/integer/int_le' y x))))).
tt('thm/HolSmt/r116_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x y) = (~ ('const/integer/int_ge' x y))))).
tt('thm/HolSmt/r117_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x y) = (~ ('const/integer/int_le' ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r118_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x y) = (~ ('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r119_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) = (~ ('const/integer/int_ge' ('const/integer/int_add' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) z) ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r120_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) = (~ ('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) z)) ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r121_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_add' ('const/integer/int_neg' y) z)) = (~ ('const/integer/int_le' ('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)) y))))).
tt('thm/HolSmt/r122_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int', u : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_add' ('const/integer/int_neg' y) ('const/integer/int_add' z u))) = (~ ('const/integer/int_le' ('const/integer/int_add' z ('const/integer/int_add' u ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x))) y))))).
tt('thm/HolSmt/r123_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int', v : 'type/integer/int', u : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_add' ('const/integer/int_neg' y) ('const/integer/int_add' z ('const/integer/int_add' u v)))) = (~ ('const/integer/int_le' ('const/integer/int_add' z ('const/integer/int_add' u ('const/integer/int_add' v ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))) y))))).
tt('thm/HolSmt/r124_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_add' ('const/integer/int_neg' x) y) z) = (~ ('const/integer/int_ge' ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) x))))).
tt('thm/HolSmt/r125_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_add' x y) z) = (~ ('const/integer/int_le' ('const/integer/int_add' z ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) x))))).
tt('thm/HolSmt/r126_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' ('const/integer/int_neg' x) y)) = (~ ('const/integer/int_le' y x))))).
tt('thm/HolSmt/r127_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' x ('const/integer/int_of_num' 'const/num/0')) = x))).
tt('thm/HolSmt/r128_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_of_num' 'const/num/0') x) = ('const/integer/int_neg' x)))).
tt('thm/HolSmt/r129_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_of_num' 'const/num/0') x) = ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))).
tt('thm/HolSmt/r130_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_sub' x y) = ('const/integer/int_add' ('const/integer/int_neg' y) x)))).
tt('thm/HolSmt/r131_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_sub' x y) = ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y))))).
tt('thm/HolSmt/r132_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_sub' x y) = ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) x)))).
tt('thm/HolSmt/r133_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))).
tt('thm/HolSmt/r134_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_add' x y) z) = ('const/integer/int_add' x ('const/integer/int_add' y ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)))))).
tt('thm/HolSmt/r135_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_add' x y) z) = ('const/integer/int_add' x ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z) y))))).
tt('thm/HolSmt/r136_', ax, (![x : 'type/realax/real', u : 'type/realax/real']: ((('const/real/real_of_num' 'const/num/0') = ('const/realax/real_mul' ('const/realax/real_neg' u) x)) = (('const/realax/real_mul' u x) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r137_', ax, (![x : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_mul' ('const/realax/real_neg' u) x)) = (('const/realax/real_mul' u x) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r138_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' x ('const/realax/real_add' y z))) = (('const/realax/real_add' x ('const/realax/real_add' y ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) a) z))) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r139_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' x ('const/realax/real_add' y z))) = (('const/realax/real_add' x ('const/realax/real_add' y ('const/realax/real_add' z ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) a)))) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r140_', ax, (![z : 'type/realax/real', y : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) y) ('const/realax/real_mul' v z))) = (('const/realax/real_add' ('const/realax/real_mul' u y) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) z) a)) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r141_', ax, (![z : 'type/realax/real', y : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) y) ('const/realax/real_mul' ('const/realax/real_neg' v) z))) = (('const/realax/real_add' ('const/realax/real_mul' u y) ('const/realax/real_add' a ('const/realax/real_mul' v z))) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r142_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_neg' a) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) = a)))).
tt('thm/HolSmt/r143_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' w) z) a))) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r144_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r145_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r146_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r147_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r148_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_neg' a) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = a)))).
tt('thm/HolSmt/r149_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_neg' a) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) = a)))).
tt('thm/HolSmt/r150_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_neg' a) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = a)))).
tt('thm/HolSmt/r151_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_neg' a) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) = a)))).
tt('thm/HolSmt/r152_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/realax/real_mul' w z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' y ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r153_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((a = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z)))) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' y ('const/realax/real_mul' w z))) = ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r154_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) = ('const/realax/real_neg' a)) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' v y)) = a)))).
tt('thm/HolSmt/r155_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = ('const/realax/real_neg' a)) = (('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) = a)))).
tt('thm/HolSmt/r156_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) = ('const/realax/real_neg' a)) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = a)))).
tt('thm/HolSmt/r157_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) = ('const/realax/real_neg' a)) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = a)))).
tt('thm/HolSmt/r158_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: ((('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) = ('const/realax/real_neg' a)) = (('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) = a)))).
tt('thm/HolSmt/r159_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_ge' ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_lte' y x)))).
tt('thm/HolSmt/r160_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_ge' x y) = ('const/real/real_ge' ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r161_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_gt' x y) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r162_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_lte' x y) = ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r163_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_lte' x ('const/realax/real_add' y z)) = ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) y)))).
tt('thm/HolSmt/r164_', ax, (![x : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_mul' ('const/realax/real_neg' u) x) a) = ('const/real/real_ge' ('const/realax/real_mul' u x) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r165_', ax, (![x : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_mul' u x) a)))).
tt('thm/HolSmt/r166_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y)) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r167_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y)) a) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r168_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y)) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) a)))).
tt('thm/HolSmt/r169_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) a) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' v y)) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r170_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' v y)) a)))).
tt('thm/HolSmt/r171_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r172_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r173_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r174_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/r175_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) a) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r176_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a)))).
tt('thm/HolSmt/r177_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r178_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) a)))).
tt('thm/HolSmt/r179_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) a) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r180_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a)))).
tt('thm/HolSmt/r181_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a))))).
tt('thm/HolSmt/r182_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) a)))).
tt('thm/HolSmt/r183_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = ('const/real/real_ge' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a)))).
tt('thm/HolSmt/r184_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_lt' x y) = (~ ('const/real/real_ge' x y))))).
tt('thm/HolSmt/r185_', ax, (![x : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_mul' ('const/realax/real_neg' u) x) a) = (~ ('const/real/real_lte' ('const/realax/real_mul' u x) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r186_', ax, (![x : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_mul' u x) a))))).
tt('thm/HolSmt/r187_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y)) ('const/real/real_of_num' 'const/num/0')) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r188_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/real/real_of_num' 'const/num/0')) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' v y)) ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r189_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y)) a) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r190_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' v y)) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) a))))).
tt('thm/HolSmt/r191_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) a) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' v y)) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r192_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_mul' ('const/realax/real_neg' v) y)) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_mul' v y)) a))))).
tt('thm/HolSmt/r193_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r194_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a))))).
tt('thm/HolSmt/r195_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r196_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) a))))).
tt('thm/HolSmt/r197_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r198_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a))))).
tt('thm/HolSmt/r199_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r200_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) a))))).
tt('thm/HolSmt/r201_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/real/real_of_num' 'const/num/0')) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r202_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/real/real_of_num' 'const/num/0')) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/HolSmt/r203_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r204_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a))))).
tt('thm/HolSmt/r205_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r206_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) a))))).
tt('thm/HolSmt/r207_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r208_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a))))).
tt('thm/HolSmt/r209_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) a) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) ('const/realax/real_neg' a)))))).
tt('thm/HolSmt/r210_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', v : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' w z))) a))))).
tt('thm/HolSmt/r211_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', w : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/realax/real_mul' ('const/realax/real_neg' w) z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' y ('const/realax/real_mul' w z))) a))))).
tt('thm/HolSmt/r212_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real', a : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) x) ('const/realax/real_add' ('const/realax/real_mul' v y) ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z))) ('const/realax/real_neg' a)) = (~ ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' u x) ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' v) y) z)) a))))).
tt('thm/HolSmt/r213_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' ('const/real/real_of_num' 'const/num/0') x) = x))).
tt('thm/HolSmt/r214_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' x ('const/real/real_of_num' 'const/num/0')) = x))).
tt('thm/HolSmt/r215_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' x y) = ('const/realax/real_add' y x)))).
tt('thm/HolSmt/r216_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' x x) = ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)))).
tt('thm/HolSmt/r217_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' ('const/realax/real_add' x y) z) = ('const/realax/real_add' x ('const/realax/real_add' y z))))).
tt('thm/HolSmt/r218_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' ('const/realax/real_add' x y) z) = ('const/realax/real_add' x ('const/realax/real_add' z y))))).
tt('thm/HolSmt/r219_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' x ('const/realax/real_add' y z)) = ('const/realax/real_add' y ('const/realax/real_add' z x))))).
tt('thm/HolSmt/r220_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' x ('const/realax/real_add' y z)) = ('const/realax/real_add' y ('const/realax/real_add' x z))))).
tt('thm/HolSmt/r221_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' ('const/real/real_of_num' 'const/num/0') x) = ('const/realax/real_neg' x)))).
tt('thm/HolSmt/r222_', ax, (![x : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_sub' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' u x)) = ('const/realax/real_mul' ('const/realax/real_neg' u) x)))).
tt('thm/HolSmt/r223_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' x ('const/real/real_of_num' 'const/num/0')) = x))).
tt('thm/HolSmt/r224_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_sub' x y) = ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y))))).
tt('thm/HolSmt/r225_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_sub' x y) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) x)))).
tt('thm/HolSmt/r226_', ax, (![y : 'type/realax/real', x : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_sub' x ('const/realax/real_mul' u y)) = ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' u) y))))).
tt('thm/HolSmt/r227_', ax, (![y : 'type/realax/real', x : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_sub' x ('const/realax/real_mul' u y)) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) y) x)))).
tt('thm/HolSmt/r228_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) z) = ('const/realax/real_add' x ('const/realax/real_add' y ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)))))).
tt('thm/HolSmt/r229_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) z) = ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z) y))))).
tt('thm/HolSmt/r230_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) ('const/realax/real_mul' u z)) = ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) z) ('const/realax/real_add' x y))))).
tt('thm/HolSmt/r231_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) ('const/realax/real_mul' u z)) = ('const/realax/real_add' x ('const/realax/real_add' ('const/realax/real_mul' ('const/realax/real_neg' u) z) y))))).
tt('thm/HolSmt/r232_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real', u : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) ('const/realax/real_mul' u z)) = ('const/realax/real_add' x ('const/realax/real_add' y ('const/realax/real_mul' ('const/realax/real_neg' u) z)))))).
tt('thm/HolSmt/r233_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' ('const/real/real_of_num' 'const/num/0') x) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/HolSmt/r234_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) = x))).
tt('thm/HolSmt/r235_', ax, ![A : $t]: (![x : ('type/fcp/cart' $o A)]: ((('const/words/word_add' A) (('const/words/n2w' A) 'const/num/0') x) = x))).
tt('thm/HolSmt/r236_', ax, ![A : $t]: (![y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_add' A) x y) = (('const/words/word_add' A) y x)))).
tt('thm/HolSmt/r237_', ax, ![A : $t]: (![x : ('type/fcp/cart' $o A)]: ((('const/words/word_add' A) (('const/words/n2w' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/words/word_add' A) (('const/words/n2w' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x)) = (('const/words/word_add' A) (('const/words/n2w' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)))).
tt('thm/HolSmt/r238_', ax, ![A : $t]: (![z : ('type/fcp/cart' $o A), y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: (((('const/words/word_add' A) x z) = (('const/words/word_add' A) y x)) = (y = z)))).
tt('thm/HolSmt/r239_', ax, ![C : $t, B : $t, A : $t]: (![x : 'type/num/num']: (('const/prim_rec/<' x (('const/words/dimword' B) ('const/bool/the_value' B))) => ((('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A)) => ((('const/words/word_concat' A B C) (('const/words/n2w' A) 'const/num/0') (('const/words/n2w' B) x)) = (('const/words/n2w' C) x)))))).
tt('thm/HolSmt/r240_', ax, ![B : $t, A : $t]: (![x : 'type/num/num']: (('const/prim_rec/<' x (('const/words/dimword' A) ('const/bool/the_value' A))) => ((('const/words/w2w' A B) (('const/words/n2w' A) x)) = (('const/words/n2w' B) x))))).
tt('thm/HolSmt/r241_', ax, ![B : $t, C : $t, A : $t]: (![y : 'type/num/num', x : ('type/fcp/cart' $o B)]: (('const/arithmetic/<=' (('const/fcp/dimindex' B) ('const/bool/the_value' B)) (('const/fcp/dimindex' C) ('const/bool/the_value' C))) => (('const/prim_rec/<' y (('const/words/dimword' B) ('const/bool/the_value' B))) => ((('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A)) => (((('const/words/word_concat' A B C) (('const/words/n2w' A) 'const/num/0') x) = (('const/words/n2w' C) y)) = (x = (('const/words/n2w' B) y)))))))).
tt('thm/HolSmt/r242_', ax, ![B : $t, C : $t, A : $t]: (![y : 'type/num/num', x : ('type/fcp/cart' $o B)]: (('const/arithmetic/<=' (('const/fcp/dimindex' B) ('const/bool/the_value' B)) (('const/fcp/dimindex' C) ('const/bool/the_value' C))) => (('const/prim_rec/<' y (('const/words/dimword' B) ('const/bool/the_value' B))) => ((('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A)) => (((('const/words/word_concat' A B C) (('const/words/n2w' A) 'const/num/0') x) = (('const/words/n2w' C) y)) = ((('const/words/n2w' B) y) = x))))))).
tt('thm/HolSmt/r243_', ax, ![B : $t, A : $t, C : $t]: (![y : 'type/num/num', x : ('type/fcp/cart' $o B)]: (('const/arithmetic/<=' (('const/fcp/dimindex' B) ('const/bool/the_value' B)) (('const/fcp/dimindex' C) ('const/bool/the_value' C))) => (('const/prim_rec/<' y (('const/words/dimword' B) ('const/bool/the_value' B))) => ((('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A)) => (((('const/words/n2w' C) y) = (('const/words/word_concat' A B C) (('const/words/n2w' A) 'const/num/0') x)) = (x = (('const/words/n2w' B) y)))))))).
tt('thm/HolSmt/r244_', ax, ![B : $t, A : $t, C : $t]: (![y : 'type/num/num', x : ('type/fcp/cart' $o B)]: (('const/arithmetic/<=' (('const/fcp/dimindex' B) ('const/bool/the_value' B)) (('const/fcp/dimindex' C) ('const/bool/the_value' C))) => (('const/prim_rec/<' y (('const/words/dimword' B) ('const/bool/the_value' B))) => ((('const/pred_set/FINITE' A) ('const/pred_set/UNIV' A)) => (((('const/words/n2w' C) y) = (('const/words/word_concat' A B C) (('const/words/n2w' A) 'const/num/0') x)) = ((('const/words/n2w' B) y) = x))))))).
tt('thm/HolSmt/r245_', ax, ![A : $t]: (![y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_and' A) x y) = (('const/words/word_and' A) y x)))).
tt('thm/HolSmt/r246_', ax, ![A : $t]: (![z : ('type/fcp/cart' $o A), y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_and' A) x (('const/words/word_and' A) y z)) = (('const/words/word_and' A) y (('const/words/word_and' A) x z))))).
tt('thm/HolSmt/r247_', ax, ![A : $t]: (![z : ('type/fcp/cart' $o A), y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_and' A) x (('const/words/word_and' A) y z)) = (('const/words/word_and' A) (('const/words/word_and' A) x y) z)))).
tt('thm/HolSmt/r248_', ax, (![y : ('type/fcp/cart' $o 'type/one/one'), x : ('type/fcp/cart' $o 'type/one/one')]: (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (('const/words/word_and' 'type/one/one') x y)) = (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x) & ((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = y))))).
tt('thm/HolSmt/r249_', ax, (![y : ('type/fcp/cart' $o 'type/one/one'), x : ('type/fcp/cart' $o 'type/one/one')]: (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (('const/words/word_and' 'type/one/one') x y)) = (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = y) & ((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x))))).
tt('thm/HolSmt/r250_', ax, (![x : ('type/fcp/cart' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))]: ((('const/words/word_extract' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))) ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/num/0' x) = x))).
tt('thm/HolSmt/r251_', ax, ![A : $t]: (![y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_lo' A) x y) = (~ (('const/words/word_ls' A) y x))))).
tt('thm/HolSmt/r252_', ax, ![A : $t]: (![y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_mul' A) x y) = (('const/words/word_mul' A) y x)))).
tt('thm/HolSmt/r253_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: ((('const/words/word_extract' 'type/one/one' 'type/one/one') 'const/num/0' 'const/num/0' x) = x))).
tt('thm/HolSmt/r254_', ax, ![A : $t]: (![z : ('type/fcp/cart' $o A), y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: ((('const/words/word_and' A) (('const/words/word_and' A) x y) z) = (('const/words/word_and' A) x (('const/words/word_and' A) y z))))).
tt('thm/HolSmt/r255_', ax, ![A : $t]: (![x : ('type/fcp/cart' $o A)]: ((('const/words/word_or' A) (('const/words/n2w' A) 'const/num/0') x) = x))).
tt('thm/HolSmt/t001_', ax, ![A : $t, B : $t]: (![z : B, y : A, x : A, f : (A > B)]: ((x = y) | ((f x) = (('const/combin/UPDATE' A B) y z f x))))).
tt('thm/HolSmt/t002_', ax, ![A : $t, B : $t]: (![z : B, y : A, x : A, f : (A > B)]: ((x = y) | ((f y) = (('const/combin/UPDATE' A B) x z f y))))).
tt('thm/HolSmt/t003_', ax, ![A : $t, B : $t]: (![z : B, y : A, x : A, f : (A > B)]: ((x = y) | ((('const/combin/UPDATE' A B) y z f x) = (f x))))).
tt('thm/HolSmt/t004_', ax, ![A : $t, B : $t]: (![z : B, y : A, x : A, f : (A > B)]: ((x = y) | ((('const/combin/UPDATE' A B) x z f y) = (f y))))).
tt('thm/HolSmt/t005_', ax, ![A : $t, B : $t]: (![g : (A > B), f : (A > B)]: ((f = g) | (~ ((f (('const/HolSmt/array_ext' A B) f g)) = (g (('const/HolSmt/array_ext' A B) f g))))))).
tt('thm/HolSmt/t006_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((~ (x = y)) | ('const/integer/int_le' x y)))).
tt('thm/HolSmt/t007_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((~ (x = y)) | ('const/integer/int_ge' x y)))).
tt('thm/HolSmt/t008_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((~ (x = y)) | ('const/integer/int_ge' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/t009_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((~ (x = y)) | ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/t010_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: ((x = y) | ((~ ('const/integer/int_le' x y)) | (~ ('const/integer/int_ge' x y)))))).
tt('thm/HolSmt/t011_', ax, (![x : 'type/integer/int']: ((~ ('const/integer/int_le' x ('const/integer/int_of_num' 'const/num/0'))) | ('const/integer/int_le' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/HolSmt/t012_', ax, (![x : 'type/integer/int']: ((~ ('const/integer/int_le' x ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) | ('const/integer/int_le' x ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/HolSmt/t013_', ax, (![x : 'type/integer/int']: ((~ ('const/integer/int_ge' x ('const/integer/int_of_num' 'const/num/0'))) | ('const/integer/int_ge' x ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/HolSmt/t014_', ax, (![x : 'type/integer/int']: ((~ ('const/integer/int_ge' x ('const/integer/int_of_num' 'const/num/0'))) | (~ ('const/integer/int_le' x ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/HolSmt/t015_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_ge' x y) | ('const/integer/int_le' x y)))).
tt('thm/HolSmt/t016_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: ((~ (x = y)) | ('const/real/real_ge' ('const/realax/real_add' x ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/HolSmt/t017_', ax, ![A : $t]: (![x : ('type/fcp/cart' $o A)]: (~ (x = (('const/words/word_1comp' A) x))))).
tt('thm/HolSmt/t018_', ax, ![A : $t]: (![y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A), i : 'type/num/num']: ((x = y) => ((('const/fcp/fcp_index' $o A) x i) => (('const/fcp/fcp_index' $o A) y i))))).
tt('thm/HolSmt/t019_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (('const/words/word_1comp' 'type/one/one') x)) | (('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0')))).
tt('thm/HolSmt/t020_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: ((('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0') => ((('const/words/n2w' 'type/one/one') 'const/num/0') = (('const/words/word_1comp' 'type/one/one') x))))).
tt('thm/HolSmt/t021_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: ((('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0') => ((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x)))).
tt('thm/HolSmt/t022_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: ((~ (('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0')) => ((('const/words/n2w' 'type/one/one') 'const/num/0') = x)))).
tt('thm/HolSmt/t023_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: ((~ (('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0')) => ((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (('const/words/word_1comp' 'type/one/one') x))))).
tt('thm/HolSmt/t024_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: (((('const/words/n2w' 'type/one/one') 'const/num/0') = (('const/words/word_1comp' 'type/one/one') x)) | (~ (('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0'))))).
tt('thm/HolSmt/t025_', ax, (![y : ('type/fcp/cart' $o 'type/one/one'), x : ('type/fcp/cart' $o 'type/one/one')]: (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (('const/words/word_or' 'type/one/one') (('const/words/word_1comp' 'type/one/one') x) (('const/words/word_1comp' 'type/one/one') y))) | (~ ((~ (('const/fcp/fcp_index' $o 'type/one/one') x 'const/num/0')) | (~ (('const/fcp/fcp_index' $o 'type/one/one') y 'const/num/0'))))))).
tt('thm/HolSmt/t026_', ax, (![x : ('type/fcp/cart' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))]: (((('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) 'const/num/0') = x) | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x 'const/num/0') | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) | ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) | (('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))))).
tt('thm/HolSmt/t027_', ax, (![x : ('type/fcp/cart' $o 'type/one/one'), p : $o]: (((x = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = p) = (x = (('const/bool/COND' ('type/fcp/cart' $o 'type/one/one')) p (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/words/n2w' 'type/one/one') 'const/num/0')))))).
tt('thm/HolSmt/t028_', ax, (![x : ('type/fcp/cart' $o 'type/one/one'), p : $o]: ((((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x) = p) = (x = (('const/bool/COND' ('type/fcp/cart' $o 'type/one/one')) p (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/words/n2w' 'type/one/one') 'const/num/0')))))).
tt('thm/HolSmt/t029_', ax, (![x : ('type/fcp/cart' $o 'type/one/one'), p : $o]: ((p = (x = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (x = (('const/bool/COND' ('type/fcp/cart' $o 'type/one/one')) p (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/words/n2w' 'type/one/one') 'const/num/0')))))).
tt('thm/HolSmt/t030_', ax, (![x : ('type/fcp/cart' $o 'type/one/one'), p : $o]: ((p = ((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x)) = (x = (('const/bool/COND' ('type/fcp/cart' $o 'type/one/one')) p (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/words/n2w' 'type/one/one') 'const/num/0')))))).
tt('thm/HolSmt/t031_', ax, (![x : ('type/fcp/cart' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))]: (((('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) 'const/num/0') = (('const/words/word_mul' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) (('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))))))))))))))))))))) (('const/words/sw2sw' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))) ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) x))) => (~ (('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x 'const/num/0'))))).
tt('thm/HolSmt/t032_', ax, (![x : ('type/fcp/cart' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))]: (((('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) 'const/num/0') = (('const/words/word_mul' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) (('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))))))))))))))))))))) (('const/words/sw2sw' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))) ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) x))) => (~ ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (~ (('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x 'const/num/0'))))))).
tt('thm/HolSmt/t033_', ax, (![x : ('type/fcp/cart' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))]: (((('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) 'const/num/0') = (('const/words/word_mul' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) (('const/words/n2w' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))))))))))))))))))))) (('const/words/sw2sw' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))) ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) x))) => (~ ((('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ((~ (('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x 'const/num/0')) & (~ (('const/fcp/fcp_index' $o ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))).
tt('thm/HolSmt/t034_', ax, ![A : $t]: (![y : ('type/fcp/cart' $o A), x : ('type/fcp/cart' $o A)]: (((('const/words/word_add' A) (('const/words/n2w' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) = y) => ((('const/fcp/fcp_index' $o A) x 'const/num/0') => (~ (('const/fcp/fcp_index' $o A) y 'const/num/0')))))).
tt('thm/HolSmt/t035_', ax, (![x : ('type/fcp/cart' $o 'type/one/one')]: (((('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x) | (~ ((('const/words/word_extract' 'type/one/one' 'type/one/one') 'const/num/0' 'const/num/0' x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/HolSmt/p001_', ax, ![A : $t]: ('const/prim_rec/<' 'const/num/0' (('const/words/dimword' A) ('const/bool/the_value' A)))).
tt('thm/HolSmt/p002_', ax, ![A : $t]: ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/words/dimword' A) ('const/bool/the_value' A)))).
tt('thm/HolSmt/p003_', ax, ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) (('const/words/dimword' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) ('const/bool/the_value' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))))).
tt('thm/HolSmt/p004_', ax, (('const/pred_set/FINITE' 'type/one/one') ('const/pred_set/UNIV' 'type/one/one'))).
tt('thm/HolSmt/p005_', ax, (('const/pred_set/FINITE' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))) ('const/pred_set/UNIV' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))))).
tt('thm/HolSmt/p006_', ax, (('const/pred_set/FINITE' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit1' 'type/one/one'))))) ('const/pred_set/UNIV' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit1' 'type/one/one'))))))).
tt('thm/HolSmt/p007_', ax, (('const/pred_set/FINITE' ('type/fcp/bit0' ('type/fcp/bit1' ('type/fcp/bit1' ('type/fcp/bit1' 'type/one/one'))))) ('const/pred_set/UNIV' ('type/fcp/bit0' ('type/fcp/bit1' ('type/fcp/bit1' ('type/fcp/bit1' 'type/one/one'))))))).
tt('thm/HolSmt/p008_', ax, (('const/pred_set/FINITE' ('type/fcp/bit1' ('type/fcp/bit1' ('type/fcp/bit1' ('type/fcp/bit1' 'type/one/one'))))) ('const/pred_set/UNIV' ('type/fcp/bit1' ('type/fcp/bit1' ('type/fcp/bit1' ('type/fcp/bit1' 'type/one/one'))))))).
tt('thm/HolSmt/p009_', ax, ('const/arithmetic/<=' (('const/fcp/dimindex' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))) ('const/bool/the_value' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))) (('const/fcp/dimindex' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one')))))) ('const/bool/the_value' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' ('type/fcp/bit0' 'type/one/one'))))))))).
