# Check event type and transition conditions

## Intent

I want to move an application only by a suitable event when the conditions hold.

## Wrong form and why it stays silent

```text title="Incorrect form"
// on Filed считают необязательным описанием; либо один when заменяет requires.
```

Carrier type, when, and requires are checked independently. ElectronicFiled is a subtype of Filed; Other does not fit even with all facts. Missing approved is not treated as satisfied.

## Correct form

```law
language "law.core" version "0.2";
package recipes.k.r02 version "0.1.0";
namespace "urn:recipe:k-procedures:02";

entity Application;
event Filed { }
event ElectronicFiled: Filed { }
event Other { }
relation ready(app: Application);
relation approved(app: Application);
procedure Filing(app: Application) {
    state Draft initial;
    state Done terminal;
    transition Submit { from Draft; to Done; on Filed; when ready(app); requires approved(app); }
}
```

## Frozen execution scene

P and Q in the table are different instances; E1/E2/E3 are carriers with an explicitly given time.
All identifiers and instants are pinned in the scenes.

| Events and facts | Question | Answer |
|---|---|---|
| all conditions | `truth(current_state(P,Done))` | `truth_status == TRUE_ONLY;` / `COMPUTED` |
| event subtype | `truth(current_state(P,Done))` | `truth_status == TRUE_ONLY;` / `COMPUTED` |
| required condition missing | `truth(current_state(P,Done))` | `truth_status == NEITHER;` / `COMPUTED` |
| false guard | `truth(current_state(P,Done))` | `truth_status == NEITHER;` / `COMPUTED` |
| foreign type | `truth(current_state(P,Done))` | `truth_status == NEITHER;` / `COMPUTED` |
| without requires | `truth(current_state(P,Done))` | `truth_status == TRUE_ONLY;` / `COMPUTED` |

```law
test "matching carrier and conditions transition" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}
```

```law
test "event subtype transitions" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, ElectronicFiled { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}
```

```law
test "missing approval blocks silently" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;

}
```

```law
test "refuted guard blocks transition" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert not ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;

}
```

```law
test "foreign carrier type mismatches" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Other { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
    expect issue(TRANSITION_CARRIER_TYPE_MISMATCH);
}
```

```law
test "transition passes without requires" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}
```

```python
>>> import runpy
>>> check = runpy.run_path("docs/recipes/k-procedures/resources/check.py")
>>> check["check_steps"](https://github.com/arxohq/law/blob/master/docs/recipes/k-procedures/2)
'К2: причины шагов и отсутствие лишних предупреждений проверены; lawc = lawref'
```

## Counterfactual

Mutation check — LDC-E1344.

Original fragment:

```text
on Filed;
```

Replacement:

```text
on ready;
```

Scenes with a condition removed are marked separately; the same inputs get a different outcome.

## Boundary

requires here reads empirical approved. Cross-procedure completed(P,y) needs a concrete instance and reads only a strict temporal prefix. A guard must not depend on a rule over the fold result (E1348); the witness is [Explain an unreached state](/recipes/k-procedures/why-not-state/).