13 *} |
13 *} |
14 types |
14 types |
15 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list" |
15 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list" |
16 |
16 |
17 constdefs |
17 constdefs |
18 bounded :: "'s step_type => nat => bool" |
18 bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool" |
19 "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n" |
19 "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n" |
20 |
20 |
21 stable :: "'s ord => 's step_type => 's list => nat => bool" |
21 stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" |
22 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q" |
22 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q" |
23 |
23 |
24 stables :: "'s ord => 's step_type => 's list => bool" |
24 stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" |
25 "stables r step ss == !p<size ss. stable r step ss p" |
25 "stables r step ss == !p<size ss. stable r step ss p" |
26 |
26 |
27 is_bcv :: "'s ord => 's => 's step_type |
27 is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type |
28 => nat => 's set => ('s list => 's list) => bool" |
28 \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool" |
29 "is_bcv r T step n A bcv == !ss : list n A. |
29 "is_bcv r T step n A bcv == !ss : list n A. |
30 (!p<n. (bcv ss)!p ~= T) = |
30 (!p<n. (bcv ss)!p ~= T) = |
31 (? ts: list n A. ss <=[r] ts & wt_step r T step ts)" |
31 (? ts: list n A. ss <=[r] ts & wt_step r T step ts)" |
32 |
32 |
33 wt_step :: |
33 wt_step :: |
34 "'s ord => 's => 's step_type => 's list => bool" |
34 "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" |
35 "wt_step r T step ts == |
35 "wt_step r T step ts == |
36 !p<size(ts). ts!p ~= T & stable r step ts p" |
36 !p<size(ts). ts!p ~= T & stable r step ts p" |
37 |
37 |
38 end |
38 end |