Console composer allows you to store a composition with the same name as a component of one of its components

[PetrosPapapa]

Trying to store a composition with the same name as on of its components fails. However, storing it with the same name as one of the component of one of its components succeeds.

Reproduce:

create "P" [`A`] `B`;;
create "Q" [`B`] `C`;;
join "P" "" "Q" "";;
store "_Step1" "R";;
create "S" [`C`] `D`;;
join "R" "" "S" "C";;
store "_Step2" "P";;

Atomic process P gets replaced by a composite process that has R as a component, which in turn has the atomic P as a component. This breaks R as its component P is no longer available. It also creates an undesirable recursive specification.

One could argue this should not be allowed at the level of the logic, but the proof state does not know about components of components, so it allows it.