Как доказать, что свойство отношения имеет место для транзитивного замыкания этого отношения?

Question

Я определил следующее свойство отношения:

definition rel_limited_under :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
  "rel_limited_under R A = 
   (∀x y z :: 'a. R x y ⟶ R y z ⟶ x ∈ A ⟶ z ∈ A ⟶ y ∈ A)"

Отношение R ограничено набором A, если любые два элемента x и z из этого набора могут быть связаны толькочерез элемент y, принадлежащий этому набору.Другими словами, элементы из набора A не могут быть связаны через элемент, не принадлежащий этому набору.

Знаете ли вы общее имя этого свойства?Я думаю, что это что-то из теории графов.

Не могли бы вы предложить, как доказать, что свойство имеет место для транзитивного замыкания отношения?

lemma rel_tcl_limited_under:
  fixes R :: "'a ⇒ 'a ⇒ bool"
    and A :: "'a set"
  assumes as_R: "rel_limited_under R A"
  shows "rel_limited_under R⇧+⇧+ A"

Answer 1

Я могу вам сказать, что вы не можете доказать собственность rel_tcl_limited_under в Изабель, так как она просто не имеет места.В качестве контрпримеров рассмотрим A = {0} и R = {(0,1), (1,2), (2,0)}.Тогда rel_limited_under R A удовлетворяется тривиально, поскольку не существует x, y, z такого, что R x y /\ R y z /\ x ∈ A /\ z ∈ A.Но rel_limited_under (R^+) A не держится: выберите x = 0, y = 1, z = 0.