Доработка математического представления Модели отношений

[netkeep80]

Доработать файлы:
https://github.com/netkeep80/jsonRVM/blob/master/doc/relations-model-ru.md
https://github.com/netkeep80/jsonRVM/blob/master/doc/relations-model-en.md
https://github.com/netkeep80/jsonRVM/blob/master/proofs/rocq/RelationsModel.v

А именно, у меня такие размышления:
Определение 1.3 (Дуплет). Дуплет (упорядоченная пара ссылок) — это элемент множества:
D = L² = L × L = {(b, e) : b ∈ L, e ∈ L}
,где b - begin начало, e - end конец.

Определение 1.4 (Триплет). Триплет (кортеж длины 3) — это элемент множества:
T = L³ = L × L × L = {(r, s, o) : r ∈ L, s ∈ L, o ∈ L}
или
T = L × D, D = L × L

Представление триплета через вложенные упорядоченные пары: (s, r, o) = ((s, r), o)
заменить на (r, s, o) = (r, (s, o)) = (e, d)

Внутренняя структура связей
Внутренний аспект (структура) каждого типа сущности определяется через связи:
E = ER (сущность определяется парой сущность-отношение)
R = SO (отношение определяется парой объект-субъект)
S ⊆ E
O ⊆ E

Типы связей (дуплетов)
Определим два базовых типа связей:

SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E}
ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E}

Теорема об эквивалентности представлений
Теорема 3.1. Множество RM может быть эквивалентно представлено двумя подмножествами дуплетов:

RM = {ER, SO}
где:
E = ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E}
R = SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E}

Модель Отношений как четыре взаимосвязанных множества, заменить на функцию:
rm : E -> ExExE

---

Обдумай это математически... и перепиши:
relations-model-ru.md
relations-model-en.md
RelationsModel.v