\begin{table}
\begin{tabular}{|l|}
\hline
\begin{minipage}[t]{\columnwidth}

\begin{ccprogram}
\agent always(A) :: [A, (next\  always(A))]..

\agent if(Cond, Then, Else) :: [Cond -> Then, Cond ~> Else]..

\agent whenever(C, A) :: [C -> A, C ~> whenever(C,A)]..

\agent watching(\_C, {D})      :: {D}..
\agent watching(C, D -> A)    :: D -> watching(C, A)..
\agent watching(C, D ~> A)    :: (C;D) ~> watching(C, A)..
\agent watching(C, (next\   A)) :: C ~> watching(C, A)..
\agent watching(C, Vars^A)    :: Vars^watching(C, A)..
\agent watching(C, \_Vars\$A)   :: watching(C, A)..
\agent watching(\_C, abort)    :: abort..
\agent watching(\_C, [])       :: []..
\agent watching(C, [A | R])   :: [watching(C, A) | watching(C, R)]..
\agent watching(C, Proc)      :: Body\$((Proc::Body) -> watching(C, Body))..
\agent time\_on(C, A)     :: clock(always(C), A)..
\agent do\_watching(C, A) :: clock(whenever(C, (next\  abort)), A)..
\agent susp\_act(C, E, A) :: clock(whenever(C, (next\  E)), A)..
\end{ccprogram}
\end{minipage}\\
\hline
\end{tabular}

\caption{\tgentzen{} definition of assorted combinators.}\label{assorted-def}

\end{table}

\begin{table}
\begin{tabular}{|l|}
\hline
\begin{minipage}[t]{\columnwidth}
\begin{ccprogram}
\agent clock({C},A):: whenever(C, A)..
\agent clock(abort, \_A):: []..
\agent clock(\_A, abort):: abort..
\agent clock([], A) :: A..
\agent clock(\_A, []) :: skip..
\agent clock([B | R], A) :: clock(B, clock(R, A))..
\agent clock(B, [A | R]) :: [clock(B, A) | clock(B, R)]..
\agent clock(next\  \_B, {D})    :: {D}..
\agent clock(next\  B, D -> A)  :: D -> clock(next\   B, A)..
\agent clock(next\  B, D ~> A)  :: D ~> clock(B,A)..
\agent clock(next\  B, next\  A)  :: next\  clock(B,A).. 
\agent clock(next\  B, Vars^A)  :: Vars^clock(next\  B, A)..
\agent clock(next\  B, \_Vars\$A) :: clock(next\  B, A)..
\agent clock(next\  B, Proc)    :: Body\$(Proc::Body -> clock(next\  B, Body))..
\agent clock((\_C -> (next\  \_B)), {D})    :: {D}..
\agent clock((C -> (next\  B)), (D -> A)) :: D -> clock((C -> (next\  B)),A)..
\agent clock((C -> (next\  B)), (D ~> A)) :: [(C -> clock((next\  B), (D ~> A))), ((C,D) ~> A)]..
\agent clock((C -> (next\  B)), next\  A)   :: [(C -> (next\  clock(B,A))), (C ~> A)]..
\agent clock((C -> (next\  B)), Vars^A)   :: Vars^clock((C -> (next\  B)), A)..
\agent clock((C -> (next\  B)), \_Vars\$A)  :: clock((C -> (next\  B)), A)..
\agent clock((C -> (next\  B)), Proc)  :: Body\$(Proc::Body -> clock((C -> (next\  B)), Body))..
\agent clock((\_C ~> \_B), {D})      :: {D}..
\agent clock((C ~> B), (D -> A)) :: D -> clock((C ~> B),A)..
\agent clock((C ~> B), (D ~> A)) :: [(C -> (D ~> A)), ((C, D) ~> clock(B,A))]..
\agent clock((C ~> B), next\  A)   :: [(C -> (next\  A)),   (C ~> clock(B,A))]..
\agent clock((C ~> B), Vars^A)   :: Vars^clock((C ~> B), A)..
\agent clock((C ~> B), \_Vars\$A)   :: clock((C ~> B), A)..
\agent clock((C ~> B), Proc)     :: Body\$(Proc::Body -> clock((C ~> B), Body))..
\agent clock(Proc, A) :: Body\$(Proc::Body -> clock(Body, A))..
\end{ccprogram}
\end{minipage}\\
\hline
\end{tabular}

\caption{\tgentzen{} definition of {\tt clock/2}.}\label{clock-def}
\end{table}