ocaml re-migration

25 files changed, 84 insertions, 2876 deletions

diff --git a/docs/architecture.plantuml b/docs/architecture.plantuml
new file mode 100644
index 0000000..90985ba
--- /dev/null
+++ b/docs/architecture.plantuml
@@ -0,0 +1,72 @@
+@startuml
+allowmixing
+
+package Client {
+    object "Query Interface" as query_interface
+}
+
+package Algebra {
+    object "Unifier" as unifier
+    object "Bytecode Builder" as bytecode_builder
+    object "Parser" as parser
+    object "Lexer" as lexer
+}
+
+query_interface --> lexer
+lexer --> parser
+parser --> unifier
+unifier --> bytecode_builder
+
+package Query {
+    object "Schema Builder" as schema_builder
+    object "Facts Builder" as facts_builder
+    object "Optimizer" as optimizer
+    object "Commands Generator" as commands_generator
+    object "B+ Tree" as b_plus_tree
+}
+
+bytecode_builder --> optimizer
+optimizer --> commands_generator
+facts_builder --> commands_generator
+schema_builder --> commands_generator
+commands_generator --> b_plus_tree
+b_plus_tree --> query_interface
+
+package Coordinator {
+    object "File Historical Hashes" as file_historical_hashes
+    object "Location Hashes" as location_hashes
+    object "Command Parser" as command_parser
+    object "Curator" as curator
+}
+
+commands_generator <-- command_parser
+
+package Disk {
+    object "Merkle Tree Root Generator" as merkle_tree
+    object "WAL Reader" as wal_reader
+    object "WAL Writer" as wal_writer
+    object "ARIES" as aries
+    object "SHA256 Hasher" as sha
+    object "Executor" as executor
+    map storage {
+        write => +λ
+        read => +λ
+    }
+    object "Courier" as courier
+    database Wal
+}
+
+executor *--> merkle_tree
+executor *--> sha
+curator --> command_parser
+command_parser --> executor
+location_hashes *--> curator
+file_historical_hashes *--> curator
+executor --> aries
+aries --> wal_reader
+aries --> wal_writer
+wal_writer --> Wal
+wal_reader --> Wal
+courier <-- wal_reader
+courier --> storage
+@enduml
\ No newline at end of file
diff --git a/docs/code.org b/docs/code.org
deleted file mode 100644
index 30ff9c9..0000000
--- a/docs/code.org
+++ /dev/null
@@ -1,272 +0,0 @@
-#+TITLE: Code Documentation
-
-* Overview
-
-Domino is a content-addressed, immutable relational database engine written in Erlang. The system uses cryptographic hashing (SHA-256) and Merkle trees to provide version control, deduplication, and efficient synchronization capabilities.
-
-* Architecture
-
-** Design Patterns
-
-- *Content-Addressed Storage* :: All data (attributes, tuples, relations, databases) are identified by their cryptographic hash
-- *Immutable Data Structures* :: All operations create new versions rather than modifying existing data
-- *Merkle Trees* :: Relations and databases use merkle trees for efficient diffing and synchronization
-- *Volcano Iterator Model* :: Query execution uses lazy evaluation with process-based iterators
-- *Actor Model* :: Iterators are implemented as independent Erlang processes
-- *Transactional Storage* :: Mnesia provides ACID guarantees for all mutations
-
-* Module Structure
-
-** operations.erl
-
-The core database operations module and main API.
-
-*** Public API
-
-**** Database & Relation Management
-- =setup/0= :: Initialize Mnesia schema and create all tables
-- =create_database/1= :: Create a new database state
-- =create_relation/3= :: Add a relation to a database with schema
-- =get_relations/1= :: List all relation names in a database
-- =get_relation_hash/2= :: Get relation hash by name
-
-**** Tuple Operations
-- =create_tuple/3= :: Insert a tuple into a relation (transactional)
-- =retract_tuple/3= :: Remove a tuple from a relation (default: transactional)
-- =retract_tuple/4= :: Remove a tuple with optional transaction control
-
-**** Relation Operations
-- =clear_relation/2= :: Remove all tuples from a relation (default: transactional)
-- =clear_relation/3= :: Clear relation with optional transaction control
-- =retract_relation/2= :: Remove a relation from database (default: transactional)
-- =retract_relation/3= :: Remove relation with optional transaction control
-
-**** Iterator Pattern (Volcano Model)
-- =get_tuples_iterator/2= :: Create lazy iterator process for relation tuples
-- =next_tuple/1= :: Pull next tuple from iterator (returns ={ok, Tuple} | done=)
-- =close_iterator/1= :: Terminate iterator process
-- =collect_all/1= :: Helper to consume entire iterator into list
-
-**** Utility Functions
-- =hash/1= :: SHA-256 hash of term
-- =hashes_from_tuple/1= :: Extract all tuple hashes from a relation
-
-** relation.erl
-
-Simple helper module for building tuples and relations conceptually.
-
-*** Public API
-- =new_attribute/2= :: Create attribute map: =#{name => Name, value => Value}=
-- =new_tuple/1= :: Convert list of attributes to map
-- =new_relation/1= :: Convert list of tuples to sets:set
-
-** poc.erl
-
-Proof-of-concept demonstrating the Volcano Iterator Model for query execution.
-
-*** Key Concepts
-- Content-addressed storage simulation using in-memory maps
-- Lazy iterator chain: Scan → Select → Project
-- Message-passing protocol for tuple streaming
-- Automatic deduplication via hashing
-
-** main.erl
-
-OTP application entry point. Starts Mnesia on application startup.
-
-* Data Structures
-
-All core records are defined in =include/operations.hrl=.
-
-** attribute
-#+BEGIN_SRC erlang
--record(attribute, {
-    hash,    % SHA-256 hash of value
-    value    % Actual value (any Erlang term)
-}).
-#+END_SRC
-
-** tuple
-#+BEGIN_SRC erlang
--record(tuple, {
-    hash,           % SHA-256 hash of entire tuple
-    relation,       % Relation name (atom)
-    attribute_map   % #{attr_name => value_hash}
-}).
-#+END_SRC
-
-** relation
-#+BEGIN_SRC erlang
--record(relation, {
-    hash,    % hash({name, schema, tree_root})
-    name,    % Relation name (atom)
-    tree,    % Merkle tree of tuple hashes
-    schema   % Schema definition map
-}).
-#+END_SRC
-
-** database_state
-#+BEGIN_SRC erlang
--record(database_state, {
-    hash,       % Merkle tree root hash
-    name,       % Database name (atom)
-    tree,       % Merkle tree of relations
-    relations,  % #{relation_name => relation_hash}
-    timestamp   % Creation/modification timestamp
-}).
-#+END_SRC
-
-* Data Flow
-
-** Creating a Tuple
-
-1. Store each attribute value separately (enables deduplication)
-2. Build attribute_map with hashes: =#{name => AttrHash1, age => AttrHash2}=
-3. Create tuple record with hash
-4. Insert tuple hash into relation's merkle tree
-5. Compute new relation hash from tree root
-6. Update database merkle tree
-7. Return updated database and relation
-
-All operations occur within a Mnesia transaction.
-
-** Querying Tuples
-
-1. Lookup relation hash from database
-2. Read relation from Mnesia
-3. Extract tuple hashes from merkle tree
-4. Spawn iterator process with hash list
-5. Client pulls tuples via message passing
-6. Iterator resolves: hash → tuple → attribute hashes → actual values
-7. Return materialized tuple map
-
-* Usage Examples
-
-** Basic Workflow
-
-#+BEGIN_SRC erlang
-%% Setup
-operations:setup().
-
-%% Create database
-DB = operations:create_database(my_app).
-
-%% Create relation with schema
-{DB1, _Rel} = operations:create_relation(DB, users, #{
-    name => string,
-    age => integer
-}).
-
-%% Insert tuples
-{DB2, _} = operations:create_tuple(DB1, users, #{name => "Alice", age => 30}).
-{DB3, _} = operations:create_tuple(DB2, users, #{name => "Bob", age => 25}).
-
-%% Query tuples
-Iterator = operations:get_tuples_iterator(DB3, users).
-Tuples = operations:collect_all(Iterator).
-%% Returns: [#{name => "Alice", age => 30}, #{name => "Bob", age => 25}]
-
-%% Remove tuple
-{ok, RelHash} = operations:get_relation_hash(DB3, users).
-[TupleHash|_] = operations:hashes_from_tuple(RelHash).
-{atomic, {DB4, _}} = operations:retract_tuple(DB3, RelHash, TupleHash).
-
-%% Clear relation (remove all tuples, keep schema)
-{atomic, {DB5, _}} = operations:clear_relation(DB4, RelHash).
-
-%% Remove relation entirely
-{atomic, DB6} = operations:retract_relation(DB5, users).
-#+END_SRC
-
-** Iterator Protocol
-
-#+BEGIN_SRC erlang
-Iterator = operations:get_tuples_iterator(DB, users).
-
-%% Pull tuples one by one
-case operations:next_tuple(Iterator) of
-    {ok, Tuple} -> process_tuple(Tuple);
-    done -> io:format("No more tuples~n")
-end.
-
-%% Or collect all at once
-AllTuples = operations:collect_all(Iterator).
-
-%% Clean up
-operations:close_iterator(Iterator).
-#+END_SRC
-
-* Key Implementation Details
-
-** Immutability & Versioning
-
-Every modification creates a new hash. Old versions remain accessible via their hash. Database evolution is tracked via timestamp and hash chain.
-
-** Deduplication
-
-Identical attribute values are stored once (content-addressed). Example: 1000 users with age=30 store the value "30" only once.
-
-** Transaction Semantics
-
-All mutations are wrapped in =mnesia:transaction/1=. Dirty reads are used for immutable data lookups.
-
-** Merkle Tree Strategy
-
-- Relations store tuple hashes as keys: ={TupleHash, <<>>}=
-- Databases store relation names → hashes: ={RelationName, RelationHash}=
-- Enables efficient diff computation between versions
-- Foundation for distributed synchronization
-
-** Iterator Pattern
-
-- Decouples query execution from data access
-- Enables pipelined query operators (future: select, project, join)
-- Memory bounded (doesn't materialize entire relation)
-- Process-based concurrency via Erlang actors
-
-** Schema Flexibility
-
-Schema stored as map (e.g., =#{name => string, age => integer}=). Currently not enforced, but provides foundation for future domain validation.
-
-* Dependencies
-
-- =merklet= (2.0.0) :: Merkle tree implementation for set reconciliation
-- =mnesia= :: Distributed database for persistent storage
-- =crypto= :: SHA-256 hashing
-
-* Testing
-
-The test suite (=test/operations_test.erl=) validates:
-
-- Functional correctness (CRUD operations)
-- Hash determinism and consistency
-- Transactional integrity
-- Iterator protocol compliance
-- State evolution tracking
-- Cross-database consistency
-
-Run tests with:
-
-#+BEGIN_SRC sh
-rebar3 eunit
-#+END_SRC
-
-* Current State
-
-** Implemented
-- Core data model (attribute, tuple, relation, database)
-- Content-addressed storage with SHA-256
-- Immutable versioning
-- Merkle tree integration
-- Iterator-based lazy evaluation
-- Transactional CRUD operations
-- Comprehensive test suite
-
-** Not Yet Implemented
-- Relational algebra operators (σ, π, ⋈, ∪, ∩, −)
-- Schema validation and type checking
-- Infinite relations (aleph₀)
-- Join indexing
-- Query optimization
-- Distributed synchronization
-- REPL/query console
diff --git a/docs/command-interface.puml b/docs/command-interface.puml
deleted file mode 100644
index 4c0319a..0000000
--- a/docs/command-interface.puml
+++ /dev/null
@@ -1,58 +0,0 @@
-@startuml command-interface
-!theme plain
-title Command-Based Interface Flow
-
-participant "Karuta" as K
-participant "domino:execute/2" as API
-participant "Command Validator" as V
-participant "operations.erl" as Ops
-database "Mnesia" as DB
-
-K -> API: execute(DB0, {create, relation, employee, Schema})
-activate API
-API -> V: validate({create, relation, ...})
-activate V
-V -> V: check schema format
-V -> V: verify types
-V --> API: ok
-deactivate V
-
-API -> Ops: create_relation(DB0, employee, Schema)
-activate Ops
-Ops -> DB: transaction(fn -> ... end)
-activate DB
-DB -> DB: insert relation record
-DB -> DB: update database tree
-DB --> Ops: {atomic, {NewDB, Hash}}
-deactivate DB
-Ops --> API: {NewDB, Hash}
-deactivate Ops
-
-API --> K: {ok, DB1, {relation_created, employee, Hash}}
-deactivate API
-
-K -> API: execute(DB1, {insert, tuple, employee, Data})
-activate API
-API -> V: validate({insert, tuple, ...})
-activate V
-V -> V: check schema compliance
-V -> V: verify constraints
-V --> API: ok
-deactivate V
-
-API -> Ops: create_tuple(DB1, employee, Data)
-activate Ops
-Ops -> DB: transaction(fn -> ... end)
-activate DB
-DB -> DB: store attribute values
-DB -> DB: create tuple record
-DB -> DB: update merkle tree
-DB --> Ops: {atomic, {NewDB2, TupleHash}}
-deactivate DB
-Ops --> API: {NewDB2, TupleHash}
-deactivate Ops
-
-API --> K: {ok, DB2, {tuple_inserted, TupleHash}}
-deactivate API
-
-@enduml
diff --git a/docs/constraint-classification.puml b/docs/constraint-classification.puml
deleted file mode 100644
index 09094f1..0000000
--- a/docs/constraint-classification.puml
+++ /dev/null
@@ -1,82 +0,0 @@
-@startuml constraint-classification
-!theme plain
-title Constraint Classification (McGoveran Framework)
-
-package "Database Constraints" {
-  class RelationConstraints {
-    Which relations must/can exist
-    Example: referential integrity
-  }
-
-  class CardinalityConstraints {
-    Relation size limits
-    Examples:
-    - exactly N tuples
-    - at most M tuples
-  }
-}
-
-package "Relation Constraints" {
-  package "Tuple Constraints" {
-    class AttributeConstraints {
-      Domain constraints per attribute
-      Examples:
-      - age >= 18
-      - salary > 0
-      - name ≠ ""
-    }
-
-    class TupleLevelConstraints {
-      Cross-attribute rules
-      Example:
-      if salary > 200k then age >= 30
-    }
-  }
-
-  package "Relation-Level Constraints" {
-    class KeyConstraints {
-      Uniqueness + not null
-      - Primary keys
-      - Candidate keys
-      - Composite keys
-    }
-
-    class FunctionalDependencies {
-      A → B
-      Example: ZIP → {city, state}
-    }
-
-    class ForeignKeys {
-      Inclusion dependencies
-      Example: employee.dept_id ⊆ department.id
-    }
-  }
-}
-
-package "Transition Constraints" {
-  class StateTransitionRules {
-    Before → After constraints
-    Examples:
-    - salary (monotonic increasing)
-    - created_at (immutable)
-  }
-
-  class TemporalConstraints {
-    Time-based rules
-    Example: end_date >= start_date
-  }
-}
-
-package "Multi-Relation Constraints" {
-  class AggregateConstraints {
-    Cross-relation aggregates
-    Example: sum(dept_salaries) <= dept_budget
-  }
-
-  class MutualExclusion {
-    Disjoint sets
-    Example: managers ∩ ICs = ∅
-  }
-}
-
-@enduml
diff --git a/docs/constraint-enforcement-strategies.puml b/docs/constraint-enforcement-strategies.puml
deleted file mode 100644
index 6e0305d..0000000
--- a/docs/constraint-enforcement-strategies.puml
+++ /dev/null
@@ -1,42 +0,0 @@
-@startuml constraint-enforcement-strategies
-!theme plain
-title Constraint Enforcement Strategies
-
-state "Operation Request" as Request
-state "Immediate Validation" as Immediate
-state "Deferred Validation" as Deferred
-state "Execute Operation" as Execute
-state "Transaction Commit" as Commit
-state "Rollback" as Rollback
-state "Success" as Success
-
-Request --> Immediate: Strategy 1:\nEager
-Request --> Execute: Strategy 2:\nDeferred
-
-Immediate --> Execute: Valid
-Immediate --> Rollback: Invalid
-
-Execute --> Deferred: At commit
-Deferred --> Commit: Valid
-Deferred --> Rollback: Invalid
-
-Commit --> Success
-Rollback --> Request: Retry
-
-note right of Immediate
-  Immediate Checking:
-  - Validate before execute
-  - Simple reasoning
-  - May reject valid intermediate states
-  - Lower performance
-end note
-
-note right of Deferred
-  Deferred Checking:
-  - Validate at transaction end
-  - Allows intermediate invalid states
-  - Better performance
-  - Complex error handling
-end note
-
-@enduml
diff --git a/docs/constraints.org b/docs/constraints.org
deleted file mode 100644
index b3978e6..0000000
--- a/docs/constraints.org
+++ /dev/null
@@ -1,97 +0,0 @@
-#+TITLE: Constraints
-
-* Preamble
-Under an ontological commitment to objects, with an objects-properties
-modeling in a conceptual model, there are primitive and compound objects:
-
-** Primitive objects
-These are things we directly observe their existence independent of their individual properties
-
-** Compound objects
-These are collective properties observed through their relationships in groups or multigroups
-
-* Entity Properties
-These are the properties derived by observation or measurement
-procedures. They can be further divided in:
-- Quantitative :: which include ordinal and cardinal properties; for
-  example, customer rating and price of a product.
-- Qualitative :: observed only, for example an enum
-
-* 1st Order Properties
-They are inferred properties not directly observable in entities. They
-are abstractions generalized from multiple observed or measured
-properties that share:
-- The same kind of values;
-- The same allowable manipulations, and;
-- Meaningful comparability.
-
-They arise when several concrete properties, for example salary,
-commission and department budget, meet the above criteria. They are
-understood as deriving from a more general underlying property, in the
-example aforementioned, compensation, budget or whatever. That
-underlying abstraction is the 1OP.
-
-** 1st Order Properties in Context
-These are directly observed or measured properties of entities that
-appear in a specific group in context. In other words, they are
-concrete properties associated with entities of a particular type
-whithin a context of a specific group or multigroup. The context is
-essential because the underlying 1OP may manifest as different 1OPiCs
-depending on the entity type (employee VS department) or group
-membership (sales employees VS marketing employees).
-
-They are related to 1OPs insofar as they are contextual instantiations
-of a 1OP, therefore, all 1OPiCs of the same kind share comparable
-value sets and allow operations because they derive from the same
-root. To illustrate with one example: salary and commission are 1OPiC
-of the 1OP Compensation in the context of employees.
-
-* Constraint Algebra
-The costrait module attempts to implement constraints as relations, in
-other words, it follows the principle that Entity/1OPs/1OPiCs should
-be a relation or domain.
-
-** Core Distinction: Domains vs Relations
-- Domain (#domain{}): A VALUE SET with membership criteria (e.g., integers, rationals)
-- Relation (#relation{}): A SET OF TUPLES
-`less_than` is NOT a domain. It is a binary relation (subset of D × D).
-
-** 1st Order Properties (1OPs)
-A 1OP is a direct property (attribute) of individual entities. 1OPs can be:
-- Observed/measured: directly observed from entities (e.g., `salary`, `commission`)
-- Derived/inferred: computed from other 1OPs (e.g., `compensation` = salary + commission)
-
-** Types
-Domain constraints: ARE the domains themselves (membership criteria)
-- `integer` domain: membership test is_integer/1
-- `rational` domain: numerator, denominator (integers), denominator ≠ 0
-Attribute constraints (1OP constraints): Restrict attribute values
-- Specify which domain the attribute draws from
-- Add constraints beyond domain membership
-- Example: `salary` draws from `rational` + [gt(0), lt(1000000)]
-
-** 1st Order Properties in Context (1OPiCs)
-A 1OPiC is a 1OP that is DERIVED from other observed/measured 1OPs within
-the context of a specific relation.
-Examples in `employees` relation:
-- `salary`: observed/measured 1OP (draws from `money` domain)
-- `commission`: observed/measured 1OP (draws from `money` domain)
-- `compensation`: 1OPiC derived as salary + commission in context of employees
-The schema entry `#{compensation => money}` declares which domain the
-derived 1OPiC draws its values from.
-
-** Binary Relations
-Comparisons are proper relations (not domains!):
-```
-Less_Than_Integer = {(a, b) | a, b in Z, a < b}
-```
-To express "x < 5", we check: `(x, 5) in Less_Than_Integer`
-
-** First-Order Logic Interface
-Constraints become membership tests in relations:
-- `x < 5` becomes `(x, 5) in less_than`
-- `x > 3 AND x < 10` becomes `(3, x) in less_than AND (x, 10) in less_than`
-
-** Negation
-Negation requires an explicit universe: `not(R, Universe)` computes
-the complement of R within Universe.
diff --git a/docs/data-model.puml b/docs/data-model.puml
deleted file mode 100644
index 59e2cff..0000000
--- a/docs/data-model.puml
+++ /dev/null
@@ -1,101 +0,0 @@
-@startuml data-model
-!theme plain
-title Data Model Core Abstractions
-
-class attribute {
-  + hash: SHA256
-  + value: term()
-}
-
-class tuple {
-  + hash: SHA256
-  + relation: atom()
-  + attribute_map: #{name => hash}
-}
-
-class relation {
-  + hash: SHA256
-  + name: atom()
-  + tree: merkle_tree()
-  + schema: #{attr => type_relation}
-  + constraints: constraints()
-  + cardinality: {finite, N} | aleph_zero | continuum
-  + generator: function() | undefined
-  + provenance: provenance()
-}
-
-class type_relation {
-  + name: atom()
-  + erlang_type: type()
-  + membership_predicate: function()
-  + unfold_generator: function()
-  + cardinality: aleph_zero | continuum
-}
-
-class database_state {
-  + hash: SHA256
-  + name: atom()
-  + tree: merkle_tree()
-  + relations: #{name => hash}
-  + type_relations: #{name => type_relation}
-  + timestamp: integer()
-}
-
-database_state "1" *-- "many" relation : contains
-database_state "1" *-- "many" type_relation : defines types
-relation "1" *-- "many" tuple : contains
-tuple "1" *-- "many" attribute : references
-relation --> type_relation : schema references
-
-note right of attribute
-  Content-Addressed Storage:
-  - SHA-256 hash of value
-  - Automatic deduplication
-  - Immutable once stored
-
-  Value Validation:
-  Value must be member of
-  type relation specified in schema
-end note
-
-note right of relation
-  Storage Strategy:
-  - Finite: Merkle tree (materialized)
-  - Infinite: Generator (lazy)
-
-  Type Relations:
-  - Primitives: natural, integer, real, string
-  - Composite: views over other relations
-end note
-
-note left of type_relation
-  **Schema Philosophy:**
-  Attributes are typed by type relations (not primitives).
-  Types are relations (stored as infinite relations).
-  Schema validation = membership checking.
-
-  **Type Relations are Relations:**
-  They define domains via:
-  1. Erlang type constraint
-  2. Additional predicates
-  3. Unfold generator for enumeration
-
-  Examples:
-  - natural[X] :- integer[X], X >= 0
-  - complex[X] :- X is (A,B), real[A], real[B]
-end note
-
-note bottom of database_state
-  **Schema Example:**
-  employee relation schema:
-  #{
-    name => non_empty_string,  % type relation
-    age => natural,             % type relation
-    salary => positive_integer  % type relation
-  }
-
-  Each schema value is a reference to a type relation,
-  NOT a primitive type string like "integer"
-end note
-
-@enduml
diff --git a/docs/distribution-architecture.puml b/docs/distribution-architecture.puml
deleted file mode 100644
index fd2fd8c..0000000
--- a/docs/distribution-architecture.puml
+++ /dev/null
@@ -1,63 +0,0 @@
-@startuml distribution-architecture
-!theme plain
-title Future Distribution Architecture (Proposed)
-
-node "Node 1" {
-  component "Domino Instance 1" as D1
-  database "Mnesia Replica 1" as M1
-  component "Merkle Tree 1" as MT1
-}
-
-node "Node 2" {
-  component "Domino Instance 2" as D2
-  database "Mnesia Replica 2" as M2
-  component "Merkle Tree 2" as MT2
-}
-
-node "Node 3" {
-  component "Domino Instance 3" as D3
-  database "Mnesia Replica 3" as M3
-  component "Merkle Tree 3" as MT3
-}
-
-cloud "Sync Protocol" {
-  [Hash Comparison] as HC
-  [Delta Transfer] as DT
-  [Conflict Resolution] as CR
-}
-
-D1 --> MT1
-D2 --> MT2
-D3 --> MT3
-
-MT1 --> M1
-MT2 --> M2
-MT3 --> M3
-
-MT1 <--> HC: compare hashes
-MT2 <--> HC
-MT3 <--> HC
-
-HC --> DT: if different
-DT --> CR: if conflict
-CR --> M1: apply changes
-CR --> M2
-CR --> M3
-
-note right of HC
-  Merkle tree enables efficient sync:
-  1. Compare root hashes
-  2. If different, compare subtrees
-  3. Transfer only changed branches
-  4. O(log n) comparison complexity
-end note
-
-note bottom of CR
-  Conflict Resolution Strategies:
-  - Last-write-wins (timestamp)
-  - CRDTs (commutative operations)
-  - Consensus (Raft/Paxos)
-  - Application-defined merge
-end note
-
-@enduml
diff --git a/docs/features.org b/docs/features.org
deleted file mode 100644
index 98350c5..0000000
--- a/docs/features.org
+++ /dev/null
@@ -1,429 +0,0 @@
-#+TITLE: Domino Features & Roadmap
-
-* Extended Relational Model (RM/T)
-  :PROPERTIES:
-  :CATEGORY: semantic-modeling
-  :END:
-  An extended relational database engine based on E. F. Codd's RM/T (1979).
-  Captures more meaning through entity types, surrogates, and molecular semantics.
-
-** Implemented Features
-
-*** DONE Content-Addressed Storage
-    CLOSED: [2025-01-21]
-    - [X] SHA-256 surrogates for all entities
-    - [X] System-controlled entity identifiers (E-domain)
-    - [X] Automatic deduplication via content addressing
-    - [X] Immutable data structures
-
-*** DONE Entity Types (E-Relations)
-    CLOSED: [2025-01-21]
-    - [X] Kernel entity types (database, relation)
-    - [X] E-relations for entity existence assertion
-    - [X] Surrogate-based entity identification
-    - [X] Entity integrity enforcement
-
-*** DONE Property Relations (P-Relations)
-    CLOSED: [2025-01-21]
-    - [X] Immediate property storage
-    - [X] Single-valued property support
-    - [X] Property integrity (Rule 4)
-    - [X] Foreign key references via surrogates
-
-*** DONE Merkle Tree Integration
-    CLOSED: [2025-01-21]
-    - [X] Relations as Merkle trees
-    - [X] Database state versioning
-    - [X] Efficient state diffing
-    - [X] Content-addressed relation hashing
-
-*** DONE Volcano Iterator Model
-    CLOSED: [2025-01-21]
-    - [X] Lazy tuple evaluation
-    - [X] Process-based iterators
-    - [X] Message-passing protocol
-    - [X] Memory-bounded queries
-
-*** DONE Transactional Operations
-    CLOSED: [2025-01-21]
-    - [X] ACID guarantees via Mnesia
-    - [X] Atomic tuple insertion
-    - [X] Tuple retraction with transactions
-    - [X] Relation clear and retract operations
-
-*** DONE Comprehensive Test Suite
-    CLOSED: [2025-01-21]
-    - [X] Database creation tests
-    - [X] Relation and tuple operations
-    - [X] Hash consistency validation
-    - [X] Iterator protocol tests
-    - [X] Retraction and truncate tests
-    - [X] Join operation tests
-    - [X] Provenance tracking tests
-
-*** DONE Attribute-Level Provenance Tracking
-    CLOSED: [2025-01-22]
-    - [X] Nested metadata structure (meta.provenance)
-    - [X] Track immediate source of each attribute
-    - [X] Always enabled - every tuple includes metadata
-    - [X] Automatic provenance merging in joins
-    - [X] Conflict resolution for duplicate attributes
-    - [X] Clean separation of data attributes and metadata
-    - [X] Foundation for tuple-level lineage tracking (implemented)
-
-** Planned RM/T Extensions
-
-*** TODO Characteristic Entities
-    Multi-valued properties as subordinate entities.
-    - [ ] Characteristic entity types (C-relations)
-    - [ ] Characteristic graph (CG-relation)
-    - [ ] Characteristic tree hierarchy
-    - [ ] Characteristic integrity (Rule 5)
-    - [ ] Example: Job history as characteristic of Employee
-
-*** TODO Associative Entities
-    Relationships as first-class entities with properties.
-    - [ ] Associative entity types (A-relations)
-    - [ ] Association graph (AG-relation)
-    - [ ] Association integrity (Rule 6)
-    - [ ] Higher-order associations
-    - [ ] Example: Assignment(employee, project, start_date)
-
-*** TODO Generalization Hierarchies
-    Entity subtyping and inheritance.
-    - [ ] Unconditional gen inclusion (UGI-relation)
-    - [ ] Alternative gen inclusion (AGI-relation)
-    - [ ] Subtype integrity (Rule 7)
-    - [ ] Property inheritance
-    - [ ] Multiple inheritance support
-    - [ ] Example: Engineer/Secretary/Trucker subtypes of Employee
-
-*** TODO Cover Aggregation
-    Collections and groupings.
-    - [ ] Cover membership relation (KG-relation)
-    - [ ] Cover entity types
-    - [ ] Dynamic membership
-    - [ ] Heterogeneous covers
-    - [ ] Example: Convoys, Teams, Departments
-
-*** TODO Event Precedence
-    Temporal ordering and scripts.
-    - [ ] Event entity types (T-relations)
-    - [ ] Unconditional successor (US-relation)
-    - [ ] Alternative successor (AS-relation)
-    - [ ] Unconditional predecessor (UP-relation)
-    - [ ] Alternative predecessor (AP-relation)
-    - [ ] Example: Order → Shipment → Invoice
-
-*** TODO Extended Operators
-    Operators for molecular semantics.
-    - [ ] OUTER NATURAL JOIN
-    - [ ] OUTER UNION
-    - [ ] OUTER THETA-JOIN
-    - [ ] MAYBE operators (null handling)
-    - [ ] Graph operators (OPEN, CLOSE, STEP)
-
-*** TODO RM/T Catalog
-    Extensible schema catalog.
-    - [ ] CATR (relations catalog)
-    - [ ] CATRA (relation-attribute)
-    - [ ] CATA (attributes catalog)
-    - [ ] CATAD (attribute-domain)
-    - [ ] CATD (domains catalog)
-    - [ ] CATC (categories catalog)
-    - [ ] CATRC (relation-category)
-
-*** TODO Property Graph (PG-relation)
-    Link P-relations to E-relations.
-    - [ ] Property molecule types
-    - [ ] Dynamic property schema
-    - [ ] Property graph traversal
-
-** Classical Relational Algebra
-
-*** TODO Selection (σ)
-    Filter tuples by predicate.
-    - [ ] THETA-SELECT with comparison operators
-    - [ ] Support for <, ≤, =, ≥, >, ≠
-    - [ ] TRUE and MAYBE versions (null handling)
-
-*** TODO Projection (π)
-    Project relation onto subset of attributes.
-    - [ ] Remove specified columns
-    - [ ] Eliminate duplicate rows
-    - [ ] Preserve set semantics
-
-*** TODO Cartesian Product (×)
-    Cross product of two relations.
-    - [ ] Unrestricted concatenation
-    - [ ] Basis for joins
-
-*** DONE Natural Join (⋈)
-    CLOSED: [2025-01-22]
-    Join on common attributes.
-    - [X] Equi-join with duplicate removal (equijoin_iterator)
-    - [X] Nested loop join strategy
-    - [X] Attribute conflict resolution (right_ prefix)
-    - [X] Attribute-level provenance tracking
-    - [X] Comprehensive test coverage
-
-*** DONE Theta Join (⋈θ)
-    CLOSED: [2025-01-22]
-    Join with arbitrary comparison.
-    - [X] Support all theta operators via predicate functions
-    - [X] Generalizes natural join
-    - [X] Nested loop join with custom predicates
-    - [X] Provenance merging from both sides
-
-*** TODO Union (∪)
-    Set union of compatible relations.
-    - [ ] Union-compatible constraint
-    - [ ] Duplicate removal
-
-*** TODO Intersection (∩)
-    Set intersection.
-    - [ ] Union-compatible constraint
-
-*** TODO Difference (−)
-    Set difference.
-    - [ ] Union-compatible constraint
-
-*** TODO Divide (÷)
-    Relational division.
-    - [ ] Algebraic universal quantifier
-
-*** TODO Rename (ρ)
-    Attribute renaming.
-    - [ ] Enable self-joins
-
-** Advanced Features
-
-*** DONE Tuple-Level Lineage Tracking
-    CLOSED: [2025-01-23]
-    Track complete operational history of each tuple through query pipelines.
-
-**** Status: IMPLEMENTED
-
-**** API Usage
-
-    Metadata tracking is ALWAYS enabled. All tuples include the 'meta' field:
-    #+BEGIN_SRC erlang
-    %% Simple query (metadata automatically included)
-    Iter = operations:get_tuples_iterator(DB, employees, #{}).
-
-    %% With constraints (metadata still included)
-    Iter = operations:get_tuples_iterator(DB, employees,
-        #{constraints => #{age => {gt, 30}}}).
-
-    %% Results always have:
-    %% #{id => 1, name => "Alice",
-    %%   meta => #{
-    %%     provenance => #{id => {employees, id}, name => {employees, name}},
-    %%     lineage => {base, employees}
-    %%   }}
-    #+END_SRC
-
-**** Provenance vs. Lineage
-
-    - *Provenance* (IMPLEMENTED): Tracks immediate source of each attribute
-      #+BEGIN_SRC erlang
-      meta => #{
-        provenance => #{
-          name => {employees, name},
-          dept_name => {departments, dept_name}
-        }
-      }
-      #+END_SRC
-
-    - *Lineage* (IMPLEMENTED): Tracks complete operation tree that created the tuple
-      #+BEGIN_SRC erlang
-      meta => #{
-        provenance => #{...},  % Attribute sources
-        lineage => {project, [name, dept_name],
-                     {join, dept_id,
-                       {select, fun(T) -> maps:get(age, T) > 30 end,
-                         {base, employees}},
-                       {base, departments}}}
-      }
-      #+END_SRC
-
-**** Type Definition
-
-    #+BEGIN_SRC erlang
-    -type lineage_op() ::
-        {base, atom()}                                    % Base relation
-      | {select, fun(), lineage_op()}                     % Filter operation
-      | {project, [atom()], lineage_op()}                 % Projection
-      | {join, atom(), lineage_op(), lineage_op()}        % Join on attribute
-      | {theta_join, fun(), lineage_op(), lineage_op()}   % Join with predicate
-      | {sort, fun(), lineage_op()}                       % Sort operation
-      | {take, pos_integer(), lineage_op()}               % Limit operation
-      | {aggregate, atom(), atom(), lineage_op()}.        % Aggregation (future)
-    #+END_SRC
-
-**** Use Cases
-
-    - [ ] *Updatable Views*: Propagate updates back to base relations
-      - Example: =UPDATE view SET name = "Bob"= → trace lineage → =UPDATE employees SET name = "Bob"=
-
-    - [ ] *Incremental View Maintenance*: Identify affected tuples when base data changes
-      - Example: If employees tuple changes, lineage identifies which view tuples need recomputation
-
-    - [ ] *Audit Trails*: Track how sensitive data was transformed
-      - Example: "This salary came from: employees → join(departments) → aggregate(avg)"
-
-    - [ ] *Query Explanation*: Debug complex pipelines
-      - Example: "Why is this tuple here?" → inspect lineage to see operations applied
-
-    - [ ] *Provenance Queries*: Query the lineage itself
-      - Example: "Show all tuples derived from employees.id=5"
-
-**** Implementation Plan
-
-    1. [X] Extend =tuple_metadata()= type with lineage field
-    2. [X] Add lineage construction to each iterator operator
-       - [X] select_iterator: ={select, Predicate, ChildLineage}=
-       - [X] project_iterator: ={project, Attributes, ChildLineage}=
-       - [X] equijoin_iterator: ={join, Attr, LeftLineage, RightLineage}=
-       - [X] theta_join_iterator: ={theta_join, Pred, LeftLineage, RightLineage}=
-       - [X] sort_iterator: ={sort, CompareFun, ChildLineage}=
-       - [X] take_iterator: ={take, N, ChildLineage}=
-    3. [X] Implement lineage merging in joins (combine operation trees)
-    4. [ ] Add lineage querying API for provenance analysis (future)
-    5. [ ] Use lineage for updatable view update propagation (future)
-    6. [X] Add comprehensive lineage tests
-
-**** Relation to Existing Code
-
-    Relation-level provenance already exists in =#relation.provenance=:
-    #+BEGIN_SRC erlang
-    -type provenance() ::
-        {base, atom()}
-      | {join, provenance(), provenance()}
-      | {select, provenance(), constraints()}
-      | {project, provenance(), [atom()]}
-      | {take, provenance(), pos_integer()}.
-    #+END_SRC
-
-    This tracks where *relations* come from. Lineage is the *tuple-level*
-    equivalent, tracking operational history of individual tuples through
-    query pipelines.
-
-**** Example: Complete Lineage Chain
-
-    #+BEGIN_SRC erlang
-    % Query: employees → select(age>30) → join(departments) → project([name, dept_name])
-
-    % Resulting tuple with full lineage:
-    #{name => "Alice",
-      dept_name => "Engineering",
-      meta => #{
-        provenance => #{
-          name => {employees, name},
-          dept_name => {departments, dept_name}
-        },
-        lineage => {
-          project, [name, dept_name],
-          {join, dept_id,
-            {select, fun(T) -> maps:get(age, T) > 30 end,
-              {base, employees}},
-            {base, departments}}}
-      }}
-
-    % From this lineage, we can:
-    % 1. Trace "Alice" back to employees.name
-    % 2. Know she passed the age>30 filter
-    % 3. See she was joined with departments on dept_id
-    % 4. Understand the projection removed other attributes
-    #+END_SRC
-
-*** TODO Null Value Handling
-    Three-valued logic for incomplete information.
-    - [ ] "Value unknown" null type
-    - [ ] "Property inapplicable" null type
-    - [ ] E-null for "entity unknown"
-    - [ ] Null substitution principle
-    - [ ] MAYBE operators
-
-*** TODO Infinite Relations (Aleph₀)
-    Countably infinite relation generators.
-    - [ ] Integer generator
-    - [ ] Arithmetic relations (plus, minus, multiply)
-    - [ ] Lazy evaluation with constraints
-    - [ ] Partially materialized storage
-    - [ ] User-defined generators
-
-*** TODO View Integration
-    Merging multiple perspectives.
-    - [ ] View definition language
-    - [ ] Automatic view maintenance
-    - [ ] View update translation
-
-*** TODO Temporal Support
-    Time-varying databases.
-    - [ ] Transaction time
-    - [ ] Valid time
-    - [ ] Bitemporal support
-    - [ ] Non-forgetting mode
-
-*** TODO Distributed Synchronization
-    Merkle tree-based replication.
-    - [ ] Efficient diff protocol
-    - [ ] Conflict resolution
-    - [ ] Eventual consistency
-
-** Developer Experience
-
-*** TODO Query Language
-    High-level relational query language.
-    - [ ] Algebraic syntax
-    - [ ] Tuple calculus variant
-    - [ ] Domain calculus variant
-
-*** TODO REPL Console
-    Interactive query environment.
-    - [ ] Live query evaluation
-    - [ ] Schema introspection
-    - [ ] Query history
-
-*** TODO Visualization Tools
-    Graphical representation.
-    - [ ] Relation browser
-    - [ ] Join graph visualization
-    - [ ] Generalization hierarchy diagrams
-    - [ ] Query execution plans
-
-*** TODO Org Babel Integration
-    Literate programming support.
-    - [ ] Execute relational queries in org-mode
-    - [ ] Export results to tables
-    - [ ] Reproducible analysis
-
-** Documentation & Validation
-
-*** DONE Code Documentation
-    CLOSED: [2025-01-21]
-    - [X] Module architecture overview
-    - [X] Data structure specifications
-    - [X] Usage examples
-    - [X] Implementation details
-
-*** TODO Theoretical Validation
-    Ensure correctness.
-    - [ ] Formal proofs of operator properties
-    - [ ] Closure verification
-    - [ ] Idempotence tests
-    - [ ] Property-based testing with PropEr
-    - [ ] Comparison with Date & Darwen semantics
-
-*** TODO Research Papers
-    Link to foundational theory.
-    - [ ] Codd 1970: "A Relational Model"
-    - [ ] Codd 1979: "Extending the Database Relational Model" (RM/T)
-    - [ ] Codd 1985: "Does AlOL Need the Relational Algebra?"
-    - [ ] Date & Darwen: "Foundation for Future Database Systems"
-
-** References
-   - E. F. Codd (1979). "Extending the Database Relational Model to Capture More Meaning"
-   - E. F. Codd (1970). "A Relational Model of Data for Large Shared Data Banks"
-   - C. J. Date & Hugh Darwen. "Foundation for Future Database Systems: The Third Manifesto"
diff --git a/docs/infinite-relations.puml b/docs/infinite-relations.puml
deleted file mode 100644
index cd6aa0f..0000000
--- a/docs/infinite-relations.puml
+++ /dev/null
@@ -1,177 +0,0 @@
-@startuml infinite-relations
-!theme plain
-title Infinite Type Relations: Unfold Pattern & Membership
-
-abstract class InfiniteTypeRelation {
-  + name: atom()
-  + cardinality: aleph_zero | continuum
-  + erlang_type: type()
-  + membership_predicate: function()
-  + unfold_generator: function()
-  + constraints: constraints()
-}
-
-class Naturals {
-  Erlang Type: integer()
-  Membership: natural[X] :-
-    erlang:is_integer(X),
-    X >= 0.
-
-  Unfold Generator:
-  unfold(0, fun(N) -> N + 1 end)
-  → 0, 1, 2, 3, ...
-
-  Cardinality: aleph_zero
-}
-
-class Integers {
-  Erlang Type: integer()
-  Membership: integer[X] :-
-    erlang:is_integer(X).
-
-  Unfold Generator:
-  unfold({0, 1}, fun({N, S}) ->
-    case S of
-      1 -> {N, -1};
-      -1 -> {N+1, 1}
-    end
-  end)
-  → 0, 1, -1, 2, -2, ...
-
-  Cardinality: aleph_zero
-}
-
-class Rationals {
-  Erlang Type: {integer(), integer()}
-  Membership: rational[X] :-
-    X is (P, Q),
-    integer[P], integer[Q],
-    Q ≠ 0.
-
-  Unfold Generator:
-  Stern-Brocot tree unfold
-  → (0,1), (1,1), (1,2), ...
-
-  Cardinality: aleph_zero
-}
-
-class Reals {
-  Erlang Type: float()
-  Membership: real[X] :-
-    erlang:is_float(X).
-
-  Unfold Generator:
-  IEEE 754 float enumeration
-  (impractical, continuum)
-
-  Cardinality: continuum
-}
-
-class Strings {
-  Erlang Type: string()
-  Membership: string[X] :-
-    erlang:is_list(X),
-    all_chars(X).
-
-  Unfold Generator:
-  Length-ordered, lexicographic
-  → "", "a", "b", ..., "aa", ...
-
-  Cardinality: aleph_zero
-}
-
-class Plus {
-  Erlang Type: {integer(), integer(), integer()}
-  Membership: plus[A, B, Sum] :-
-    integer[A], integer[B],
-    Sum is A + B.
-
-  Unfold Generator:
-  Diagonalization of ℤ × ℤ
-  → (0,0,0), (0,1,1), (1,0,1), ...
-
-  Cardinality: continuum (ℤ × ℤ)
-}
-
-package "Constraint Application" {
-  class ConstrainedGenerator {
-    Pattern: Apply constraints during unfold
-    base_generator: unfold()
-    constraints: [constraint()]
-    ..
-    filter_unfold(Gen, Constraints) ->
-      filter(Gen, satisfies_all(Constraints))
-  }
-
-  note bottom of ConstrainedGenerator
-    **Example 1: Bounded Naturals**
-    natural[X], X >= 0, X =< 100
-    → Generates: 0, 1, 2, ..., 100 (finite!)
-
-    **Example 2: Constrained Plus**
-    plus[5, B, 12]
-    → Solves: B = 7
-    → Generates: single tuple (5, 7, 12)
-
-    **Example 3: Range Query**
-    integer[X], X >= -10, X =< 10
-    → Generates: 0, 1, -1, 2, -2, ..., 10, -10
-  end note
-}
-
-package "Composite Type Relations (Views)" {
-  class Complex {
-    Type Definition (Karuta):
-    complex[X] :-
-      X is (A, B),
-      real[A], real[B].
-
-    Implementation:
-    Unfold real × real with
-    product enumeration
-
-    Not primitive: Defined as view
-    over primitive real relation
-  }
-}
-
-InfiniteTypeRelation <|-- Naturals
-InfiniteTypeRelation <|-- Integers
-InfiniteTypeRelation <|-- Rationals
-InfiniteTypeRelation <|-- Reals
-InfiniteTypeRelation <|-- Strings
-InfiniteTypeRelation <|-- Plus
-
-Naturals --> ConstrainedGenerator: apply\nconstraints
-Integers --> ConstrainedGenerator
-Rationals --> ConstrainedGenerator
-Plus --> ConstrainedGenerator
-
-Reals --> Complex: used in\nproduct
-Complex : (view relation)
-
-note right of Naturals
-  **Core Pattern:** Infinite relations use unfold
-  to generate members. Primitive types are
-  infinite relations.
-
-  **Membership:** Erlang type + constraints
-
-  **Unfold Pattern:**
-  unfold(Seed, Step) generates infinite sequence:
-  Seed, Step(Seed), Step(Step(Seed)), ...
-
-  This enables lazy evaluation and
-  constraint-based pruning.
-end note
-
-note left of Plus
-  **Function Relations:**
-  Mathematical functions like plus, multiply, etc.
-  are relations with continuum cardinality.
-
-  Membership = evaluation
-  Generation = enumeration
-end note
-
-@enduml
diff --git a/docs/infinite_relations_design.org b/docs/infinite_relations_design.org
deleted file mode 100644
index c13e783..0000000
--- a/docs/infinite_relations_design.org
+++ /dev/null
@@ -1,348 +0,0 @@
-#+TITLE: Infinite Relations Design
-#+AUTHOR: Nekoma Team
-#+DATE: 2025-01-22
-
-* Overview
-
-This document specifies the design for infinite relations in Domino, enabling
-countably infinite (ℵ₀) and uncountably infinite (continuum) relations alongside
-finite relations.
-
-** Core Principle
-
-*Everything is a relation.* Types are relations. Functions are relations.
-Numbers are relations. This unifies the type system with the data model.
-
-* Cardinality System
-
-** Cardinality Types
-
-#+BEGIN_SRC erlang
--type cardinality() :: {finite, non_neg_integer()}  % Finite set with N elements
-                     | aleph_zero                    % Countably infinite (ℵ₀)
-                     | continuum.                    % Uncountably infinite (2^ℵ₀)
-#+END_SRC
-
-** Properties
-
-- Finite relations have explicit tuple count: ={finite, 1000}=
-- Countably infinite relations: =aleph_zero=
-- Uncountably infinite relations: =continuum=
-
-* Extended Data Model
-
-** Modified Relation Record
-
-#+BEGIN_SRC erlang
--record(relation, {
-    hash,           % Content hash (for finite) or generator hash (for infinite)
-    name,           % Relation name (atom)
-    tree,           % Merkle tree (finite only), undefined for infinite
-    schema,         % Schema definition
-    cardinality,    % {finite, N} | aleph_zero | continuum
-    generator,      % Generator function (infinite only), undefined for finite
-    is_function     % Boolean: true if relation represents a function
-}).
-#+END_SRC
-
-** Generator Specification
-
-Generators are functions that produce tuples on-demand based on constraints.
-
-#+BEGIN_SRC erlang
--type generator_spec() ::
-    {primitive, atom()}                          % Built-in: naturals, integers, rationals
-  | {function_relation, atom(), arity()}        % Built-in function: plus/3, times/3
-  | {custom, fun((constraints()) -> tuple())}   % User-defined generator
-  | {derived, relational_operation()}.          % Derived from other relations
-
--type constraints() :: #{
-    attribute_name() => constraint_spec()
-}.
-
--type constraint_spec() ::
-    {eq, value()}                    % Equality: age = 30
-  | {neq, value()}                   % Inequality: age ≠ 30
-  | {lt, value()}                    % Less than: age < 30
-  | {lte, value()}                   % Less than or equal
-  | {gt, value()}                    % Greater than
-  | {gte, value()}                   % Greater than or equal
-  | {in, [value()]}                  % Membership: age in [20,30,40]
-  | {range, value(), value()}        % Range: age in [20..30]
-  | {member_of, relation_name()}.    % Type constraint: x ∈ Naturals
-#+END_SRC
-
-* Primitive Infinite Relations
-
-** Naturals (ℕ)
-
-#+BEGIN_SRC erlang
-Schema: #{value => natural}
-Cardinality: aleph_zero
-Generator: Enumerates 0, 1, 2, 3, ...
-
-Example tuples:
-  #{value => 0}
-  #{value => 1}
-  #{value => 2}
-  ...
-#+END_SRC
-
-** Integers (ℤ)
-
-#+BEGIN_SRC erlang
-Schema: #{value => integer}
-Cardinality: aleph_zero
-Generator: Enumerates 0, 1, -1, 2, -2, 3, -3, ...
-
-Enumeration strategy: Interleave positive and negative
-  f(0) = 0
-  f(2n) = n      (for n > 0)
-  f(2n+1) = -n   (for n > 0)
-#+END_SRC
-
-** Rationals (ℚ)
-
-#+BEGIN_SRC erlang
-Schema: #{numerator => integer, denominator => natural}
-Cardinality: aleph_zero
-Generator: Stern-Brocot tree or Calkin-Wilf sequence
-
-Constraints:
-  - denominator > 0
-  - gcd(numerator, denominator) = 1  (reduced form)
-
-Example tuples:
-  #{numerator => 0, denominator => 1}   % 0/1
-  #{numerator => 1, denominator => 1}   % 1/1
-  #{numerator => 1, denominator => 2}   % 1/2
-  #{numerator => 2, denominator => 1}   % 2/1
-  #{numerator => 1, denominator => 3}   % 1/3
-  ...
-#+END_SRC
-
-** Reals (ℝ) - Theoretical
-
-#+BEGIN_SRC erlang
-Schema: #{value => real}
-Cardinality: continuum
-Generator: Not fully enumerable (conceptual only)
-
-Note: In practice, we can only represent computable reals or
-      algebraic reals (still countable but more expressive).
-#+END_SRC
-
-* Function Relations
-
-A relation R is a *function* if: ∀a ∃!b : (a,b) ∈ R
-
-That is, for every input, there exists exactly one output.
-
-** Plus (addition)
-
-#+BEGIN_SRC erlang
-Name: plus
-Schema: #{a => number, b => number, sum => number}
-Cardinality: aleph_zero (when a,b ∈ ℤ or ℚ)
-Is_function: false (it's a 3-way relation, not (a,b) → sum)
-Function view: plus(a, b) = sum  where (a, b, sum) ∈ Plus
-
-Generator: For each (a, b) pair, yield #{a => A, b => B, sum => A + B}
-
-Constraints required for iteration:
-  - At least two of {a, b, sum} must be bounded
-
-Valid queries:
-  - plus where a ∈ [0..10], b ∈ [0..10]          ✓ (finite result: 121 tuples)
-  - plus where a = 5, b ∈ Naturals               ✓ (countable: {5,0,5}, {5,1,6}, ...)
-  - plus where sum = 10                          ✓ (countable: infinitely many a+b=10)
-  - plus with no constraints                     ✗ (cannot enumerate)
-#+END_SRC
-
-** Times (multiplication)
-
-#+BEGIN_SRC erlang
-Name: times
-Schema: #{a => number, b => number, product => number}
-Cardinality: aleph_zero
-Generator: For each (a, b) pair, yield #{a => A, b => B, product => A * B}
-#+END_SRC
-
-** Successor
-
-#+BEGIN_SRC erlang
-Name: successor
-Schema: #{n => integer, succ => integer}
-Cardinality: aleph_zero
-Is_function: true (n → succ is a function)
-Generator: For each n, yield #{n => N, succ => N + 1}
-#+END_SRC
-
-* Cardinality Algebra
-
-Rules for computing cardinality of relational operations:
-
-** Union (∪)
-
-| Left       | Right      | Result     | Notes                    |
-|------------+------------+------------+--------------------------|
-| {finite,m} | {finite,n} | {finite,≤m+n} | May have duplicates  |
-| {finite,n} | aleph_zero | aleph_zero | Finite + infinite = infinite |
-| aleph_zero | aleph_zero | aleph_zero | ℵ₀ + ℵ₀ = ℵ₀            |
-| aleph_zero | continuum  | continuum  | Continuum dominates      |
-| continuum  | continuum  | continuum  | 2^ℵ₀ + 2^ℵ₀ = 2^ℵ₀      |
-
-** Cartesian Product (×)
-
-| Left       | Right      | Result        | Notes                 |
-|------------+------------+---------------+-----------------------|
-| {finite,m} | {finite,n} | {finite,m·n}  | Product of sizes      |
-| {finite,n} | aleph_zero | aleph_zero    | n · ℵ₀ = ℵ₀           |
-| aleph_zero | aleph_zero | aleph_zero    | ℵ₀ · ℵ₀ = ℵ₀          |
-| aleph_zero | continuum  | continuum     | ℵ₀ · 2^ℵ₀ = 2^ℵ₀      |
-| continuum  | continuum  | continuum     | 2^ℵ₀ · 2^ℵ₀ = 2^ℵ₀   |
-
-** Natural Join (⋈)
-
-Cardinality depends on join selectivity:
-
-| Left       | Right      | Result     | Notes                              |
-|------------+------------+------------+------------------------------------|
-| {finite,m} | {finite,n} | {finite,k} | k ≤ min(m,n) typically            |
-| {finite,n} | aleph_zero | varies     | Could be finite or aleph_zero      |
-| aleph_zero | aleph_zero | varies     | Depends on join condition          |
-
-*Examples:*
-
-#+BEGIN_SRC erlang
-%% Finite ⋈ Infinite (finite result)
-Employees = {finite, 100}     % 100 employees
-Naturals = aleph_zero         % Infinite numbers
-Employees ⋈ Naturals on employee_id = value
-  ⇒ {finite, 100}  % At most 100 matches
-
-%% Infinite ⋈ Infinite (infinite result)
-Naturals ⋈ Plus on Naturals.value = Plus.a
-  ⇒ aleph_zero     % For each natural n, infinite (n,b,n+b) tuples
-
-%% Infinite ⋈ Infinite (finite result with constraints)
-(Naturals where value < 10) ⋈ (Naturals where value < 10)
-  ⇒ {finite, 100}  % 10 × 10 = 100
-#+END_SRC
-
-** Selection (σ)
-
-| Input      | Result     | Notes                              |
-|------------+------------+------------------------------------|
-| {finite,n} | {finite,k} | k ≤ n (filtering reduces size)    |
-| aleph_zero | varies     | Could be finite or aleph_zero      |
-| continuum  | varies     | Could be any cardinality           |
-
-*Examples:*
-
-#+BEGIN_SRC erlang
-σ(Naturals, value < 10)    ⇒ {finite, 10}      % Bounded selection
-σ(Naturals, value > 5)     ⇒ aleph_zero         % Infinite result
-σ(Naturals, value % 2 = 0) ⇒ aleph_zero         % Even numbers (infinite)
-#+END_SRC
-
-** Projection (π)
-
-| Input      | Result     | Notes                           |
-|------------+------------+---------------------------------|
-| {finite,n} | {finite,k} | k ≤ n (duplicates removed)     |
-| aleph_zero | aleph_zero | Typically preserves infinity    |
-| continuum  | continuum  | Typically preserves cardinality |
-
-* Constraint System
-
-** Mandatory Constraints
-
-Queries on infinite relations *must* provide constraints that bound the iteration.
-
-#+BEGIN_SRC erlang
-%% INVALID: Cannot iterate infinite relation without constraints
-Iterator = get_tuples_iterator(DB, naturals).  ❌
-
-%% VALID: Bounded by constraint
-Iterator = get_tuples_iterator(DB, naturals, #{value => {range, 0, 100}}).  ✓
-#+END_SRC
-
-** Constraint Validation
-
-Before executing a query on an infinite relation, validate:
-
-1. *Finite result check*: Do constraints guarantee finite result?
-2. *Bounded iteration check*: Can we enumerate results in finite time?
-
-#+BEGIN_SRC erlang
-validate_constraints(Relation, Constraints) ->
-    case Relation#relation.cardinality of
-        {finite, _} ->
-            ok;  % Finite relations don't need constraints
-        aleph_zero ->
-            case infers_finite_result(Relation, Constraints) of
-                true -> ok;
-                false -> {error, unbounded_iteration}
-            end;
-        continuum ->
-            {error, uncountable_relation}  % Cannot iterate continuum
-    end.
-#+END_SRC
-
-** Constraint Inference
-
-Smart inference of finiteness:
-
-#+BEGIN_SRC erlang
-%% These constraints imply finite results:
-#{value => {range, 0, 100}}                    % Range is finite
-#{value => {in, [1,2,3,4,5]}}                  % Membership in finite set
-#{value => {lt, 10}}                           % Bounded above (if naturals)
-
-%% These do NOT imply finite results:
-#{value => {gt, 10}}                           % Unbounded above
-#{value => {neq, 5}}                           % Excludes one element
-#+END_SRC
-
-* Implementation Strategy
-
-** Phase 1: Core Infrastructure
-1. Extend =relation= record with =cardinality= and =generator= fields
-2. Implement cardinality algebra functions
-3. Add constraint validation framework
-
-** Phase 2: Primitive Relations
-1. Implement =naturals= generator
-2. Implement =integers= generator (interleaving strategy)
-3. Implement =rationals= generator (Stern-Brocot or Calkin-Wilf)
-
-** Phase 3: Function Relations
-1. Implement =plus= relation
-2. Implement =times= relation
-3. Implement =successor=, =predecessor= relations
-
-** Phase 4: Query Engine
-1. Extend iterator model to support generators
-2. Implement constraint-based enumeration
-3. Add cardinality inference for query results
-
-** Phase 5: Relational Operators
-1. Extend join to handle infinite relations
-2. Extend union with cardinality tracking
-3. Extend selection with constraint propagation
-
-* Open Questions
-
-1. *Partial materialization*: Should we cache generated tuples?
-2. *Generator composition*: How to compose generators for derived relations?
-3. *Constraint solving*: Do we need a full constraint solver (CLP)?
-4. *Termination guarantees*: How to prove queries terminate?
-5. *Physical storage*: How to persist infinite relation definitions?
-
-* References
-
-- Codd, E. F. (1979). "Extending the Database Relational Model"
-- Cantor, G. "On the Cardinality of Sets"
-- Stern-Brocot Tree: Enumeration of rationals
-- Calkin-Wilf Tree: Alternative rational enumeration
diff --git a/docs/iterator-pipeline.puml b/docs/iterator-pipeline.puml
deleted file mode 100644
index 810ef63..0000000
--- a/docs/iterator-pipeline.puml
+++ /dev/null
@@ -1,45 +0,0 @@
-@startuml iterator-pipeline
-!theme plain
-title Volcano Iterator Model - Process Pipeline
-
-component "Scan Iterator\n(Process)" as P1 {
-  [Read from Relation] as S1
-}
-
-component "Select Iterator\n(Process)" as P2 {
-  [Apply Predicate] as S2
-}
-
-component "Project Iterator\n(Process)" as P3 {
-  [Filter Attributes] as S3
-}
-
-component "Sort Iterator\n(Process)" as P4 {
-  [Sort All Tuples] as S4
-}
-
-component "Take Iterator\n(Process)" as P5 {
-  [Limit N Tuples] as S5
-}
-
-P1 -right-> P2: {next, Pid}\n{tuple, T} | done
-P2 -right-> P3: {next, Pid}\n{tuple, T} | done
-P3 -right-> P4: {next, Pid}\n{tuple, T} | done
-P4 -right-> P5: {next, Pid}\n{tuple, T} | done
-
-note bottom of P1
-  Each iterator is an
-  independent Erlang process
-
-  Message passing protocol:
-  - Request: {next, CallerPid}
-  - Response: {tuple, Data} | done
-
-  Benefits:
-  - Lazy evaluation
-  - Memory-bounded
-  - Composable
-  - Concurrent
-end note
-
-@enduml
diff --git a/docs/karuta-interface-layers.puml b/docs/karuta-interface-layers.puml
deleted file mode 100644
index cd5443e..0000000
--- a/docs/karuta-interface-layers.puml
+++ /dev/null
@@ -1,65 +0,0 @@
-@startuml karuta-interface-layers
-!theme plain
-title Karuta Interface Architecture Layers
-
-actor "Karuta Program" as Karuta
-
-package "Language Bindings" {
-  [Karuta FFI] as FFI
-  [Erlang Ports] as Ports
-  [NIF (Native)] as NIF
-}
-
-package "Stable Contract Layer" {
-  component "domino.erl" as DominoAPI {
-    [create_database/1]
-    [execute/2]
-    [query/2]
-    [transaction/2]
-  }
-}
-
-package "Command Processor" {
-  [Command Parser] as CmdParser
-  [Validator] as Validator
-  [Executor] as Executor
-}
-
-package "Implementation Layer" {
-  component "operations.erl" as Ops {
-    [create_relation/3]
-    [create_tuple/3]
-    [get_tuples_iterator/2]
-    [etc...]
-  }
-}
-
-database "Mnesia Storage" as Storage
-
-Karuta --> FFI
-Karuta --> Ports
-Karuta --> NIF
-
-FFI --> DominoAPI
-Ports --> DominoAPI
-NIF --> DominoAPI
-
-DominoAPI --> CmdParser
-CmdParser --> Validator
-Validator --> Executor
-
-Executor --> Ops
-Ops --> Storage
-
-note right of DominoAPI
-  Stable, versioned interface
-  Command format:
-  {Verb, Entity, Name, Parameters}
-
-  Examples:
-  {create, relation, employee, Schema}
-  {insert, tuple, employee, Data}
-  {query, relation, employee, Constraints}
-end note
-
-@enduml
diff --git a/docs/merkle-tree-hierarchy.puml b/docs/merkle-tree-hierarchy.puml
deleted file mode 100644
index 4e86e26..0000000
--- a/docs/merkle-tree-hierarchy.puml
+++ /dev/null
@@ -1,50 +0,0 @@
-@startuml merkle-tree-hierarchy
-!theme plain
-title Merkle Tree Hierarchy
-
-package "Database Level" {
-  [Database Hash] as DBHash
-  database "Merkle Tree of Relations" as DBTree
-}
-
-package "Relation Level" {
-  [Relation Hash 1] as R1Hash
-  [Relation Hash 2] as R2Hash
-  [Relation Hash N] as RNHash
-
-  database "Merkle Tree of Tuples (R1)" as R1Tree
-  database "Merkle Tree of Tuples (R2)" as R2Tree
-}
-
-package "Tuple Level" {
-  [Tuple Hash 1.1] as T11
-  [Tuple Hash 1.2] as T12
-  [Tuple Hash 2.1] as T21
-  [Tuple Hash 2.2] as T22
-}
-
-DBHash --> DBTree
-DBTree --> R1Hash
-DBTree --> R2Hash
-DBTree --> RNHash
-
-R1Hash --> R1Tree
-R2Hash --> R2Tree
-
-R1Tree --> T11
-R1Tree --> T12
-R2Tree --> T21
-R2Tree --> T22
-
-note bottom of DBHash
-  Single hash represents
-  entire database state
-
-  Benefits:
-  - Version control
-  - Efficient diffing
-  - Distributed sync
-  - Integrity verification
-end note
-
-@enduml
diff --git a/docs/module-dependencies.puml b/docs/module-dependencies.puml
deleted file mode 100644
index dcc955b..0000000
--- a/docs/module-dependencies.puml
+++ /dev/null
@@ -1,39 +0,0 @@
-@startuml module-dependencies
-!theme plain
-title Module Dependencies
-
-package "Entry Points" {
-  [main.erl] as Main
-  [repl.erl] as REPL
-}
-
-package "Server Layer" {
-  [xml_server_app.erl] as XMLApp
-  [xml_server.erl] as XMLServer
-}
-
-package "Query Layer" {
-  [query_planner.erl] as Planner
-}
-
-package "Core Layer" {
-  [operations.erl] as Ops
-}
-
-package "Support Modules" {
-  [relation.erl] as Relation
-  [generators.erl] as Generators
-  [visualizer.erl] as Visualizer
-}
-
-Main --> XMLApp
-XMLApp --> XMLServer
-XMLServer --> Planner
-REPL --> Ops
-
-Planner --> Ops
-Ops --> Relation
-Ops --> Generators
-Ops --> Visualizer
-
-@enduml
diff --git a/docs/provenance-lineage.puml b/docs/provenance-lineage.puml
deleted file mode 100644
index 4e8f68a..0000000
--- a/docs/provenance-lineage.puml
+++ /dev/null
@@ -1,69 +0,0 @@
-@startuml provenance-lineage
-!theme plain
-title Provenance and Lineage Tracking
-
-component "Base Tuple\n(employee)" as T1
-
-note right of T1
-  **Data:**
-  id = 1
-  name = "Alice"
-  age = 30
-  salary = 100000
-
-  **Meta:**
-  provenance:
-    id: (employee, id)
-    name: (employee, name)
-    age: (employee, age)
-    salary: (employee, salary)
-  lineage: (base, employee)
-end note
-
-component "After Select\n(age > 25)" as T2
-
-note right of T2
-  **Data:**
-  id = 1
-  name = "Alice"
-  age = 30
-  salary = 100000
-
-  **Meta:**
-  provenance: (same as above)
-  lineage:
-    select
-    fun(T) -> age > 25 end
-    (base, employee)
-end note
-
-component "After Project\n[name, age]" as T3
-
-note right of T3
-  **Data:**
-  name = "Alice"
-  age = 30
-
-  **Meta:**
-  provenance:
-    name: (employee, name)
-    age: (employee, age)
-  lineage:
-    project
-    [name, age]
-    (select, _, (base, employee))
-end note
-
-T1 -down-> T2: select operation\nadds to lineage
-T2 -down-> T3: project operation\nfilters provenance
-
-note bottom of T3
-  **Benefits:**
-  - Data source tracking
-  - Query result explanation
-  - Reproducibility
-  - Debugging support
-  - Foundation for updatable views
-end note
-
-@enduml
diff --git a/docs/query-execution-flow.puml b/docs/query-execution-flow.puml
deleted file mode 100644
index 998b0e2..0000000
--- a/docs/query-execution-flow.puml
+++ /dev/null
@@ -1,54 +0,0 @@
-@startuml query-execution-flow
-!theme plain
-title Query Execution Flow
-
-actor Client
-participant "Query Planner" as Planner
-participant "Scan Iterator" as Scan
-participant "Select Iterator" as Select
-participant "Project Iterator" as Project
-participant "Operations API" as Ops
-database "Mnesia" as DB
-
-Client -> Planner: query({project,\n  {select, {scan, employee}, Pred},\n  [name, age]})
-activate Planner
-Planner -> Planner: parse & validate
-Planner -> Scan: spawn_iterator(employee)
-activate Scan
-Planner -> Select: spawn_iterator(Scan, Pred)
-activate Select
-Planner -> Project: spawn_iterator(Select, [name, age])
-activate Project
-Planner --> Client: {ok, Iterator}
-deactivate Planner
-
-Client -> Project: next_tuple()
-Project -> Select: next_tuple()
-Select -> Scan: next_tuple()
-Scan -> Ops: get_tuples_iterator(employee)
-Ops -> DB: transaction(read tuple)
-DB --> Ops: {ok, Tuple}
-Ops --> Scan: {ok, Tuple}
-Scan --> Select: {ok, Tuple}
-Select -> Select: apply Predicate
-Select --> Project: {ok, Tuple}
-Project -> Project: filter attributes
-Project --> Client: {ok, #{name => "Alice", age => 30}}
-
-Client -> Project: next_tuple()
-Project -> Select: next_tuple()
-Select -> Scan: next_tuple()
-Scan -> Ops: get_tuples_iterator(employee)
-Ops -> DB: transaction(read tuple)
-DB --> Ops: done
-Ops --> Scan: done
-Scan --> Select: done
-Select --> Project: done
-Project --> Client: done
-
-Client -> Project: close_iterator()
-deactivate Project
-deactivate Select
-deactivate Scan
-
-@enduml
diff --git a/docs/reactive-queries.puml b/docs/reactive-queries.puml
deleted file mode 100644
index bcba5d5..0000000
--- a/docs/reactive-queries.puml
+++ /dev/null
@@ -1,51 +0,0 @@
-@startuml reactive-queries
-!theme plain
-title Reactive Queries (Live Subscriptions)
-
-participant "Client" as C
-participant "Subscription Manager" as SM
-participant "Domino" as D
-database "employee relation" as E
-
-C -> SM: subscribe(query: "age > 30")
-activate SM
-SM -> D: register_subscription(employee, predicate)
-activate D
-D -> E: initial query
-E --> D: [{name: "Alice", age: 35}]
-D --> SM: initial results
-SM --> C: [{name: "Alice", age: 35}]
-deactivate D
-deactivate SM
-
-... time passes ...
-
-C -> D: insert(employee, {name: "Bob", age: 32})
-activate D
-D -> D: check affected subscriptions
-D -> D: evaluate predicate on new tuple\n(32 > 30? yes)
-D -> SM: notify(subscription_id, {inserted: "Bob"})
-activate SM
-SM -> C: delta: {inserted: {name: "Bob", age: 32}}
-deactivate SM
-deactivate D
-
-C -> D: insert(employee, {name: "Charlie", age: 25})
-activate D
-D -> D: evaluate predicate\n(25 > 30? no)
-D -> D: no notification needed
-deactivate D
-
-note right of SM
-  Subscription tracks:
-  - Relation(s) to watch
-  - Filter predicate
-  - Client callback
-
-  On mutation:
-  1. Check which subscriptions affected
-  2. Evaluate predicate on changed tuples
-  3. Send delta (not full re-query)
-end note
-
-@enduml
diff --git a/docs/reliability_roadmap.org b/docs/reliability_roadmap.org
deleted file mode 100644
index d47a00e..0000000
--- a/docs/reliability_roadmap.org
+++ /dev/null
@@ -1,223 +0,0 @@
-#+TITLE: Sakura Reliability Roadmap (Precise)
-
-* Scope
-
-Build Sakura into a correct and efficient first-order predicate logic (FOPL)
-relational algebra engine where relations are first-class values with:
-
-- *Extension* :: denotation as a tuple set (finite stored set or generated stream)
-- *Intension* :: logical meaning (schema + normalized constraints + derivation)
-
-* Formal Position on Issue =#48=
-
-Issue =#48= is *not* semantic redundancy.
-
-- =constraint:create_1op/3= is an attribute-constraint *definition* constructor.
-- =constraint:add_attribute_constraint/3= is a relation-level *binding* operation.
-
-They are distinct layers. The defect is API ambiguity and weak invariants.
-
-- [ ] Require key/record coherence: key =:= =#attribute_constraint.attribute=.
-- [ ] Provide one canonical "declare and bind" path to prevent invalid states.
-
-* Relation Contract (Non-Negotiable)
-
-** C1 Representation Contract
-
-- [ ] Exactly one extension mode per relation:
-  - finite stored: =tree =/= undefined= and =generator= is factory for tree iterator
-  - generated: =tree == undefined= and =generator= is mandatory
-- [ ] Intension is always =#relation_constraints{}=, never raw =#{}=.
-- [ ] =membership_criteria= is either removed (Issue =#47=) or treated as a derived cache from constraints, never a second source of truth.
-
-** C2 Identity Contract
-
-- [ ] Relation hash function is canonical and identical across all mutation paths.
-- [ ] Hash input includes the same semantic fields in the same order, with explicit versioned format.
-- [ ] Any relation update that changes intension or extension must change hash deterministically.
-
-** C3 Algebraic Closure Contract
-
-- [ ] Every algebra operator returns a relation with valid extension + intension.
-- [ ] Constraint propagation rules are explicit and tested per operator.
-- [ ] Result schema and constraints are compatible and normalized.
-
-* Current Critical Correctness Gaps
-
-- [ ] Non-canonical relation hash updates in =src/operations.erl=.
-- [ ] Split semantics between =constraints= and =membership_criteria=.
-- [ ] Mixed constraints shapes (=#relation_constraints{}= and raw maps).
-- [ ] Placeholder substitution search in =constraint:find_satisfying_substitution/4=.
-- [ ] Derived infinite/finite relations not consistently honoring constraints (=#13=, =#14=).
-- [ ] Dual planner paths with mismatched behavior in =src/query_planner.erl=.
-- [ ] Iterator close protocol mismatch (=stop= vs =close= forms).
-- [ ] XML schema endpoint assumes map constraints and crashes.
-
-* Workstreams
-
-** W0 Safety and Determinism (P0)
-
-- [ ] Fix =xml_server= SCHEMA serialization for record constraints (=src/xml_server.erl=).
-- [ ] Replace ad-hoc prints with =logger= (=#39=), remove debug output in constraint lookup.
-- [ ] Make =repl:start/0= non-destructive; add explicit destructive reset command.
-- [ ] Standardize iterator termination protocol across all iterator loops.
-- [ ] Normalize constraints type in all constructors (planner/operators/operations).
-
-*Acceptance criteria*
-
-- [ ] No SCHEMA crash under any built-in relation set.
-- [ ] No unsolicited stdout noise during normal queries.
-- [ ] No relation loss on default REPL startup.
-- [ ] No orphan iterator processes after collect/close paths.
-
-** W1 FOPL Semantics Core (P1)
-
-- [ ] Implement full variable binding search and substitution for partial constraints.
-- [ ] Define and enforce formula AST for =and/or/not/exists/forall=.
-- [ ] Separate logical membership from physical storage existence checks.
-- [ ] Decide and document two-valued logic policy (no NULL) or explicit three-valued policy.
-- [ ] Complete 1OPiC modeling (=#42=) and baseline 1OP constraints (=#28=).
-
-*Acceptance criteria*
-
-- [ ] Quantified constraints produce correct truth values on finite fixtures.
-- [ ] Membership equivalence tests pass for stored vs generated extension of same intension.
-- [ ] Constraint violation diagnostics identify failing attribute/formula branch.
-
-** W2 Constraint Model Consistency (P1)
-
-- [ ] Resolve =#48= with scope-safe API (define vs bind) and strict invariant checks.
-- [ ] Implement relation creation with constraints in one call (=#15=).
-- [ ] Decide fate of =membership_criteria= (=#47=): remove or strict derivation cache.
-- [ ] Add migration helper to convert legacy constraint maps to =#relation_constraints{}=.
-- [ ] Establish extension/intension introspection API for debugging and tooling.
-
-*Acceptance criteria*
-
-- [ ] No public path can construct mismatched attribute constraint key/record pairs.
-- [ ] New relation creation API supports schema + constraints atomically.
-- [ ] Intension is serialized/deserialized in one normalized shape everywhere.
-
-** W3 Planner Unification (P1)
-
-- [ ] Remove dual compile paths; keep one logical -> rewrite -> physical pipeline.
-- [ ] Add semantic validation (schema compatibility, attribute existence, constraint shape).
-- [ ] Add rewrite rules: projection pruning, predicate pushdown, limited join reordering.
-- [ ] Add typed planner errors for REPL/XML consumers.
-
-*Acceptance criteria*
-
-- [ ] Same query plan always yields same output schema and row semantics across interfaces.
-- [ ] Planner rejects invalid plans with stable machine-readable reasons.
-
-** W4 Algebra Completeness and Performance (P2)
-
-- [ ] Implement union/intersection/difference with strict compatibility checks.
-- [ ] Implement semijoin/antijoin/division.
-- [ ] Add hash join and merge join; keep nested loop fallback.
-- [ ] Enforce bounded execution preconditions for blocking operators over infinite relations.
-- [ ] Improve tuple hash retrieval path performance (=#7=).
-
-*Acceptance criteria*
-
-- [ ] Algebra law regression tests pass for finite relations (where laws apply).
-- [ ] Join strategy selection is observable and benchmarked.
-- [ ] Infinite + blocking plans fail fast with actionable diagnostics unless bounded.
-
-** W5 Versioning and Updatable Views (P2)
-
-- [ ] Implement branch metadata and lineage (=#43=).
-- [ ] Implement fast-forward merge semantics and conflict checks (=#44=).
-- [ ] Implement provenance-safe updatable ephemeral views (=#26=).
-
-*Acceptance criteria*
-
-- [ ] Branch/merge operations are deterministic and test-covered.
-- [ ] Updatable views reject ambiguous write-back paths.
-
-** W6 Interfaces and Hardening (P2)
-
-- [ ] Replace XML =erl_eval= execution with safe parsed DSL/AST.
-- [ ] Version protocol responses and provide structured errors.
-- [ ] Add explain-analyze metrics (rows, time, strategy, spills/materialization).
-- [ ] Add visualizer mode for relation semantics (schema, constraints, lineage, extension mode).
-- [ ] Integrate or deprecate =relation.erl= helper model.
-
-*Acceptance criteria*
-
-- [ ] No arbitrary code execution path through external query interface.
-- [ ] Interface responses are stable under malformed input and concurrency.
-
-* GitHub Issue Mapping
-
-** Core reliability and semantics
-
-- [ ] =#39= logging
-- [ ] =#15= define constraints at finite relation creation
-- [ ] =#14= derived finite from infinite honors/inherits constraints
-- [ ] =#13= derived infinite honors constraints
-- [ ] =#7= tuple hash retrieval performance
-
-** Constraint/data model
-
-- [ ] =#48= clarify define/bind API and enforce invariants
-- [ ] =#47= remove/replace membership_criteria split
-- [ ] =#42= proper 1OPiC model
-- [ ] =#28 #29 #30 #31= 1st/2nd/3rd/4th order property constraints
-
-** Versioning and updates
-
-- [ ] =#43= branching
-- [ ] =#44= fast-forward merge
-- [ ] =#26= updatable views
-
-** Optional research tracks
-
-- [ ] =#45= nullary relations vs booleans
-- [ ] =#40= state monad
-- [ ] =#41= C node for hot loops
-- [ ] =#19= chessboard integration
-
-* Verification Matrix (Must Exist in CI)
-
-- [ ] Unit tests: constraints AST eval, membership semantics, hash determinism
-- [ ] Property tests: algebra laws, hash stability, propagation invariants
-- [ ] Integration tests: REPL flows, XML QUERY/NEXT/CLOSE/SCHEMA, malformed inputs
-- [ ] Performance tests: join algorithms, bounded infinite queries, Merkle hash retrieval
-- [ ] Concurrency tests: iterator lifecycle and server session cleanup
-
-* Milestones and Exit Criteria
-
-** M1 (Safety Baseline)
-
-- Deliver W0
-- Close target issues: =#39 #15 #14 #13 #7=
-- Exit: no destructive default startup, no XML schema crash, no protocol-level iterator leaks
-
-** M2 (Semantic Correctness)
-
-- Deliver W1 + W2
-- Close target issues: =#48 #47 #42 #28= (with foundations for =#29 #30 #31=)
-- Exit: extension/intension invariants hold across create/query/derive flows
-
-** M3 (Planner and Performance)
-
-- Deliver W3 + W4
-- Exit: unified planner, bounded infinite behavior, measurable join improvements
-
-** M4 (Versioned Workflows)
-
-- Deliver W5 + W6
-- Close target issues: =#43 #44 #26=
-- Exit: deterministic branch/merge and safe updatable views with stable interfaces
-
-* Execution Order
-
-1. W0 Safety and Determinism
-2. W1 FOPL Semantics Core
-3. W2 Constraint Model Consistency
-4. W3 Planner Unification
-5. W4 Algebra Completeness and Performance
-6. W5 Versioning and Updatable Views
-7. W6 Interfaces and Hardening
-8. Optional research tracks (=#45 #40 #41 #19=)
diff --git a/docs/roadmap.puml b/docs/roadmap.puml
deleted file mode 100644
index 42ad8c2..0000000
--- a/docs/roadmap.puml
+++ /dev/null
@@ -1,72 +0,0 @@
-@startuml roadmap
-!theme plain
-title Suggested Implementation Roadmap
-
-package "Phase 1: Stable Interface (MVP)" {
-  [domino.erl wrapper] as P1_1
-  [Command interface] as P1_2
-  [Basic constraint validation] as P1_3
-  [Karuta FFI bindings] as P1_4
-}
-
-package "Phase 2: Type System" {
-  [Fake-relations primitives] as P2_1
-  [Constraint-based refinement] as P2_2
-  [Subtype checking] as P2_3
-  [Type inference] as P2_4
-}
-
-package "Phase 3: Advanced Constraints" {
-  [Foreign keys] as P3_1
-  [Functional dependencies] as P3_2
-  [Tuple/relation-level constraints] as P3_3
-  [Transition constraints] as P3_4
-}
-
-package "Phase 4: Query Features" {
-  [Updatable views] as P4_1
-  [Materialized views] as P4_2
-  [Query optimization] as P4_3
-  [Explain plans] as P4_4
-}
-
-package "Phase 5: Distribution" {
-  [Merkle sync] as P5_1
-  [Multi-node replication] as P5_2
-  [Partition strategies] as P5_3
-  [Consistency protocols] as P5_4
-}
-
-package "Phase 6: Advanced Features" {
-  [Temporal queries] as P6_1
-  [Reactive queries] as P6_2
-  [Constraint solving] as P6_3
-  [Datalog engine] as P6_4
-}
-
-P1_1 -down-> P2_1
-P1_2 -down-> P2_2
-P1_3 -down-> P3_1
-P1_4 -down-> P2_1
-
-P2_1 -down-> P3_1
-P2_2 -down-> P3_2
-P2_3 -down-> P3_3
-P2_4 -down-> P4_1
-
-P3_1 -down-> P4_1
-P3_2 -down-> P4_2
-P3_3 -down-> P4_3
-P3_4 -down-> P4_4
-
-P4_1 -down-> P5_1
-P4_2 -down-> P5_2
-P4_3 -down-> P5_3
-P4_4 -down-> P6_1
-
-P5_1 -down-> P6_1
-P5_2 -down-> P6_2
-P5_3 -down-> P6_3
-P5_4 -down-> P6_4
-
-@enduml
diff --git a/docs/system-overview.puml b/docs/system-overview.puml
deleted file mode 100644
index 8d76fc5..0000000
--- a/docs/system-overview.puml
+++ /dev/null
@@ -1,81 +0,0 @@
-@startuml system-overview
-!theme plain
-title Domino System Overview
-
-package "Client Interfaces" {
-  [XML Server\n(TCP/IP Port 8080)] as XML
-  [REPL\n(Interactive Shell)] as REPL
-  [Direct API\n(Erlang Apps)] as API
-}
-
-package "Query Processing Layer" {
-  package "Query Planner" {
-    [DSL Parser] as Parser
-    [Plan Validation\n& Compilation] as Validator
-  }
-
-  package "Volcano Iterator Model" {
-    [Scan Iterator] as Scan
-    [Select Iterator] as Select
-    [Project Iterator] as Project
-    [Sort Iterator] as Sort
-    [Take Iterator] as Take
-    [Join Iterators] as Join
-  }
-}
-
-package "Operations Layer (API)" {
-  [Database Management] as DBMgmt
-  [Relation Operations] as RelOps
-  [Tuple Operations] as TupleOps
-  [Iterator Management] as IterMgmt
-}
-
-package "Data Model Layer" {
-  [Core Abstractions\nattribute, tuple,\nrelation, database_state] as CoreAbs
-  [Finite Relations\n(Merkle Trees)] as Finite
-  [Infinite Relations\n(Generators)] as Infinite
-}
-
-package "Content-Addressed Storage" {
-  database "Mnesia" {
-    [attribute table] as AttrTable
-    [tuple table] as TupleTable
-    [relation table] as RelTable
-    [database_state table] as DBTable
-  }
-}
-
-XML --> Parser
-REPL --> Parser
-API --> Parser
-
-Parser --> Validator
-Validator --> Scan
-
-Scan --> Select
-Select --> Project
-Project --> Sort
-Sort --> Take
-Join --> Take
-
-Scan --> TupleOps
-Select --> IterMgmt
-Project --> IterMgmt
-
-DBMgmt --> CoreAbs
-RelOps --> CoreAbs
-TupleOps --> CoreAbs
-IterMgmt --> CoreAbs
-
-CoreAbs --> Finite
-CoreAbs --> Infinite
-
-Finite --> AttrTable
-Finite --> TupleTable
-Finite --> RelTable
-Finite --> DBTable
-
-Infinite --> AttrTable
-
-@enduml
diff --git a/docs/temporal-queries.puml b/docs/temporal-queries.puml
deleted file mode 100644
index 7d72ed5..0000000
--- a/docs/temporal-queries.puml
+++ /dev/null
@@ -1,61 +0,0 @@
-@startuml temporal-queries
-!theme plain
-title Temporal Queries with Immutable Database States
-
-database "DB @ t0" as DB0
-note bottom of DB0
-  hash = abc123...
-  timestamp = 2024-01-01 10:00
-
-  relations:
-    employee => hash_e0
-end note
-
-database "DB @ t1" as DB1
-note bottom of DB1
-  hash = def456...
-  timestamp = 2024-01-01 11:00
-
-  relations:
-    employee => hash_e1
-end note
-
-database "DB @ t2" as DB2
-note bottom of DB2
-  hash = ghi789...
-  timestamp = 2024-01-01 12:00
-
-  relations:
-    employee => hash_e2
-end note
-
-database "Current DB" as DB3
-note bottom of DB3
-  hash = jkl012...
-  timestamp = 2024-01-01 13:00
-
-  relations:
-    employee => hash_e3
-end note
-
-DB0 -right-> DB1: insert tuple
-DB1 -right-> DB2: update salary
-DB2 -right-> DB3: delete tuple
-
-note top of DB0
-  **Time Travel Queries:**
-
-  query_at_time(2024-01-01 10:00)
-    → returns DB0
-
-  query_at_time(2024-01-01 12:00)
-    → returns DB2
-
-  diff(DB0, DB3)
-    → (inserted: [...], deleted: [...], modified: [...])
-
-  history(employee, id: 1)
-    → [(t0, state0), (t1, state1), (t2, state2)]
-end note
-
-@enduml
diff --git a/docs/transaction-algo.org b/docs/transaction-algo.org
new file mode 100644
index 0000000..22903ec
--- /dev/null
+++ b/docs/transaction-algo.org
@@ -0,0 +1,12 @@
+* Check if temporary file with the command hash with exists
+To hash the command, we must hash its bytes without the timestamp,
+since it will always vary given it's a transactional time, and add
+instead the commit HEAD of the state of the database.
+
+If such file exists, load the transaction and storage offsets
+alongside the command and attempt to write it as a recovery.
+* Get the transaction offset of the transaction graph file AND storage file
+* Write the offsets to a tmp file
+* Write the command with a flag **flushed** set to false to a tmp file
+* Attempt to execute the command
+* Delete the temporary file
diff --git a/docs/type-checking-flow.puml b/docs/type-checking-flow.puml
deleted file mode 100644
index d1e6654..0000000
--- a/docs/type-checking-flow.puml
+++ /dev/null
@@ -1,108 +0,0 @@
-@startuml type-checking-flow
-!theme plain
-title Type Checking as Relation Membership Checking
-
-participant "Karuta Program" as K
-participant "Type Checker" as TC
-participant "Domino" as D
-database "Type Relations\n(Infinite Relations)" as TR
-
-note over K,TR
-  **Type Checking:** Check if value is member of type relation
-  **Type Relations:** Primitives stored as infinite relations
-  **Membership:** Erlang type check + constraint satisfaction
-end note
-
-K -> TC: insert(employee, {age: 25, name: "Alice"})
-activate TC
-
-TC -> D: check: natural[25]?
-activate D
-D -> TR: membership query: natural[25]
-activate TR
-TR -> TR: 1. Erlang type check:\n   is_integer(25) → true
-TR -> TR: 2. Constraint check:\n   25 >= 0 → true
-TR --> D: true (25 ∈ natural)
-deactivate TR
-D --> TC: member ✓
-deactivate D
-
-TC -> D: check: non_empty_string["Alice"]?
-activate D
-D -> TR: membership query: non_empty_string["Alice"]
-activate TR
-TR -> TR: 1. Check string["Alice"]:\n   is_list("Alice") ∧ all_chars → true
-TR -> TR: 2. Constraint check:\n   length("Alice") > 0 → true
-TR --> D: true ("Alice" ∈ non_empty_string)
-deactivate TR
-D --> TC: member ✓
-deactivate D
-
-TC --> K: type_check passed ✓\n{age: 25, name: "Alice"} ∈ employee
-deactivate TC
-
-== Type Check Failure Example ==
-
-K -> TC: insert(employee, {age: -5, name: ""})
-activate TC
-
-TC -> D: check: natural[-5]?
-activate D
-D -> TR: membership query: natural[-5]
-activate TR
-TR -> TR: 1. Erlang type check:\n   is_integer(-5) → true
-TR -> TR: 2. Constraint check:\n   -5 >= 0 → false ✗
-TR --> D: false (-5 ∉ natural)
-deactivate TR
-D --> TC: not_member ✗
-deactivate D
-
-TC --> K: type_error: -5 ∉ natural\nExpected: natural[Age]\nGot: Age = -5
-deactivate TC
-
-== Composite Type Example ==
-
-K -> TC: check: complex[(3.14, 2.71)]?
-activate TC
-
-TC -> D: check: complex[(3.14, 2.71)]?
-activate D
-note over D
-  complex[X] :-
-    X is (A, B),
-    real[A], real[B].
-end note
-
-D -> TR: membership query: real[3.14]
-activate TR
-TR -> TR: is_float(3.14) → true
-TR --> D: true (3.14 ∈ real)
-deactivate TR
-
-D -> TR: membership query: real[2.71]
-activate TR
-TR -> TR: is_float(2.71) → true
-TR --> D: true (2.71 ∈ real)
-deactivate TR
-
-D --> TC: member ✓\n(3.14, 2.71) ∈ complex
-deactivate D
-
-TC --> K: type_check passed ✓
-deactivate TC
-
-note right of TR
-  **Type Relation Storage:**
-  - Primitives: infinite relations
-  - Membership: predicate evaluation
-  - No materialization needed
-  - Lazy constraint checking
-
-  **Example:**
-  natural[X] is stored as:
-  - erlang_type: integer()
-  - constraint: X >= 0
-  - generator: unfold(0, +1)
-end note
-
-@enduml
diff --git a/docs/type-hierarchy.puml b/docs/type-hierarchy.puml
deleted file mode 100644
index c53a965..0000000
--- a/docs/type-hierarchy.puml
+++ /dev/null
@@ -1,289 +0,0 @@
-@startuml type-hierarchy
-!theme plain
-title Type System: Stratified Universes & Types as Relations
-
-package "Universe Stratification" {
-  class "Universe₀" as U0 {
-    Base values
-    Examples: 3, -5, 3.14, true, "hello"
-    The set of all runtime values
-  }
-
-  class "Universe₁" as U1 {
-    Type relations (classify values)
-    Examples: natural, integer, real, boolean
-    Each type is a relation over Universe₀
-    Type relations are infinite relations
-  }
-
-  class "Universe₂" as U2 {
-    Type of type relations
-    The classifier of type relations
-    Prevents self-reference paradoxes
-  }
-
-  class "Universe₃" as U3 {
-    Meta-type level
-    Type : Universe₂ : Universe₃
-  }
-
-  U0 : Universe₁
-  U1 : Universe₂
-  U2 : Universe₃
-  U3 : Universe₄
-
-  note right of U1
-    **Stratification prevents Russell's Paradox**
-    Type relations live in Universe₁
-    and classify values in Universe₀.
-    A type cannot contain itself.
-
-    natural : Universe₁
-    3 ∈ natural (3 ∈ Universe₀)
-    But: natural ∉ natural ✗ (universe mismatch)
-  end note
-}
-
-package "Supertypes (Universe₁)" {
-  class Number {
-    Membership: number[X] where X : Universe₀
-    Definition: Union of all numeric types
-    number[X] :- natural[X]; integer[X];
-                 rational[X]; real[X].
-    Allows polymorphism over numeric types
-    Universe level: Universe₁
-  }
-
-  class Scalar {
-    Membership: scalar[X] where X : Universe₀
-    Definition: Atomic (non-composite) values
-    scalar[X] :- number[X]; boolean[X]; string[X].
-    Universe level: Universe₁
-  }
-}
-
-package "Numeric Type Relations (Universe₁)" {
-  class Naturals {
-    Membership: natural[X] where X : Universe₀
-    Criteria:
-    - X is erlang:integer()
-    - X >= 0
-    Cardinality: aleph_zero
-    Generator: 0, 1, 2, 3, ...
-    Universe level: Universe₁
-  }
-
-  class Integers {
-    Membership: integer[X] where X : Universe₀
-    Criteria:
-    - X is erlang:integer()
-    Cardinality: aleph_zero
-    Generator: 0, 1, -1, 2, -2, ...
-    Universe level: Universe₁
-  }
-
-  class Rationals {
-    Membership: rational[X] where X : Universe₀
-    Criteria:
-    - X is (P, Q)
-    - integer[P], integer[Q]
-    - Q ≠ 0
-    Cardinality: aleph_zero
-    Generator: Stern-Brocot tree
-    Universe level: Universe₁
-  }
-
-  class Reals {
-    Membership: real[X] where X : Universe₀
-    Criteria:
-    - X is erlang:float()
-    Cardinality: continuum
-    Generator: IEEE 754 floats
-    Universe level: Universe₁
-  }
-}
-
-package "Other Primitive Types (Universe₁)" {
-  class Strings {
-    Membership: string[X] where X : Universe₀
-    Criteria:
-    - X is erlang:string()
-    Cardinality: aleph_zero
-    Ordering: by length, then lexicographic
-    Universe level: Universe₁
-  }
-
-  class Booleans {
-    Membership: boolean[X] where X : Universe₀
-    Criteria:
-    - X is erlang:boolean()
-    - X ∈ {true, false}
-    Cardinality: 2
-    Universe level: Universe₁
-  }
-}
-
-package "Constrained Type Relations (Universe₁)" {
-  class PositiveIntegers {
-    Definition: positive_int[X] where X : Universe₀
-    Criteria:
-    - integer[X]
-    - X > 0
-    Relation: positive_int ⊆ integer
-    Universe level: Universe₁
-  }
-
-  class BoundedInt {
-    Definition: bounded_int[X, Min, Max]
-    where X : Universe₀
-    Criteria:
-    - integer[X]
-    - Min ≤ X ≤ Max
-    Relation: bounded_int ⊆ integer
-    Universe level: Universe₁
-  }
-
-  class NonEmptyStrings {
-    Definition: non_empty_string[X]
-    where X : Universe₀
-    Criteria:
-    - string[X]
-    - length(X) > 0
-    Relation: non_empty_string ⊆ string
-    Universe level: Universe₁
-  }
-}
-
-package "Composite Type Relations (Universe₁)" {
-  class Complex {
-    Definition (Karuta-style):
-    complex[X] where X : Universe₀
-    complex[X] :-
-      X is (A, B),
-      real[A], real[B].
-
-    Interpretation:
-    - (A, B) where A is real part
-    - B is imaginary part
-    Relation: complex ⊆ real × real
-    Universe level: Universe₁
-  }
-
-  class Employee {
-    Definition:
-    employee[X] where X : Universe₀
-    employee[X] :-
-      X is (Name, Age, Salary),
-      non_empty_string[Name],
-      positive_int[Age],
-      positive_int[Salary].
-
-    Relation: employee ⊆ string × ℕ⁺ × ℕ⁺
-    Universe level: Universe₁
-  }
-}
-
-' Universe stratification relationships
-U1 --> U0 : classifies values in
-U2 --> U1 : types type relations
-U3 --> U2 : meta-level
-
-' All type relations live in Universe₁
-U1 ..> Number : contains
-U1 ..> Naturals : contains
-U1 ..> Integers : contains
-U1 ..> Rationals : contains
-U1 ..> Reals : contains
-U1 ..> Booleans : contains
-U1 ..> Strings : contains
-U1 ..> Scalar : contains
-
-' Type relation hierarchy (within Universe₁)
-Number <|-- Naturals : ⊇
-Number <|-- Integers : ⊇
-Number <|-- Rationals : ⊇
-Number <|-- Reals : ⊇
-
-Number <|-- Scalar : ⊇
-Booleans <|-- Scalar : ⊇
-Strings <|-- Scalar : ⊇
-
-' Subset relations among numeric types
-Naturals .up.|> Integers : ⊆
-Integers .up.|> Rationals : ⊆
-Rationals .up.|> Reals : ⊆
-
-' Constrained types
-Integers .down.|> PositiveIntegers : ⊇
-Integers .down.|> BoundedInt : ⊇
-Strings .down.|> NonEmptyStrings : ⊇
-
-' Composite types (also in Universe₁)
-Number .down.|> Complex : number × number
-Complex : (view: pair of numbers)
-
-Scalar .down.|> Employee : scalar × scalar × scalar
-Employee : (view: string × nat × nat)
-
-note right of Complex
-  **Views as Type Relations:**
-  Types can be defined as relational views
-  over other type relations.
-
-  Example using supertype:
-  complex[C] :- C is (R, I),
-                number[R], number[I].
-
-  Or more specifically:
-  complex[C] :- C is (R, I),
-                real[R], real[I].
-
-  Views can use supertypes for flexibility!
-  All views live in Universe₁.
-end note
-
-note left of Number
-  **Core Principle:** Every type is a relation
-  Type checking = membership checking in relations
-  T1 <: T2 iff T1 ⊆ T2 (subset relation)
-
-  **Supertypes enable polymorphism:**
-  A function can accept number[X] and work
-  with naturals, integers, rationals, or reals.
-
-  **Universe Levels:**
-  All type relations: Universe₁
-  All values: Universe₀
-  Type of types: Universe₂
-
-  **Erlang Type Mapping:**
-  natural → integer() + (≥ 0)
-  integer → integer()
-  rational → {integer(), integer()}
-  real → float()
-  string → string()
-  boolean → boolean()
-end note
-
-note bottom of U0
-  **Avoiding Russell's Paradox:**
-
-  Like F*, Domino uses predicative universe
-  stratification. The key invariant:
-
-  Type u#i : Type u#(i+1)
-
-  In Domino:
-  - Values (3, "hello", true) : Universe₀
-  - Type relations (natural, string) : Universe₁
-  - Type : Universe₂
-
-  This prevents:
-  natural ∈ natural (universe mismatch!)
-
-  A type relation cannot be a member of itself.
-  All type relations classify values in Universe₀
-  but exist at Universe₁.
-end note
-
-@enduml