proposition: Theorem Fill_ok : forall t : nat, di t di_init cx_init al_init mem_init = di' t di_init cx_init al_init mem_init DC_a DC_d /\ cx t di_init cx_init al_init mem_init = cx' t di_init cx_init al_init mem_init DC_a DC_d /\ al t di_init cx_init al_init mem_init = al' t di_init cx_init al_init mem_init DC_a DC_d /\ mem t di_init cx_init al_init mem_init = mem' t di_init cx_init al_init mem_init DC_a DC_d.
proof: Proof. split. apply di_di'. split. apply cx_cx'. split. apply al_al'. apply mem_mem'. Qed.
imports: Fill_spec Fill_impl