Theory "relation"

Parents     normalForms   combin   label

Signature

Constant Type
trichotomous :('a -> 'a -> bool) -> bool
transitive :('a -> 'a -> bool) -> bool
total :('a -> 'a -> bool) -> bool
the_fun :('a -> 'a -> bool) -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'a -> 'b
symmetric :('a -> 'a -> bool) -> bool
reflexive :('a -> 'a -> bool) -> bool
rcdiamond :('a -> 'a -> bool) -> bool
nf :('a -> 'b -> bool) -> 'a -> bool
irreflexive :('a -> 'a -> bool) -> bool
inv_image :('b -> 'b -> bool) -> ('a -> 'b) -> 'a -> 'a -> bool
inv :('a -> 'a -> bool) -> 'a -> 'a -> bool
equivalence :('a -> 'a -> bool) -> bool
diamond :('a -> 'a -> bool) -> bool
diag :('a -> bool) -> 'a -> 'a -> bool
approx :('a -> 'a -> bool) -> (('a -> 'b) -> 'a -> 'b) -> 'a -> ('a -> 'b) -> bool
antisymmetric :('a -> 'a -> bool) -> bool
WeakOrder :('g -> 'g -> bool) -> bool
WeakLinearOrder :('a -> 'a -> bool) -> bool
WFREC :('a -> 'a -> bool) -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
WFP :('a -> 'a -> bool) -> 'a -> bool
WF :('a -> 'a -> bool) -> bool
WCR :('a -> 'a -> bool) -> bool
TC :('a -> 'a -> bool) -> 'a -> 'a -> bool
StrongOrder :('g -> 'g -> bool) -> bool
StrongLinearOrder :('a -> 'a -> bool) -> bool
STRORD :('a -> 'a -> bool) -> 'a -> 'a -> bool
SN :('a -> 'a -> bool) -> bool
SC :('a -> 'a -> bool) -> 'a -> 'a -> bool
RUNIV :'a -> 'b -> bool
RUNION :('a -> 'b -> bool) -> ('a -> 'b -> bool) -> 'a -> 'b -> bool
RTC :('a -> 'a -> bool) -> 'a -> 'a -> bool
RSUBSET :('a -> 'b -> bool) -> ('a -> 'b -> bool) -> bool
RRANGE :('a -> 'b -> bool) -> 'b -> bool
RINTER :('a -> 'b -> bool) -> ('a -> 'b -> bool) -> 'a -> 'b -> bool
RESTRICT :('a -> 'b) -> ('a -> 'a -> bool) -> 'a -> 'a -> 'b
RDOM :('a -> 'b -> bool) -> 'a -> bool
RCOMPL :('a -> 'b -> bool) -> 'a -> 'b -> bool
RC :('a -> 'a -> bool) -> 'a -> 'a -> bool
PreOrder :('a -> 'a -> bool) -> bool
Order :('g -> 'g -> bool) -> bool
O :('g -> 'h -> bool) -> ('h -> 'k -> bool) -> 'g -> 'k -> bool
LinearOrder :('a -> 'a -> bool) -> bool
INVOL :('z -> 'z) -> bool
INDUCTIVE_INVARIANT_ON :('a -> 'a -> bool) -> ('a -> bool) -> ('a -> 'b -> bool) -> (('a -> 'b) -> 'a -> 'b) -> bool
INDUCTIVE_INVARIANT :('a -> 'a -> bool) -> ('a -> 'b -> bool) -> (('a -> 'b) -> 'a -> 'b) -> bool
IDEM :('z -> 'z) -> bool
EQC :('a -> 'a -> bool) -> 'a -> 'a -> bool
EMPTY_REL :'a -> 'a -> bool
CR :('a -> 'a -> bool) -> bool

Definitions

transitive_def 
|- !R. transitive R = !x y z. R x y /\ R y z ==> R x z
reflexive_def 
|- !R. reflexive R = !x. R x x
irreflexive_def 
|- !R. irreflexive R = !x. ~R x x
symmetric_def 
|- !R. symmetric R = !x y. R x y = R y x
antisymmetric_def 
|- !R. antisymmetric R = !x y. R x y /\ R y x ==> (x = y)
equivalence_def 
|- !R. equivalence R = reflexive R /\ symmetric R /\ transitive R
total_def 
|- !R. total R = !x y. R x y \/ R y x
trichotomous 
|- !R. trichotomous R = !a b. R a b \/ R b a \/ (a = b)
TC_DEF 
|- !R a b.
     TC R a b =
     !P.
       (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==> P a b
RTC_DEF 
|- !R a b.
     RTC R a b =
     !P. (!x. P x x) /\ (!x y z. R x y /\ P y z ==> P x z) ==> P a b
RC_DEF 
|- !R x y. RC R x y = (x = y) \/ R x y
SC_DEF 
|- !R x y. SC R x y = R x y \/ R y x
EQC_DEF 
|- !R. EQC R = RC (TC (SC R))
WF_DEF 
|- !R. WF R = !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b
EMPTY_REL_DEF 
|- !x y. REMPTY x y = F
inv_image_def 
|- !R f. inv_image R f = (\x y. R (f x) (f y))
RESTRICT_DEF 
|- !f R x. RESTRICT f R x = (\y. (if R y x then f y else ARB))
approx_def 
|- !R M x f. approx R M x f = (f = RESTRICT (\y. M (RESTRICT f R y) y) R x)
the_fun_def 
|- !R M x. the_fun R M x = @f. approx R M x f
WFREC_DEF 
|- !R M.
     WFREC R M =
     (\x. M (RESTRICT (the_fun (TC R) (\f v. M (RESTRICT f R v) v) x) R x) x)
WFP_DEF 
|- !R a. WFP R a = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> P a
INDUCTIVE_INVARIANT_DEF 
|- !R P M.
     INDUCTIVE_INVARIANT R P M =
     !f x. (!y. R y x ==> P y (f y)) ==> P x (M f x)
INDUCTIVE_INVARIANT_ON_DEF 
|- !R D P M.
     INDUCTIVE_INVARIANT_ON R D P M =
     !f x. D x /\ (!y. D y ==> R y x ==> P y (f y)) ==> P x (M f x)
inv_DEF 
|- !R x y. inv R x y = R y x
INVOL_DEF 
|- !f. INVOL f = (f o f = I)
IDEM_DEF 
|- !f. IDEM f = (f o f = f)
O_DEF 
|- !R1 R2 x z. (R1 O R2) x z = ?y. R1 x y /\ R2 y z
RSUBSET 
|- !R1 R2. R1 RSUBSET R2 = !x y. R1 x y ==> R2 x y
RUNION 
|- !R1 R2 x y. (R1 RUNION R2) x y = R1 x y \/ R2 x y
RINTER 
|- !R1 R2 x y. (R1 RINTER R2) x y = R1 x y /\ R2 x y
RCOMPL 
|- !R x y. RCOMPL R x y = ~R x y
PreOrder 
|- !R. PreOrder R = reflexive R /\ transitive R
Order 
|- !Z. Order Z = antisymmetric Z /\ transitive Z
WeakOrder 
|- !Z. WeakOrder Z = reflexive Z /\ antisymmetric Z /\ transitive Z
StrongOrder 
|- !Z. StrongOrder Z = irreflexive Z /\ antisymmetric Z /\ transitive Z
STRORD 
|- !R a b. STRORD R a b = R a b /\ ~(a = b)
LinearOrder 
|- !R. LinearOrder R = Order R /\ trichotomous R
StrongLinearOrder 
|- !R. StrongLinearOrder R = StrongOrder R /\ trichotomous R
WeakLinearOrder 
|- !R. WeakLinearOrder R = WeakOrder R /\ trichotomous R
diag_def 
|- !A x y. diag A x y = (x = y) /\ x IN A
RDOM_DEF 
|- !R x. RDOM R x = ?y. R x y
RRANGE 
|- !R y. RRANGE R y = ?x. R x y
RUNIV 
|- !x y. RUNIV x y = T
diamond_def 
|- !R. diamond R = !x y z. R x y /\ R x z ==> ?u. R y u /\ R z u
rcdiamond_def 
|- !R. rcdiamond R = !x y z. R x y /\ R x z ==> ?u. RC R y u /\ RC R z u
CR_def 
|- !R. CR R = diamond (RTC R)
WCR_def 
|- !R. WCR R = !x y z. R x y /\ R x z ==> ?u. RTC R y u /\ RTC R z u
SN_def 
|- !R. SN R = WF (inv R)
nf_def 
|- !R x. nf R x = !y. ~R x y

Theorems

SC_SYMMETRIC 
|- !R. symmetric (SC R)
TC_TRANSITIVE 
|- !R. transitive (TC R)
RTC_INDUCT 
|- !R P.
     (!x. P x x) /\ (!x y z. R x y /\ P y z ==> P x z) ==>
     !x y. RTC R x y ==> P x y
TC_RULES 
|- !R. (!x y. R x y ==> TC R x y) /\ !x y z. TC R x y /\ TC R y z ==> TC R x z
RTC_RULES 
|- !R. (!x. RTC R x x) /\ !x y z. R x y /\ RTC R y z ==> RTC R x z
RTC_STRONG_INDUCT 
|- !R P.
     (!x. P x x) /\ (!x y z. R x y /\ RTC R y z /\ P y z ==> P x z) ==>
     !x y. RTC R x y ==> P x y
RTC_RTC 
|- !R x y. RTC R x y ==> !z. RTC R y z ==> RTC R x z
RTC_TRANSITIVE 
|- !R. transitive (RTC R)
transitive_RTC 
|- !R. transitive (RTC R)
RTC_REFLEXIVE 
|- !R. reflexive (RTC R)
reflexive_RTC 
|- !R. reflexive (RTC R)
RC_REFLEXIVE 
|- !R. reflexive (RC R)
reflexive_RC 
|- !R. reflexive (RC R)
RC_lifts_monotonicities 
|- (!x y. R x y ==> R (f x) (f y)) ==> !x y. RC R x y ==> RC R (f x) (f y)
RC_lifts_invariants 
|- (!x y. P x /\ R x y ==> P y) ==> !x y. P x /\ RC R x y ==> P y
RC_lifts_equalities 
|- (!x y. R x y ==> (f x = f y)) ==> !x y. RC R x y ==> (f x = f y)
SC_lifts_monotonicities 
|- (!x y. R x y ==> R (f x) (f y)) ==> !x y. SC R x y ==> SC R (f x) (f y)
SC_lifts_equalities 
|- (!x y. R x y ==> (f x = f y)) ==> !x y. SC R x y ==> (f x = f y)
symmetric_RC 
|- !R. symmetric (RC R) = symmetric R
antisymmetric_RC 
|- !R. antisymmetric (RC R) = antisymmetric R
transitive_RC 
|- !R. transitive R ==> transitive (RC R)
TC_SUBSET 
|- !R x y. R x y ==> TC R x y
RTC_SUBSET 
|- !R x y. R x y ==> RTC R x y
RC_SUBSET 
|- !R x y. R x y ==> RC R x y
RC_RTC 
|- !R x y. RC R x y ==> RTC R x y
TC_INDUCT 
|- !R P.
     (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
     !u v. TC R u v ==> P u v
TC_INDUCT_LEFT1 
|- !R P.
     (!x y. R x y ==> P x y) /\ (!x y z. R x y /\ P y z ==> P x z) ==>
     !x y. TC R x y ==> P x y
TC_INDUCT_RIGHT1 
|- !R P.
     (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
     !x y. TC R x y ==> P x y
TC_STRONG_INDUCT 
|- !R P.
     (!x y. R x y ==> P x y) /\
     (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==>
     !u v. TC R u v ==> P u v
TC_STRONG_INDUCT_LEFT1 
|- !R P.
     (!x y. R x y ==> P x y) /\
     (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==>
     !u v. TC R u v ==> P u v
TC_STRONG_INDUCT_RIGHT1 
|- !R P.
     (!x y. R x y ==> P x y) /\
     (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==>
     !u v. TC R u v ==> P u v
TC_lifts_monotonicities 
|- (!x y. R x y ==> R (f x) (f y)) ==> !x y. TC R x y ==> TC R (f x) (f y)
TC_lifts_invariants 
|- (!x y. P x /\ R x y ==> P y) ==> !x y. P x /\ TC R x y ==> P y
TC_lifts_equalities 
|- (!x y. R x y ==> (f x = f y)) ==> !x y. TC R x y ==> (f x = f y)
TC_lifts_transitive_relations 
|- (!x y. R x y ==> Q (f x) (f y)) /\ transitive Q ==>
   !x y. TC R x y ==> Q (f x) (f y)
TC_RTC 
|- !R x y. TC R x y ==> RTC R x y
RTC_TC_RC 
|- !R x y. RTC R x y ==> RC R x y \/ TC R x y
TC_RC_EQNS 
|- !R. (RC (TC R) = RTC R) /\ (TC (RC R) = RTC R)
RTC_INDUCT_RIGHT1 
|- !R P.
     (!x. P x x) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
     !x y. RTC R x y ==> P x y
RTC_RULES_RIGHT1 
|- !R. (!x. RTC R x x) /\ !x y z. RTC R x y /\ R y z ==> RTC R x z
RTC_STRONG_INDUCT_RIGHT1 
|- !R P.
     (!x. P x x) /\ (!x y z. P x y /\ RTC R x y /\ R y z ==> P x z) ==>
     !x y. RTC R x y ==> P x y
EXTEND_RTC_TC 
|- !R x y z. R x y /\ RTC R y z ==> TC R x z
reflexive_RC_identity 
|- !R. reflexive R ==> (RC R = R)
symmetric_SC_identity 
|- !R. symmetric R ==> (SC R = R)
transitive_TC_identity 
|- !R. transitive R ==> (TC R = R)
RC_IDEM 
|- !R. RC (RC R) = RC R
SC_IDEM 
|- !R. SC (SC R) = SC R
TC_IDEM 
|- !R. TC (TC R) = TC R
RC_MOVES_OUT 
|- !R.
     (SC (RC R) = RC (SC R)) /\ (RC (RC R) = RC R) /\ (TC (RC R) = RC (TC R))
symmetric_TC 
|- !R. symmetric R ==> symmetric (TC R)
EQC_EQUIVALENCE 
|- !R. equivalence (EQC R)
EQC_IDEM 
|- !R. EQC (EQC R) = EQC R
RTC_IDEM 
|- !R. RTC (RTC R) = RTC R
RTC_CASES1 
|- !R x y. RTC R x y = (x = y) \/ ?u. R x u /\ RTC R u y
RTC_CASES2 
|- !R x y. RTC R x y = (x = y) \/ ?u. RTC R x u /\ R u y
RTC_CASES_RTC_TWICE 
|- !R x y. RTC R x y = ?u. RTC R x u /\ RTC R u y
TC_CASES1 
|- !R x z. TC R x z ==> R x z \/ ?y. R x y /\ TC R y z
TC_CASES2 
|- !R x z. TC R x z ==> R x z \/ ?y. TC R x y /\ R y z
TC_MONOTONE 
|- !R Q. (!x y. R x y ==> Q x y) ==> !x y. TC R x y ==> TC Q x y
RTC_MONOTONE 
|- !R Q. (!x y. R x y ==> Q x y) ==> !x y. RTC R x y ==> RTC Q x y
EQC_INDUCTION 
|- !R P.
     (!x y. R x y ==> P x y) /\ (!x. P x x) /\ (!x y. P x y ==> P y x) /\
     (!x y z. P x y /\ P y z ==> P x z) ==>
     !x y. EQC R x y ==> P x y
EQC_REFL 
|- !R x. EQC R x x
EQC_R 
|- !R x y. R x y ==> EQC R x y
EQC_SYM 
|- !R x y. EQC R x y ==> EQC R y x
EQC_TRANS 
|- !R x y z. EQC R x y /\ EQC R y z ==> EQC R x z
STRONG_EQC_INDUCTION 
|- !R P.
     (!x y. R x y ==> P x y) /\ (!x. P x x) /\
     (!x y. EQC R x y /\ P x y ==> P y x) /\
     (!x y z. P x y /\ P y z /\ EQC R x y /\ EQC R y z ==> P x z) ==>
     !x y. EQC R x y ==> P x y
ALT_equivalence 
|- !R. equivalence R = !x y. R x y = (R x = R y)
EQC_MONOTONE 
|- (!x y. R x y ==> R' x y) ==> !x y. EQC R x y ==> EQC R' x y
WF_INDUCTION_THM 
|- !R. WF R ==> !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x
INDUCTION_WF_THM 
|- !R. (!P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x) ==> WF R
WF_EQ_INDUCTION_THM 
|- !R. WF R = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x
WF_NOT_REFL 
|- !R x y. WF R ==> R x y ==> ~(x = y)
WF_EMPTY_REL 
|- WF REMPTY
WF_SUBSET 
|- !R P. WF R /\ (!x y. P x y ==> R x y) ==> WF P
WF_TC 
|- !R. WF R ==> WF (TC R)
WF_inv_image 
|- !R f. WF R ==> WF (inv_image R f)
RESTRICT_LEMMA 
|- !f R y z. R y z ==> (RESTRICT f R z y = f y)
WFREC_THM 
|- !R M. WF R ==> !x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x
WFREC_COROLLARY 
|- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (RESTRICT f R x) x
WF_RECURSION_THM 
|- !R. WF R ==> !M. ?!f. !x. f x = M (RESTRICT f R x) x
WFP_RULES 
|- !R x. (!y. R y x ==> WFP R y) ==> WFP R x
WFP_INDUCT 
|- !R P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. WFP R x ==> P x
WFP_CASES 
|- !R x. WFP R x = !y. R y x ==> WFP R y
WFP_STRONG_INDUCT 
|- !R. (!x. WFP R x /\ (!y. R y x ==> P y) ==> P x) ==> !x. WFP R x ==> P x
WF_EQ_WFP 
|- !R. WF R = !x. WFP R x
INDUCTIVE_INVARIANT_WFREC 
|- !R P M. WF R /\ INDUCTIVE_INVARIANT R P M ==> !x. P x (WFREC R M x)
TFL_INDUCTIVE_INVARIANT_WFREC 
|- !f R P M x.
     (f = WFREC R M) /\ WF R /\ INDUCTIVE_INVARIANT R P M ==> P x (f x)
INDUCTIVE_INVARIANT_ON_WFREC 
|- !R P M D x.
     WF R /\ INDUCTIVE_INVARIANT_ON R D P M /\ D x ==> P x (WFREC R M x)
TFL_INDUCTIVE_INVARIANT_ON_WFREC 
|- !f R D P M x.
     (f = WFREC R M) /\ WF R /\ INDUCTIVE_INVARIANT_ON R D P M /\ D x ==>
     P x (f x)
inv_inv 
|- !R. inv (inv R) = R
inv_RC 
|- !R. inv (RC R) = RC (inv R)
inv_SC 
|- !R. (inv (SC R) = SC R) /\ (SC (inv R) = SC R)
inv_TC 
|- !R. inv (TC R) = TC (inv R)
inv_EQC 
|- !R. (inv (EQC R) = EQC R) /\ (EQC (inv R) = EQC R)
inv_MOVES_OUT 
|- !R.
     (inv (inv R) = R) /\ (SC (inv R) = SC R) /\ (RC (inv R) = inv (RC R)) /\
     (TC (inv R) = inv (TC R)) /\ (RTC (inv R) = inv (RTC R)) /\
     (EQC (inv R) = EQC R)
reflexive_inv 
|- !R. reflexive (inv R) = reflexive R
irreflexive_inv 
|- !R. irreflexive (inv R) = irreflexive R
symmetric_inv 
|- !R. symmetric (inv R) = symmetric R
antisymmetric_inv 
|- !R. antisymmetric (inv R) = antisymmetric R
transitive_inv 
|- !R. transitive (inv R) = transitive R
symmetric_inv_identity 
|- !R. symmetric R ==> (inv R = R)
equivalence_inv_identity 
|- !R. equivalence R ==> (inv R = R)
INVOL 
|- !f. INVOL f = !x. f (f x) = x
INVOL_ONE_ONE 
|- !f. INVOL f ==> !a b. (f a = f b) = (a = b)
INVOL_ONE_ENO 
|- !f. INVOL f ==> !a b. (f a = b) = (a = f b)
NOT_INVOL 
|- INVOL $~
IDEM 
|- !f. IDEM f = !x. f (f x) = f x
inv_INVOL 
|- INVOL inv
inv_O 
|- !R R'. inv (R O R') = inv R' O inv R
RUNION_COMM 
|- R1 RUNION R2 = R2 RUNION R1
RUNION_ASSOC 
|- R1 RUNION (R2 RUNION R3) = R1 RUNION R2 RUNION R3
RINTER_COMM 
|- R1 RINTER R2 = R2 RINTER R1
RINTER_ASSOC 
|- R1 RINTER (R2 RINTER R3) = R1 RINTER R2 RINTER R3
reflexive_Id_RSUBSET 
|- !R. reflexive R = $= RSUBSET R
symmetric_inv_RSUBSET 
|- symmetric R = inv R RSUBSET R
transitive_O_RSUBSET 
|- transitive R = R O R RSUBSET R
StrongOrd_Ord 
|- !R. StrongOrder R ==> Order R
WeakOrd_Ord 
|- !R. WeakOrder R ==> Order R
WeakOrder_EQ 
|- !R. WeakOrder R ==> !y z. (y = z) = R y z /\ R z y
RSUBSET_ANTISYM 
|- !R1 R2. R1 RSUBSET R2 /\ R2 RSUBSET R1 ==> (R1 = R2)
RSUBSET_antisymmetric 
|- antisymmetric $RSUBSET
RSUBSET_WeakOrder 
|- WeakOrder $RSUBSET
EqIsBothRSUBSET 
|- !y z. (y = z) = y RSUBSET z /\ z RSUBSET y
STRORD_AND_NOT_Id 
|- STRORD R = R RINTER RCOMPL $=
RC_OR_Id 
|- RC R = R RUNION $=
RC_Weak 
|- Order R = WeakOrder (RC R)
STRORD_Strong 
|- !R. Order R = StrongOrder (STRORD R)
STRORD_RC 
|- !R. StrongOrder R ==> (STRORD (RC R) = R)
RC_STRORD 
|- !R. WeakOrder R ==> (RC (STRORD R) = R)
IDEM_STRORD 
|- IDEM STRORD
IDEM_RC 
|- IDEM RC
IDEM_SC 
|- IDEM SC
IDEM_TC 
|- IDEM TC
IDEM_RTC 
|- IDEM RTC
WeakLinearOrder_dichotomy 
|- !R. WeakLinearOrder R = WeakOrder R /\ !a b. R a b \/ R b a
O_ASSOC 
|- R1 O R2 O R3 = (R1 O R2) O R3
Id_O 
|- $= O R = R
O_Id 
|- R O $= = R
O_MONO 
|- R1 RSUBSET R2 /\ S1 RSUBSET S2 ==> R1 O S1 RSUBSET R2 O S2
inv_Id 
|- inv $= = $=
inv_diag 
|- inv (diag A) = diag A
IN_RDOM 
|- x IN RDOM R = ?y. R x y
IN_RRANGE 
|- y IN RRANGE R = ?x. R x y
RUNIV_SUBSET 
|- (RUNIV RSUBSET R = (R = RUNIV)) /\ R RSUBSET RUNIV
REMPTY_SUBSET 
|- REMPTY RSUBSET R /\ (R RSUBSET REMPTY = (R = REMPTY))
rcdiamond_diamond 
|- !R. rcdiamond R = diamond (RC R)
diamond_RC_diamond 
|- !R. diamond R ==> diamond (RC R)
diamond_TC_diamond 
|- !R. diamond R ==> diamond (TC R)
establish_CR 
|- !R. (rcdiamond R ==> CR R) /\ (diamond R ==> CR R)
Newmans_lemma 
|- !R. WCR R /\ SN R ==> CR R