Probabilistic Testing Semantics - Semantics of Probabilistic Processes: An Operational Approach - page 81

Fig. 4.2 Separation by a hyperplane. (Reprinted from [ 8 ], with kind permission from Springer
Science+Business Media)

0 large enough so that the point b : scalar d ≥ = ( b 1 , ··· , b i − d , ··· , b n ) falsifies

b <c ; since b is still in B , it contradicts the separation. Thus we continue

h ·

∃ h ∈ [0, 1] n , c ∈ R :
∀

iff

A , b ∈ B :

above comments concerning d

a ∈

b <c<h

h · · a

∃ h ∈ [0, 1] n , c ∈ R ∀ a ∈ A : h · b<c<h · a set b to b ; note b ∈ B

iff :

[0, 1] n , c

implies ∃ h ∈ ∈ R : h · b<c ≤ h · A property of infimum

[0, 1] n , c implies ∃ h ∈ ∈ R : h · B<c ≤ h · Ab ∈ B , hence h · B ≤ h · b

implies ¬ ( ∀ h ∈ [0, 1] n : h · A ≤ h · B )

The proof for the Hoare case is analogous.