| changeset 136 | fb3f52fe99d1 |
| parent 130 | 0f124691c191 |
| child 137 | 785c0f6b8184 |
| 135:9b5da0327d43 | 136:fb3f52fe99d1 |
|---|---|
1463 "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)" |
1463 "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)" |
1464 using actions_split create_bc len_action_blockers by linarith |
1464 using actions_split create_bc len_action_blockers by linarith |
1465 |
1465 |
1466 end |
1466 end |
1467 |
1467 |
1468 |
|
1469 unused_thms |
|
1470 |
|
1468 end |
1471 end |