Theory "tc"

Signature

Definitions

DRESTR

|- ∀R s a b. (R ^| s) a b ⇔ a ∈ s ∧ R a b

RRESTR

|- ∀R s a b. (R |^ s) a b ⇔ b ∈ s ∧ R a b

BRESTR

|- ∀R s. R ^|^ s = R ^| s |^ s

subTC

|- ∀R s x y.
     subTC R s x y ⇔
     R x y ∨ ∃a b. (R ^|^ s)^* a b ∧ a ∈ s ∧ b ∈ s ∧ R x a ∧ R b y

FMAP_TO_RELN

|- ∀f x. FMAP_TO_RELN f x = if x ∈ FDOM f then f ' x else ∅

RELN_TO_FMAP

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

TC_MOD

|- ∀x rx ra. TC_MOD x rx ra = if x ∈ ra then ra ∪ rx else ra

TC_ITER

|- (∀r. TC_ITER [] r = r) ∧
   ∀x d r. TC_ITER (x::d) r = TC_ITER d (TC_MOD x (r ' x) o_f r)

Theorems

DRESTR_IN

|- ∀R s a. (R ^| s) a = if a ∈ s then R a else ∅

DRESTR_EMPTY

|- ∀R. R ^| ∅ = REMPTY

DRESTR_RDOM

|- ∀R. R ^| RDOM R = R

REMPTY_RRESTR

|- ∀s. REMPTY |^ s = REMPTY

O_REMPTY_O

|- (∀R. R O REMPTY = REMPTY) ∧ ∀R. REMPTY O R = REMPTY

subTC_thm

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

subTC_EMPTY

|- ∀R. subTC R ∅ = R

RTC_INSERT

|- ∀R s a w z.
     (R ^|^ (a INSERT s))^* w z ⇔
     (R ^|^ s)^* w z ∨
     ((a = w) ∨ ∃x. x ∈ s ∧ (R ^|^ s)^* w x ∧ R x a) ∧
     ((a = z) ∨ ∃y. y ∈ s ∧ R a y ∧ (R ^|^ s)^* y z)

subTC_INSERT

|- ∀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

subTC_RDOM

|- ∀R. subTC R (RDOM R) = R⁺

subTC_INSERT_COR

|- ∀R s x a.
     subTC R (x INSERT s) a =
     if x ∈ subTC R s a then subTC R s a ∪ subTC R s x else subTC R s a

RDOM_SUBSET_FDOM

|- ∀f. RDOM (FMAP_TO_RELN f) ⊆ FDOM f

FINITE_RDOM

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

FDOM_RDOM

|- ∀R. FINITE (RDOM R) ⇒ (FDOM (RELN_TO_FMAP R) = RDOM R)

RELN_TO_FMAP_TO_RELN_ID

|- ∀R. FINITE (RDOM R) ⇒ (FMAP_TO_RELN (RELN_TO_FMAP R) = R)

RDOM_subTC

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

NOT_IN_RDOM

|- ∀Q x. (Q x = ∅) ⇔ x ∉ RDOM Q

TC_MOD_EMPTY_ID

|- ∀x ra. TC_MOD x ∅ = I

I_o_f

|- ∀f. I o_f f = f

subTC_MAX_RDOM

|- ∀R s x. x ∉ RDOM R ⇒ (subTC R (x INSERT s) = subTC R s)

subTC_SUPERSET_RDOM

|- ∀R s. FINITE s ⇒ (subTC R (RDOM R ∪ s) = subTC R (RDOM R))

subTC_FDOM

|- ∀g R.
     (subTC R (RDOM R) = FMAP_TO_RELN g) ⇒
     (subTC R (FDOM g) = subTC R (RDOM R))

SUBSET_FDOM_LEM

|- ∀R s f. (subTC R s = FMAP_TO_RELN f) ⇒ RDOM R ⊆ FDOM f

subTC_FDOM_RDOM

|- ∀R f.
     (subTC R (FDOM f) = FMAP_TO_RELN f) ⇒ (subTC R (RDOM R) = FMAP_TO_RELN f)

TC_MOD_LEM

|- ∀R s x f.
     x ∈ FDOM f ∧ (subTC R s = FMAP_TO_RELN f) ⇒
     (subTC R (x INSERT s) = FMAP_TO_RELN (TC_MOD x (f ' x) o_f f))

TC_ITER_THM

|- ∀R d f s.
     (s ∪ LIST_TO_SET d = FDOM f) ∧ (subTC R s = FMAP_TO_RELN f) ⇒
     (R⁺ = FMAP_TO_RELN (TC_ITER d f))