HOL html
| Files Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Theorems Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
C (theorems)
CCOS_0CCOS_ADD
CCOS_DOUBLE
CCOS_NEG
CEXP_0
CEXP_ADD
CEXP_CLOG
CEXP_EULER
CEXP_MUL
CEXP_NEG
CEXP_NEG_LMUL
CEXP_NEG_RMUL
CEXP_NONZERO
CEXP_SUB
CLOG_MUL
CLOG_WORKS
CNJ_ADD
CNJ_CNJ
CNJ_CX
CNJ_DIV
CNJ_INJ
CNJ_INV
CNJ_MUL
CNJ_NEG
CNJ_POW
CNJ_SUB
COMPLEX
COMPLEX_ABS_NORM
COMPLEX_ADD2_SUB2
COMPLEX_ADD_AC
COMPLEX_ADD_ASSOC
COMPLEX_ADD_LDISTRIB
COMPLEX_ADD_LID
COMPLEX_ADD_LINV
COMPLEX_ADD_RDISTRIB
COMPLEX_ADD_RID
COMPLEX_ADD_RINV
COMPLEX_ADD_SUB
COMPLEX_ADD_SUB2
COMPLEX_ADD_SYM
COMPLEX_DIFFSQ
COMPLEX_DIV_LMUL
COMPLEX_DIV_REFL
COMPLEX_DIV_RMUL
COMPLEX_ENTIRE
COMPLEX_EQ
COMPLEX_EQ_ADD_LCANCEL
COMPLEX_EQ_ADD_LCANCEL_0
COMPLEX_EQ_ADD_RCANCEL
COMPLEX_EQ_ADD_RCANCEL_0
COMPLEX_EQ_MUL_LCANCEL
COMPLEX_EQ_MUL_RCANCEL
COMPLEX_EQ_NEG2
COMPLEX_EQ_SUB_LADD
COMPLEX_EQ_SUB_RADD
COMPLEX_II_NZ
COMPLEX_INV_0
COMPLEX_INV_1
COMPLEX_INV_INV
COMPLEX_INV_MUL
COMPLEX_LNEG_UNIQ
COMPLEX_MUL_2
COMPLEX_MUL_AC
COMPLEX_MUL_ASSOC
COMPLEX_MUL_LID
COMPLEX_MUL_LINV
COMPLEX_MUL_LINV_UNIQ
COMPLEX_MUL_LNEG
COMPLEX_MUL_LZERO
COMPLEX_MUL_RID
COMPLEX_MUL_RINV
COMPLEX_MUL_RINV_UNIQ
COMPLEX_MUL_RNEG
COMPLEX_MUL_RZERO
COMPLEX_MUL_SYM
COMPLEX_NEG_0
COMPLEX_NEG_ADD
COMPLEX_NEG_EQ
COMPLEX_NEG_EQ_0
COMPLEX_NEG_LMUL
COMPLEX_NEG_MINUS1
COMPLEX_NEG_MUL2
COMPLEX_NEG_NEG
COMPLEX_NEG_RMUL
COMPLEX_NEG_SUB
COMPLEX_NORM_0
COMPLEX_NORM_ABS_NORM
COMPLEX_NORM_CNJ
COMPLEX_NORM_CX
COMPLEX_NORM_DIV
COMPLEX_NORM_GE_RE_IM
COMPLEX_NORM_INV
COMPLEX_NORM_MUL
COMPLEX_NORM_NEG
COMPLEX_NORM_NUM
COMPLEX_NORM_NZ
COMPLEX_NORM_POS
COMPLEX_NORM_POW
COMPLEX_NORM_TRIANGLE
COMPLEX_NORM_TRIANGLE_SUB
COMPLEX_NORM_ZERO
COMPLEX_POLY_CLAUSES
COMPLEX_POW_1
COMPLEX_POW_2
COMPLEX_POW_ADD
COMPLEX_POW_DIV
COMPLEX_POW_EQ_0
COMPLEX_POW_II_2
COMPLEX_POW_INV
COMPLEX_POW_MUL
COMPLEX_POW_NEG
COMPLEX_POW_ONE
COMPLEX_POW_POW
COMPLEX_RNEG_UNIQ
COMPLEX_SUB_0
COMPLEX_SUB_ADD
COMPLEX_SUB_ADD2
COMPLEX_SUB_LDISTRIB
COMPLEX_SUB_LNEG
COMPLEX_SUB_LZERO
COMPLEX_SUB_NEG2
COMPLEX_SUB_RDISTRIB
COMPLEX_SUB_REFL
COMPLEX_SUB_RNEG
COMPLEX_SUB_RZERO
COMPLEX_SUB_SUB
COMPLEX_SUB_SUB2
COMPLEX_SUB_TRIANGLE
COMPLEX_UNIMODULAR_POLAR
CONSTANT_DEGREE
COS_INTEGER_2PI
CSIN_0
CSIN_ADD
CSIN_CIRCLE
CSIN_DOUBLE
CSIN_NEG
CSQRT
CX_ABS
CX_ADD
CX_CEXP
CX_DEF
CX_DIV
CX_INJ
CX_INV
CX_MUL
CX_NEG
CX_POW
CX_SUB
ccos
cexp
clog
cnj
collinear
complex_add
complex_div
complex_inv
complex_mul
complex_neg
complex_norm
complex_pow
complex_sub
constant
csin
csqrt