equal
deleted
inserted
replaced
9 header "Kildall's Algorithm" |
9 header "Kildall's Algorithm" |
10 |
10 |
11 theory Kildall = DFA_Framework: |
11 theory Kildall = DFA_Framework: |
12 |
12 |
13 constdefs |
13 constdefs |
14 bounded :: "(nat => nat list) => nat => bool" |
|
15 "bounded succs n == !p<n. !q:set(succs p). q<n" |
|
16 |
|
17 pres_type :: "(nat => 's => 's) => nat => 's set => bool" |
14 pres_type :: "(nat => 's => 's) => nat => 's set => bool" |
18 "pres_type step n A == !s:A. !p<n. step p s : A" |
15 "pres_type step n A == !s:A. !p<n. step p s : A" |
19 |
16 |
20 mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool" |
17 mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool" |
21 "mono r step n A == |
18 "mono r step n A == |