changeset 5620 | 3ac11c4af76a |
parent 5313 | 1861a564d7e2 |
child 5648 | fe887910e32e |
5619:76a8c72e3fd4 | 5620:3ac11c4af76a |
---|---|
9 SubstAx = WFair + Constrains + |
9 SubstAx = WFair + Constrains + |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 LeadsTo :: "['a program, 'a set, 'a set] => bool" |
13 LeadsTo :: "['a program, 'a set, 'a set] => bool" |
14 "LeadsTo prg A B == |
14 "LeadsTo F A B == |
15 leadsTo (Acts prg) |
15 leadsTo (Acts F) |
16 (reachable prg Int A) |
16 (reachable F Int A) |
17 (reachable prg Int B)" |
17 (reachable F Int B)" |
18 end |
18 end |