Theory "tc"

Signature

Definitions

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)

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

RRESTR

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

RELN_TO_FMAP

⊢ ∀R. RELN_TO_FMAP R = FUN_FMAP R (RDOM R)

FMAP_TO_RELN

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

DRESTR

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

BRESTR

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

Theorems

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_MOD_EMPTY_ID

⊢ ∀x ra. TC_MOD x ∅ = I

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

subTC_thm

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

subTC_SUPERSET_RDOM

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

subTC_RDOM

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

subTC_MAX_RDOM

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

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

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

subTC_FDOM

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

subTC_EMPTY

⊢ ∀R. subTC R ∅ = R

SUBSET_FDOM_LEM

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

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)

REMPTY_RRESTR

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

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

RDOM_SUBSET_FDOM

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

O_REMPTY_O

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

NOT_IN_RDOM

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

I_o_f

⊢ ∀f. I o_f f = f

FINITE_RDOM

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

FDOM_RDOM

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

DRESTR_RDOM

⊢ ∀R. R ^| RDOM R = R

DRESTR_IN

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

DRESTR_EMPTY

⊢ ∀R. R ^| ∅ = ∅ᵣ