Fix WHILE case in definition of out. out is deterministic, total

Proving flow_subset now requires flow_apply_twice_same which states that if
applying flow gave an output, then applying flow again on it will give the same
output. This is proved using lemma flow_is_set_ops that states that out is just
a set operation. (flow_apply_twice_same uses this fact as applying same set
operation twice is same as applying once.)