equal
deleted
inserted
replaced
29 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]" |
29 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]" |
30 apply (simp add: list_ex_def is_target_def set_mem_eq) |
30 apply (simp add: list_ex_def is_target_def set_mem_eq) |
31 apply force |
31 apply force |
32 done |
32 done |
33 |
33 |
34 locale lbvc = lbv + |
34 locale (open) lbvc = lbv + |
35 fixes phi :: "'a list" ("\<phi>") |
35 fixes phi :: "'a list" ("\<phi>") |
36 fixes c :: "'a list" |
36 fixes c :: "'a list" |
37 defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>" |
37 defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>" |
38 |
38 |
39 assumes mono: "mono r step (length \<phi>) A" |
39 assumes mono: "mono r step (length \<phi>) A" |