equal
deleted
inserted
replaced
67 MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" |
67 MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" |
68 |
68 |
69 MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)" |
69 MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)" |
70 |
70 |
71 |
71 |
72 lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard] |
72 lemmas E_imp_in_V_L = Graph2 [THEN conjunct1] |
73 lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard] |
73 lemmas E_imp_in_V_R = Graph2 [THEN conjunct2] |
74 |
74 |
75 lemma lemma2: |
75 lemma lemma2: |
76 "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v" |
76 "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v" |
77 apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L]) |
77 apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L]) |
78 apply (rule_tac [3] MA6) |
78 apply (rule_tac [3] MA6) |