Proof procedures for using program composition theorem #118
Description
bir_wm_instTheory contains the theorem bir_map_prog_comp_thm, which allows for enlarging the program upon which the contract is stated. Together with the other composition theorems, this means that contracts for BIR subprogram fragments can be composed, where both are subprograms of a larger program or one is stated on a subprogram of the other.
This needs an accompanying proof procedure to do all necessary reasoning automatically.