equal
deleted
inserted
replaced
3 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
4 |
4 |
5 Weak LeadsTo relation (restricted to the set of reachable states) |
5 Weak LeadsTo relation (restricted to the set of reachable states) |
6 *) |
6 *) |
7 |
7 |
8 header{*Weak Progress*} |
8 section{*Weak Progress*} |
9 |
9 |
10 theory SubstAx imports WFair Constrains begin |
10 theory SubstAx imports WFair Constrains begin |
11 |
11 |
12 definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where |
12 definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where |
13 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |
13 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |