Theory tc

|- !R s. R ^|^ s = R ^| s |^ s

|- !R s a b. (R ^| s) a b <=> a IN s /\ R a b

|- !f x. FMAP_TO_RELN f x = if x IN FDOM f then FAPPLY f x else {}

|- !R. RELN_TO_FMAP R = FUN_FMAP R (RDOM R)

|- !R s a b. (R |^ s) a b <=> b IN s /\ R a b

|- (!r. TC_ITER [] r = r) /\
   !x d r. TC_ITER (x::d) r = TC_ITER d (TC_MOD x (FAPPLY r x) o_f r)

|- !x rx ra. TC_MOD x rx ra = if x IN ra then ra UNION rx else ra

|- !R s x y.
     subTC R s x y <=>
     R x y \/ ?a b. (R ^|^ s)^* a b /\ a IN s /\ b IN s /\ R x a /\ R b y

|- !R. R ^| {} = REMPTY

|- !R s a. (R ^| s) a = if a IN s then R a else {}

|- !R. R ^| RDOM R = R

|- !R. FINITE (RDOM R) ==> (FDOM (RELN_TO_FMAP R) = RDOM R)

|- !f. FINITE (RDOM (FMAP_TO_RELN f))

|- !f. I o_f f = f

|- !Q x. (Q x = {}) <=> x NOTIN RDOM Q

|- (!R. R O REMPTY = REMPTY) /\ !R. REMPTY O R = REMPTY

|- !f. RDOM (FMAP_TO_RELN f) SUBSET FDOM f

|- !R s. RDOM (subTC R s) = RDOM R

|- !R. FINITE (RDOM R) ==> (FMAP_TO_RELN (RELN_TO_FMAP R) = R)

|- !s. REMPTY |^ s = REMPTY

|- !R s a w z.
     (R ^|^ (a INSERT s))^* w z <=>
     (R ^|^ s)^* w z \/
     ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a) /\
     ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)

|- !R s f. (subTC R s = FMAP_TO_RELN f) ==> RDOM R SUBSET FDOM f

|- !R d f s.
     (s UNION set d = FDOM f) /\ (subTC R s = FMAP_TO_RELN f) ==>
     (R^+ = FMAP_TO_RELN (TC_ITER d f))

|- !x ra. TC_MOD x {} = I

|- !R s x f.
     x IN FDOM f /\ (subTC R s = FMAP_TO_RELN f) ==>
     (subTC R (x INSERT s) = FMAP_TO_RELN (TC_MOD x (FAPPLY f x) o_f f))

|- !R. subTC R {} = R

|- !g R.
     (subTC R (RDOM R) = FMAP_TO_RELN g) ==>
     (subTC R (FDOM g) = subTC R (RDOM R))

|- !R f.
     (subTC R (FDOM f) = FMAP_TO_RELN f) ==>
     (subTC R (RDOM R) = FMAP_TO_RELN f)

|- !R s q x y.
     subTC R (q INSERT s) x y <=>
     subTC R s x y \/ subTC R s x q /\ subTC R s q y

|- !R s x a.
     subTC R (x INSERT s) a =
     if x IN subTC R s a then subTC R s a UNION subTC R s x
     else subTC R s a

|- !R s x. x NOTIN RDOM R ==> (subTC R (x INSERT s) = subTC R s)

|- !R. subTC R (RDOM R) = R^+

|- !R s. FINITE s ==> (subTC R (RDOM R UNION s) = subTC R (RDOM R))

|- !R s. subTC R s = R RUNION R O ((R ^|^ s)^* ^| s) O R