show that an agent following P will obey the constraints specified by the user. If the agent begins in some state, s E S , we must prove that it will satisfy all of its constraints if and only if V(s) = (f, C, a UC, s, U). We prove the results for forbidding and requiring constraints separately.

Theorem 1 An agent following policy, P, with value function, V, generated as in Section 4.4, from any state s ∈ S will violate a forbidding constraint with probability zero if and only if V(s) = (f, N, U) (for some U and N).

Proof: We prove the theorem by induction over subspaces of the states, classified by how "close" they are to violating a forbidding constraint. More precisely, we partition the state space, S, into subsets, Sk, defined to contain all states that can violate a forbidding constraint after a minimum of k state transitions. In other words, So contains those states that violate a forbidding constraint directly; S 1 contains those states that do not violate any forbidding constraints themselves, but have a successor state (following the transition probability function, P ) that does (i.e., a successor state in S 0 ); S 2 contains those states that do not violate any forbidding constraints, nor have any successors that do, but who have at least one successor state that has a successor state that does (i.e., a successor state in S 1 ); etc. There are at most [ S ] nonempty subsets in this mutually exclusive sequence. To make this partition exhaustive, the special subset, S ∞ , contains all states from which the agent will never violate a forbidding constraint by following P . We first show, by induction over k, that ∀ s ∈ S k (0 ≤ k ≤ | S | ), V(s) = ⟨ t, N, U ⟩, as required by the theorem.

Basis step ( S 0 ): By definition, the agent will violate a forbidding constraint in s ∈ S 0 .

Therefore, either 3c E Cfs such that c(s) = t or 3c E Cfg such that c(s, P(s)) = t, so we know, from Equation 20, V(s) = (t, N, U).

Inductive step ( S k , 1 ≤ k ≤ | S |): Assume, as the induction hypothesis, that ∀ s ′ ∈
Sk-1, V(s') = (t, N', U').  By the definition of Sk, each state, s E Sk, has at least one successor state, s ′ ∈ S k − 1 . Then, according to Equation 20, V(s) = (t, N, U), because the disjunction over S ′ must include s ′ , for which F ′ = t .

Therefore, by induction, we know that for all s E S k (0 ≤ k ≤ | S | ), V ( s ) = ( t, N, U ).

We now show that ∀ s ∈ S ∞ , V(s) = (f, N, U) . We prove, by induction over t, that, for any state, s E S ∞ , V t (s) = (f, N, U).

Basis step (V 0 ): By definition, if s ∈ S ∞ , there cannot exist any c ∈ C f s such that c(s) = t. Then, from Equation 19, V 0 (s) = (f, N 0 , U 0 ).

Inductive step (V t, t > 0): Assume, as the inductive hypothesis, that, for any s' E S ∞,
V t − 1 ( s ′ ) = ( f t N ′ t U ′ ). We know that V t ( s ) = ( f t N t , U t ′ ) if and only if all three disjunctions in Equation 20 are false. The first is false, as described in the basis step. The second term is similarly false, since, by the definition of S ∞ , there cannot exist any c ∈ C f α such that c(s,P(s)) = t. In evaluating the third term, we first note that S' C S ∞. In other words, all of the successor states of s are also in S ∞ (if successor s ′ ∈ S k for some finite k , then s E S k +1 ).  Since all of the successors are in S ∞ , we know, by the inductive hypothesis, that the disjunction over V t -1 in all these successors is false. Therefore, all three disjunctive terms in Equation 20 are false, so V t ( s ) = ( f, N t, U t ).

Therefore, by induction, we know that for all s ∈ S ∞ , V ( s ) = ( f, N, U ). By the definition of the state partition, these two results prove the theorem as required. □