fact: Definition correspond (st : @data base_params) (sigma : name -> @data PB_base_params) tr_1 tr_m := let (d, os) := processInputs (state (sigma Primary)) (queue (sigma Primary)) in outputs_m tr_m ++ os = outputs_1 tr_1 /\ d = st.
imports: Verdi(Verdi HandlerMonad)