Trade Logic: Clarification on guarded conjunction

Clarification on guarded conjunction ("Dynamic")

Previously

Earlier I introduced Trade Logic and I said that the well-formedness criterion for formulas could be dynamic in certain limited circumstances. Essentially, if a subformula is conjoined with an appropriate type-check on an object, the object is statically treated as that.

Clarification

I forgot to distinguish this sort of conjunction from the conjunction that "and" implements. It's really not the same thing.

Simple conjunction can't do this right. Simple conjunction is built from 2 decompositions of $1. But there's no reasonable way to decompose the half-box in which the guard fails. Doing so would mean that the type-incorrect subformula was used despite being type-incorrect.

guard

Instead, these guarded conjunctions are headed by guard. Like:

(guard (accepts-type X Y) (X Y))

It decomposes like this. Note that one cannot further decompose the half-box where the guard fails.