equal
deleted
inserted
replaced
1002 h pfixGe (sub i o allocAsk) s} |
1002 h pfixGe (sub i o allocAsk) s} |
1003 LeadsTo |
1003 LeadsTo |
1004 {s. h \<le> (giv o sub i o client) s & |
1004 {s. h \<le> (giv o sub i o client) s & |
1005 h pfixGe (ask o sub i o client) s}" |
1005 h pfixGe (ask o sub i o client) s}" |
1006 apply (rule single_LeadsTo_I) |
1006 apply (rule single_LeadsTo_I) |
1007 apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s" |
1007 apply (rule_tac k1 = h and x1 = "(sub i o allocAsk) s" |
1008 in System_lemma2 [THEN LeadsTo_weaken]) |
1008 in System_lemma2 [THEN LeadsTo_weaken]) |
1009 apply auto |
1009 apply auto |
1010 apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe) |
1010 apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe) |
1011 done |
1011 done |
1012 |
1012 |