equal
deleted
inserted
replaced
47 by (ALLGOALS Asm_full_simp_tac); |
47 by (ALLGOALS Asm_full_simp_tac); |
48 by (blast_tac (claset() delrules [le0]) 1); |
48 by (blast_tac (claset() delrules [le0]) 1); |
49 by (Clarify_tac 1); |
49 by (Clarify_tac 1); |
50 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)", |
50 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)", |
51 "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1); |
51 "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1); |
52 by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2)); |
52 by (REPEAT |
53 |
53 (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2)); |
54 by (Asm_simp_tac 1); |
54 by (Asm_simp_tac 1); |
55 result(); |
55 result(); |
56 |
56 |
57 |
57 |
58 |
58 |