equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 SubstAx = WFair + Constrains + |
9 SubstAx = WFair + Constrains + |
10 |
10 |
11 constdefs |
11 constdefs |
|
12 Ensures :: "['a set, 'a set] => 'a program set" (infixl 60) |
|
13 "A Ensures B == {F. F : (reachable F Int A) ensures B}" |
|
14 |
12 LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) |
15 LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) |
13 "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}" |
16 "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}" |
14 |
17 |
15 end |
18 end |