In the marlowe specification we formally prove that computing a transaction of multiple inputs
in a time interval has the same semantics as computing multiple transactions of a single input.
Having an array of this data structure helps the developer to reason about what inputs were applied
to a contract, without caring if they were applied in a single transaction or in multiple ones.
If the input is undefined, the transaction was used to reduce a non quiesent contract.
This can happen to advance a timeout or if the contract doesn't start with a When
In the marlowe specification we formally prove that computing a transaction of multiple inputs in a time interval has the same semantics as computing multiple transactions of a single input. Having an array of this data structure helps the developer to reason about what inputs were applied to a contract, without caring if they were applied in a single transaction or in multiple ones.