tom_circuit_stateless_types[tagT, Tin, Tout: TYPE+]: THEORY
BEGIN

    tom_trans_in_t: TYPE+ = %%% The inputs to a circuit
    [# D: Tin,
       tag: tagT,
       valid: bool,
       stall: bool #];

    tom_inp_seq_t: TYPE+ = [nat -> tom_trans_in_t]; %%% Sequence of inputs 

    pipetheory: LIBRARY = "../pipetheory";
    IMPORTING pipetheory@live_calculus

    is: VAR tom_inp_seq_t;    %%% Input Sequence

    t: VAR nat;

    %%% Inputs
    Din(t, is): Tin = is(t)`D;
    tag_in(t, is): tagT = is(t)`tag;
    val_in(t, is): bool = is(t)`valid;
    stall_in(t, is): bool = is(t)`stall;

    stalli_fintrue(is): bool = %%% G F /stall_in
        finite_true(LAMBDA t: is(t)`stall);


END tom_circuit_stateless_types