(2steps) PrintForm Definitions mb state machine Sections GenAutomata Doc

At: small state

I:Type, M:(Ism{i:l}()), j:I, x:i:IM(i).state. x M(j).state
By:
Unfolds [`sm_all`;`sm_state`] 0
THEN
Reduce 0
Generated subgoal:

11. I: Type
2. M: Ism{i:l}()
3. j: I
4. x: {(M(i)).ds for i I}
x {(M(j)).ds}

About:
applyfunctionuniversememberall

(2steps) PrintForm Definitions mb state machine Sections GenAutomata Doc