equal
deleted
inserted
replaced
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}" |
14 |
14 |
15 definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where |
15 definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where |
16 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
16 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
17 |
17 |
18 notation (xsymbols) |
18 notation LeadsTo (infixl "\<longmapsto>w" 60) |
19 LeadsTo (infixl " \<longmapsto>w " 60) |
|
20 |
19 |
21 |
20 |
22 text{*Resembles the previous definition of LeadsTo*} |
21 text{*Resembles the previous definition of LeadsTo*} |
23 lemma LeadsTo_eq_leadsTo: |
22 lemma LeadsTo_eq_leadsTo: |
24 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |
23 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |