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 | _ |
R (theorems)
RC_CLOSEDRC_EXPLICIT
RC_IDEMP
RC_INC
RC_INV
RC_MONO
RC_REFL
RC_SC
RC_SYM
RC_TC
RC_TRANS
RELPOW
RELPOW_LEMMA
RELPOW_LEMMA_1
RELPOW_LEMMA_2
RELPOW_M
RELPOW_R
RELPOW_SEQUENCE
RSC
RSC_CASES
RSC_CLOSED
RSC_IDEMP
RSC_INC
RSC_INC_RC
RSC_INC_SC
RSC_INDUCT
RSC_INV
RSC_MONO
RSC_REFL
RSC_SYM
RSTC
RSTC_CASES
RSTC_CASES_L
RSTC_CASES_R
RSTC_CLOSED
RSTC_IDEMP
RSTC_INC
RSTC_INC_RC
RSTC_INC_RSC
RSTC_INC_RTC
RSTC_INC_SC
RSTC_INC_STC
RSTC_INC_TC
RSTC_INDUCT
RSTC_INV
RSTC_MONO
RSTC_REFL
RSTC_RULES
RSTC_SYM
RSTC_TRANS
RSTC_TRANS_L
RSTC_TRANS_R
RTC
RTCP
RTC_CASES
RTC_CASES_L
RTC_CASES_R
RTC_CLOSED
RTC_IDEMP
RTC_INC
RTC_INC_RC
RTC_INC_TC
RTC_INDUCT
RTC_INDUCT_L
RTC_INDUCT_R
RTC_INV
RTC_MONO
RTC_NE_IMP_TC
RTC_REFL
RTC_RELPOW
RTC_RULES
RTC_SIGMA
RTC_STUTTER
RTC_SYM
RTC_TRANS
RTC_TRANS_L
RTC_TRANS_R
robinson