# Prohibition and detecting its violation

## Intention

I want to distinguish a prohibition of an action from a detected violation of that prohibition.

A prohibition executes as a negative maintenance condition.

## Incorrect form and why it stays silent

```text title="Incorrect form"
// Отсутствие performed(p) после окна означает SATISFIED.
```

Absence of information about the action does not prove that the prohibition was observed over the whole window. Satisfaction requires completeness of observations; otherwise after the window the status is UNDETERMINED.

## Correct form

```law
language "law.core" version "0.2";
package recipes.a.r03 version "0.1.0";
namespace "urn:recipe:a-positions:03";

entity Person;
relation registered(p: Person);
relation done(p: Person);
relation performed(p: Person);
rule BanRule strict { for p: Person; when registered(p);
    then prohibition Ban { bearer p; action performed(p); window [@2026-09-01, @2026-09-10]; };
}
rule GuardRule strict { for p: Person; when registered(p);
    then duty Guard { bearer p; maintain not performed(p) during [@2026-09-01, @2026-09-10]; };
}
```

## Frozen execution scene

| Facts and snapshot | Question | Answer |
|---|---|---|
| no action; 2026-09-05 | `positions()` | `position(Ban, ACTIVE); expect position(Guard, ACTIVE);` / `COMPUTED` |
| action performed; 2026-09-05 | `positions()` | `position(Ban, VIOLATED); expect position(Guard, VIOLATED);` / `COMPUTED` |
| action established; after the window, 2026-09-13 | `positions()` | `position(Ban, VIOLATED);` / `COMPUTED` |

```law
test "no action keeps ban active" {
    given {
        context {
            legal_time @2026-09-05;
            decision_time @2026-09-05T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:a-positions:03:p"));
    }
    evaluate positions();
    expect position(Ban, ACTIVE); expect position(Guard, ACTIVE);
    expect evaluation_status == COMPUTED;

}
```

```law
test "performed action violates ban" {
    given {
        context {
            legal_time @2026-09-05;
            decision_time @2026-09-05T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:a-positions:03:p")); assert performed(entity_ref("urn:recipe:a-positions:03:p"));
    }
    evaluate positions();
    expect position(Ban, VIOLATED); expect position(Guard, VIOLATED);
    expect evaluation_status == COMPUTED;

}
```

```law
test "violation persists after window" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:a-positions:03:p")); assert performed(entity_ref("urn:recipe:a-positions:03:p"));
    }
    evaluate positions();
    expect position(Ban, VIOLATED);
    expect evaluation_status == COMPUTED;

}
```

## Counterfactual

Mutation: `action performed(p);` → ``; rejection LDC-E1305. Additional counterfactuals are shown as separate scenes.

## Boundary

Ban and Guard yield the same status. The example uses accepted facts of the current case; a separate search of historical events over the whole window is not performed here. An unestablished action is not treated as performed; an explicit negation in one snapshot does not replace completeness of observations over the whole window.