Theory "tc"

Signature

Definitions

BRESTR

⊢ ∀R s. R ^|^ s = R ^| s |^ s

DRESTR

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

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)

RRESTR

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

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)

TC_MOD

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

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

Theorems

DRESTR_EMPTY

⊢ ∀R. R ^| ∅ = ∅ᵣ

DRESTR_IN

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

DRESTR_RDOM

⊢ ∀R. R ^| RDOM R = R

FDOM_RDOM

⊢ ∀R. FINITE (RDOM R) ⇒ (FDOM (RELN_TO_FMAP R) = RDOM R)

FINITE_RDOM

⊢ ∀f. FINITE (RDOM (FMAP_TO_RELN f))

I_o_f

⊢ ∀f. I o_f f = f

NOT_IN_RDOM

⊢ ∀Q x. (Q x = ∅) ⇔ x ∉ RDOM Q

O_REMPTY_O

⊢ (∀R. R ∘ᵣ ∅ᵣ = ∅ᵣ) ∧ ∀R. ∅ᵣ ∘ᵣ R = ∅ᵣ

RDOM_SUBSET_FDOM

⊢ ∀f. RDOM (FMAP_TO_RELN f) ⊆ FDOM f

RDOM_subTC

⊢ ∀R s. RDOM (subTC R s) = RDOM R

RELN_TO_FMAP_TO_RELN_ID

⊢ ∀R. FINITE (RDOM R) ⇒ (FMAP_TO_RELN (RELN_TO_FMAP R) = R)

REMPTY_RRESTR

⊢ ∀s. ∅ᵣ |^ s = ∅ᵣ

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)

SUBSET_FDOM_LEM

⊢ ∀R s f. (subTC R s = FMAP_TO_RELN f) ⇒ RDOM R ⊆ FDOM 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))

TC_MOD_EMPTY_ID

⊢ ∀x ra. TC_MOD x ∅ = I

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

subTC_EMPTY

⊢ ∀R. subTC R ∅ = R

subTC_FDOM

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

subTC_FDOM_RDOM

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

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

subTC_MAX_RDOM

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

subTC_RDOM

⊢ ∀R. subTC R (RDOM R) = R⁺

subTC_SUPERSET_RDOM

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

subTC_thm

⊢ ∀R s. subTC R s = R ∪ᵣ R ∘ᵣ ((R ^|^ s)꙳ ^| s) ∘ᵣ R