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

C4 implies that the function g : N × N ₒ R ≥ 0 given by g ( i , j ): = f ( i , j ) +

| f ( i , j ) satisfies conditions C1 , C2 and C3 of Proposition 4.2 . In particular, the

limit lim j ₒ∞ g ( i , j )

|

= 0if f ( i , j ) ≤ 0 for all j ∈ N , and lim j ₒ∞ g ( i , j ) =

2 lim j ₒ∞ | f ( i , j ) | otherwise. Hence

∞ ∞

lim ( f ( i , j ) +| f ( i , j ) | ) = lim

j

( f ( i , j ) +| f ( i , j ) | ) . (4.8)

j ₒ∞ ₒ∞

i = 0 i = 0

Since i = 0 f ( i , j ) = i = 0 ( f ( i , j ) − i = 0 |

+| f ( i , j ) | ) f ( i , j ) | ,wehave

i = 0 ( f ( i , j )

lim j ₒ∞ i = 0 f ( i , j )

i = 0 |

= +| | − |

lim j ₒ∞ f ( i , j ) ) f ( i , j )

[existence of the two limits by ( 4.7 ) and ( 4.8 )]

lim j ₒ∞ i = 0 ( f ( i , j ) lim j ₒ∞ i = 0 | = +| f ( i , j ) | ) − f ( i , j ) |

[by ( 4.7 ) and ( 4.8 )]

i = 0 lim j ₒ∞ ( f ( i , j ) i = 0

= +| f ( i , j ) | ) −

j ₒ∞ |

lim f ( i , j ) |

i = 0 (lim j ₒ∞ ( f ( i , j )

= +| f ( i , j ) | ) − lim j ₒ∞ | f ( i , j ) | )

i = 0 lim j ₒ∞ ( f ( i , j )

= +| f ( i , j ) |−| f ( i , j ) | )

i = 0 lim j ₒ∞ f ( i , j ) .

=

Lemma 4.3 The function C defined in ( 4.1 ) is continuous.

[0, 1] ʩ . We need to show

Proof Let f 0 ≤ f 1 ≤ ... be an increasing chain in R ₒ

that

C f n =

0 C

( f n ) . (4.9)

n ≥ 0 n ≥

For any r ∈ R , we are in one of the following three cases:

ˉ
−ₒ 1. r for some ˉ ∈ ʩ .Wehave

n ≥ 0 f n ( r )( ˉ )

C =

1 by ( 4.1 )

n ≥ 0 1

=

n ≥ 0 C

= ( f n )( r )( ˉ )

n ≥ 0 C

( f n ) ( r )( ˉ ) =