equal
deleted
inserted
replaced
250 using assms |
250 using assms |
251 apply(induct v r) |
251 apply(induct v r) |
252 apply(simp_all add: retrieve_afuse retrieve_encode_STARS) |
252 apply(simp_all add: retrieve_afuse retrieve_encode_STARS) |
253 done |
253 done |
254 |
254 |
255 |
|
256 |
|
257 |
|
258 |
|
259 lemma Q00: |
255 lemma Q00: |
260 assumes "s \<in> r \<rightarrow> v" |
256 assumes "s \<in> r \<rightarrow> v" |
261 shows "\<Turnstile> v : r" |
257 shows "\<Turnstile> v : r" |
262 using assms |
258 using assms |
263 apply(induct) |
259 apply(induct) |
264 apply(auto intro: Prf.intros) |
260 apply(auto intro: Prf.intros) |
265 by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) |
261 by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) |
266 |
262 |
267 lemma Qa: |
263 lemma Qa: |