Let $I$ denote the set of blocks with user-provided initial values in a block diagram. Assume when $I$ is propogated through the block diagram, every block is has a value at time $t=0$. Let $d(t, b)$ denote the set of blocks with user-provided initial values which determine the value of block $b$ at time $t$. For example, in the diagram below colored blocks have initial values and the value of $d$ when applied to to each block for time $t=0$ is displayed. ![image](https://hackmd.io/_uploads/ryrm04FBC.png) Blocks have a single output, and take as input the output of $n$ blocks denoted $b_{i,1}\dots b_{i,n}$. If $b\in I$, then the value of $b(0)$ is user-provided, so $d(0, b)$ is $\{b\}$. Otherwise, $b(0)$ has a value if all $b$'s input blocks have one, so if for some input $b_i$, $b'\in d(0,b_i)$, then $b'\in b(0,b)$. During execution of a block diagram, initial values are propogated as above. Then the value of each $b\in I$ at $t=1$ is computed with the values of $b$'s inputs. Then, those new outputs are propogated through the diagram setting each $b\not\in I$'s value at $t=1$. To be pedantic, if $b\in I$ has no inputs, then it never receives a value at $t=1$ (nor will any blocks reachable from $b$ as there is nothing to propogate) and we say $b$ has no value at $t=1$. We can now formally define $b$. $$ d(t, b) = \begin{cases} \{b\} & \text{if } t=0\land b\in I \\ d(0, b_{i,1})\cup\dots\cup d(0, b_{i,n}) & \text{if } t=0\land b\not\in I \\ d(t-1, b_{i,1})\cup\dots\cup d(t-1, b_{i,n}) & \text{otherwise.} \\ \end{cases} $$ In a sound block diagram, removing $b_i$ from $I$ causes at least one block to not have a value at $t=0$. To why the word "sound" is used, suppose after removing $b$, $b$ still had a value. Then, $b$'s value can be determined from the other initial values $f:I\setminus b\rightarrow b(0)$, but without executing the diagram, we can't know if $f$'s output is the same as the user provided value for $b$ we removed, so we say the diagram is not sound. **Lemma 1.** In a sound block diagram if $b_i\in I$ and has a value at $t=1$, then $b_i\in d(0, b_{i,1})\cup\dots\cup d(0, b_{i,n})$. _Proof_. Towards a contradiction, if $b_i\not\in d(0, b_{i,1})\cup\dots\cup d(0, b_{i,n})$, then the values of $b$'s inputs at $t=0$ can be determined from other blocks with initial values, so after removing $b_i$ from $I$, $b_i(0)$ can still be calculated, but this contradicts our assumption the diagram is sound. Now, lets consider how we can make use of this fact to determine when a block diagram's initial conditions are invalid. In the diagram below, if a block is colored, then it has an initial value on its output. ![image](https://hackmd.io/_uploads/SywyDeYrR.png) Lets propogate these initial values through the diagram, and label each edge with the set of blocks who's initial values determine the value on the edge. That is to say, label each arrow originating at $b_i$ with $d(0, b_i)$. ![image](https://hackmd.io/_uploads/HJRrwlKHR.png) Now that initial values have been propogated. Executing each block will produce its value at $t=1$. Zooming in on block $c$, we can see from the lablels that $d(1,c)=d(0,b)=\{b\}$. However, this contradicts **Lemma 1** which says $c$'s value at $t=1$ must depend on $c$'s initial value ($c\in d(1, c)$)! So the diagram is not sound. To close here's the result of propogating valid initial conditions through a moderately complex diagram which holds up under **Lemma 1**. ![image](https://hackmd.io/_uploads/B10pxWKH0.png)