equal
deleted
inserted
replaced
175 |
175 |
176 (* 4 *) |
176 (* 4 *) |
177 by (forward_tac [rewrite_rule [Impl.inv1_def] |
177 by (forward_tac [rewrite_rule [Impl.inv1_def] |
178 (inv1 RS invariantE) RS conjunct1] 1); |
178 (inv1 RS invariantE) RS conjunct1] 1); |
179 by (tac2 1); |
179 by (tac2 1); |
180 by(arith_tac 1); |
180 by (arith_tac 1); |
181 |
181 |
182 (* 3 *) |
182 (* 3 *) |
183 by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1); |
183 by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1); |
184 |
184 |
185 by (tac2 1); |
185 by (tac2 1); |
186 by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]); |
186 by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]); |
187 by(arith_tac 1); |
187 by (arith_tac 1); |
188 |
188 |
189 (* 2 *) |
189 (* 2 *) |
190 by (tac2 1); |
190 by (tac2 1); |
191 by (forward_tac [rewrite_rule [Impl.inv1_def] |
191 by (forward_tac [rewrite_rule [Impl.inv1_def] |
192 (inv1 RS invariantE) RS conjunct1] 1); |
192 (inv1 RS invariantE) RS conjunct1] 1); |