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 ^| ∅ = ∅ᵣ

DRESTR_RDOM

⊢ ∀R. R ^| RDOM R = R

REMPTY_RRESTR

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

O_REMPTY_O

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

subTC_thm

⊢ ∀R s. subTC R s = R ∪ᵣ R ∘ᵣ ((R ^|^ s)^* ^| s) ∘ᵣ 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)